Smooth

📁 Source: Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

Statistics

Metric	Count
Definitions instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf, instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf, instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf, instCommRingObjOppositeOpensCarrierOfPresheafSmoothSheaf, instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf, instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf, smoothPresheafAddCommGroup, smoothPresheafAddGroup, smoothPresheafCommGroup, smoothPresheafCommRing, smoothPresheafGroup, smoothPresheafRing, smoothSheaf, coeFun, eval, evalAt, evalHom, smoothSheafAddCommGroup, compLeft, smoothSheafAddGroup, smoothSheafCommGroup, compLeft, smoothSheafCommRing, coeFun, eval, evalAt, evalHom, forgetStalk, smoothSheafGroup, smoothSheafRing	30
Theorems instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing, instNontrivialStalkPresheafSmoothSheaf, contMDiff_section, eval_germ, eval_surjective, obj_eq, ι_evalHom, ι_evalHom_apply, ι_evalHom_assoc, evalHom_germ, eval_germ, eval_surjective, forgetStalk_hom_comp_evalHom, forgetStalk_hom_comp_evalHom_apply, forgetStalk_hom_comp_evalHom_assoc, forgetStalk_inv_comp_eval, forgetStalk_inv_comp_eval_apply, forgetStalk_inv_comp_eval_assoc, ι_evalHom, ι_evalHom_apply, ι_evalHom_assoc, ι_forgetStalk_hom, ι_forgetStalk_hom_apply, ι_forgetStalk_hom_assoc, ι_forgetStalk_inv, ι_forgetStalk_inv_apply, ι_forgetStalk_inv_assoc	27
Total	57

(root)

Definitions

Name	Category	Theorems
instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
instCommRingObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf 📖	CompOp	—
smoothPresheafAddCommGroup 📖	CompOp	—
smoothPresheafAddGroup 📖	CompOp	—
smoothPresheafCommGroup 📖	CompOp	—
smoothPresheafCommRing 📖	CompOp	—
smoothPresheafGroup 📖	CompOp	—
smoothPresheafRing 📖	CompOp	—
smoothSheaf 📖	CompOp	19 math math: smoothSheafCommRing.ι_forgetStalk_inv, smoothSheaf.ι_evalHom_apply, smoothSheaf.ι_evalHom_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval, smoothSheafCommRing.forgetStalk_inv_comp_eval_apply, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc, smoothSheafCommRing.ι_forgetStalk_inv_apply, smoothSheaf.obj_eq, smoothSheafCommRing.forgetStalk_hom_comp_evalHom, smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheaf.eval_germ, instNontrivialStalkPresheafSmoothSheaf, smoothSheafCommRing.ι_forgetStalk_hom_apply, smoothSheafCommRing.ι_forgetStalk_hom_assoc, smoothSheaf.ι_evalHom, smoothSheafCommRing.ι_forgetStalk_hom, smoothSheaf.eval_surjective, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply
smoothSheafAddCommGroup 📖	CompOp	—
smoothSheafAddGroup 📖	CompOp	—
smoothSheafCommGroup 📖	CompOp	—
smoothSheafCommRing 📖	CompOp	22 math math: smoothSheafCommRing.ι_forgetStalk_inv, instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing, smoothSheafCommRing.nonunits_stalk, smoothSheafCommRing.ι_evalHom_apply, smoothSheafCommRing.eval_germ, smoothSheafCommRing.instLocalRing_stalk, smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval, smoothSheafCommRing.forgetStalk_inv_comp_eval_apply, smoothSheafCommRing.isUnit_stalk_iff, smoothSheafCommRing.ι_evalHom, smoothSheafCommRing.evalHom_germ, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc, smoothSheafCommRing.ι_forgetStalk_inv_apply, smoothSheafCommRing.eval_surjective, smoothSheafCommRing.forgetStalk_hom_comp_evalHom, smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheafCommRing.ι_forgetStalk_hom_apply, smoothSheafCommRing.ι_forgetStalk_hom_assoc, smoothSheafCommRing.ι_evalHom_assoc, smoothSheafCommRing.ι_forgetStalk_hom, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply
smoothSheafGroup 📖	CompOp	—
smoothSheafRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing 📖	mathematical	—	Nontrivial CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing	—	Function.Surjective.nontrivial CommRingCat.Colimits.hasColimits_commRingCat smoothSheafCommRing.eval_surjective
instNontrivialStalkPresheafSmoothSheaf 📖	mathematical	—	Nontrivial TopCat.Presheaf.stalk CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.of TopCat.Sheaf.presheaf smoothSheaf	—	Function.Surjective.nontrivial CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf.eval_surjective

smoothSheaf

Definitions

Name	Category	Theorems
coeFun 📖	CompOp	—
eval 📖	CompOp	2 math math: eval_germ, eval_surjective
evalAt 📖	CompOp	3 math math: ι_evalHom_apply, ι_evalHom_assoc, ι_evalHom
evalHom 📖	CompOp	9 math math: ι_evalHom_apply, ι_evalHom_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval, smoothSheafCommRing.forgetStalk_inv_comp_eval_apply, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc, smoothSheafCommRing.forgetStalk_hom_comp_evalHom, ι_evalHom, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_section 📖	mathematical	—	ContMDiff TopCat.carrier TopCat.of TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace WithTop.some ENat Top.top instTopENat TopCat.PrelocalPredicate.pred TopCat.LocalPredicate.toPrelocalPredicate StructureGroupoid.LocalInvariantProp.localPredicate contDiffGroupoid ContDiffWithinAtProp	—	StructureGroupoid.LocalInvariantProp.section_spec contDiffWithinAt_localInvariantProp
eval_germ 📖	mathematical	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	eval TopCat.Presheaf.germ CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.of TopCat.Sheaf.presheaf smoothSheaf TopCat.PrelocalPredicate.pred TopCat.LocalPredicate.toPrelocalPredicate StructureGroupoid.LocalInvariantProp.localPredicate contDiffGroupoid WithTop.some ENat Top.top instTopENat ContDiffWithinAtProp Opposite.unop TopCat.carrier TopCat.str Opposite.op	—	TopCat.stalkToFiber_germ contDiffWithinAt_localInvariantProp
eval_surjective 📖	mathematical	—	TopCat.Presheaf.stalk CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.of TopCat.Sheaf.presheaf smoothSheaf eval	—	TopCat.stalkToFiber_surjective contMDiff_const
obj_eq 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.of TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types TopCat.Sheaf.presheaf smoothSheaf ContMDiffMap SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace WithTop.some ENat Top.top instTopENat	—	—
ι_evalHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite TopologicalSpace.OpenNhds TopCat.of CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Sheaf.val Opens.grothendieckTopology smoothSheaf CategoryTheory.Limits.colimit CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CategoryTheory.Limits.colimit.ι evalHom evalAt Opposite.unop	—	CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self
ι_evalHom_apply 📖	mathematical	—	evalHom CategoryTheory.Limits.colimit.ι Opposite TopologicalSpace.OpenNhds TopCat.of CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CategoryTheory.types CategoryTheory.Functor.comp TopologicalSpace.Opens TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Sheaf.val Opens.grothendieckTopology smoothSheaf CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self TopCat.carrier TopCat.str evalAt Opposite.unop	—	CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_evalHom
ι_evalHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology smoothSheaf TopologicalSpace.OpenNhds TopCat.of TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self TopCat.carrier TopCat.str CategoryTheory.Limits.colimit.ι evalHom evalAt Opposite.unop	—	CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_evalHom

smoothSheafAddCommGroup

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	—

smoothSheafCommGroup

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	—

smoothSheafCommRing

Definitions

Name	Category	Theorems
coeFun 📖	CompOp	—
eval 📖	CompOp	4 math math: nonunits_stalk, eval_germ, isUnit_stalk_iff, eval_surjective
evalAt 📖	CompOp	3 math math: ι_evalHom_apply, ι_evalHom, ι_evalHom_assoc
evalHom 📖	CompOp	10 math math: ι_evalHom_apply, forgetStalk_inv_comp_eval_assoc, forgetStalk_inv_comp_eval, forgetStalk_inv_comp_eval_apply, ι_evalHom, evalHom_germ, forgetStalk_hom_comp_evalHom_assoc, forgetStalk_hom_comp_evalHom, ι_evalHom_assoc, forgetStalk_hom_comp_evalHom_apply
forgetStalk 📖	CompOp	12 math math: ι_forgetStalk_inv, forgetStalk_inv_comp_eval_assoc, forgetStalk_inv_comp_eval, forgetStalk_inv_comp_eval_apply, forgetStalk_hom_comp_evalHom_assoc, ι_forgetStalk_inv_apply, forgetStalk_hom_comp_evalHom, ι_forgetStalk_inv_assoc, ι_forgetStalk_hom_apply, ι_forgetStalk_hom_assoc, ι_forgetStalk_hom, forgetStalk_hom_comp_evalHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalHom_germ 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.of SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.Sheaf.presheaf smoothSheafCommRing CommRingCat.of CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier evalHom CategoryTheory.Functor.obj Opposite TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ TopCat.PrelocalPredicate.pred TopCat.LocalPredicate.toPrelocalPredicate StructureGroupoid.LocalInvariantProp.localPredicate contDiffGroupoid WithTop.some ENat Top.top instTopENat ContDiffWithinAtProp Opposite.unop	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat ι_evalHom
eval_germ 📖	mathematical	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe RingHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike eval CategoryTheory.Functor.obj Opposite TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.germ TopCat.PrelocalPredicate.pred TopCat.LocalPredicate.toPrelocalPredicate StructureGroupoid.LocalInvariantProp.localPredicate contDiffGroupoid WithTop.some ENat Top.top instTopENat ContDiffWithinAtProp Opposite.unop	—	evalHom_germ
eval_surjective 📖	mathematical	—	CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike eval	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CommRingCat.Colimits.hasColimits_commRingCat smoothSheaf.eval_surjective forgetStalk_inv_comp_eval_apply
forgetStalk_hom_comp_evalHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf CategoryTheory.Iso.hom forgetStalk smoothSheaf.evalHom DFunLike.coe CommRingCat.of CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier evalHom	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self forgetStalk_inv_comp_eval
forgetStalk_hom_comp_evalHom_apply 📖	mathematical	—	smoothSheaf.evalHom CategoryTheory.Iso.hom CategoryTheory.types CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf forgetStalk DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CommRingCat.of evalHom	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise forgetStalk_hom_comp_evalHom
forgetStalk_hom_comp_evalHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf CategoryTheory.Iso.hom forgetStalk smoothSheaf.evalHom DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CommRingCat.of evalHom	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' forgetStalk_hom_comp_evalHom
forgetStalk_inv_comp_eval 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types TopCat.Presheaf.stalk CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.of TopCat.Sheaf.presheaf smoothSheaf CommRingCat.carrier CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat smoothSheafCommRing CommRingCat.of CategoryTheory.Iso.inv forgetStalk DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom evalHom smoothSheaf.evalHom	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small ι_forgetStalk_inv_assoc smoothSheaf.ι_evalHom CategoryTheory.types_ext CategoryTheory.congr_fun ι_evalHom
forgetStalk_inv_comp_eval_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CommRingCat.of evalHom CategoryTheory.Iso.inv CategoryTheory.types CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf forgetStalk smoothSheaf.evalHom	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise forgetStalk_inv_comp_eval
forgetStalk_inv_comp_eval_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types TopCat.Presheaf.stalk CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self TopCat.of TopCat.Sheaf.presheaf smoothSheaf CommRingCat.carrier CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat smoothSheafCommRing CategoryTheory.Iso.inv forgetStalk DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CommRingCat.of evalHom smoothSheaf.evalHom	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' forgetStalk_inv_comp_eval
ι_evalHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.OpenNhds TopCat.of CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CommRingCat.of CategoryTheory.Limits.colimit.ι evalHom evalAt Opposite.unop	—	CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat
ι_evalHom_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Limits.colimit Opposite TopologicalSpace.OpenNhds TopCat.of CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor CategoryTheory.Functor.category TopCat.carrier TopCat.str CategoryTheory.Functor.whiskeringLeft Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CommRingCat.of evalHom Opposite.op Opposite.unop CategoryTheory.Limits.colimit.ι evalAt	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_evalHom
ι_evalHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Sheaf.presheaf TopCat.of smoothSheafCommRing TopologicalSpace.OpenNhds TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor CategoryTheory.Functor.category TopCat.carrier TopCat.str CategoryTheory.Functor.whiskeringLeft CategoryTheory.Limits.colimit.ι CommRingCat.of evalHom evalAt Opposite.unop	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_evalHom
ι_forgetStalk_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.of TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory TopCat.Sheaf.presheaf smoothSheafCommRing Opposite.op TopologicalSpace.OpenNhds TopologicalSpace.OpenNhds.partialOrder TopologicalSpace.OpenNhds.inclusion Opposite.unop CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.stalk CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom forgetStalk CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small	—	CategoryTheory.ι_preservesColimitIso_hom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CommRingCat.Colimits.hasColimits_commRingCat
ι_forgetStalk_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf forgetStalk DFunLike.coe RingHom CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopologicalSpace.OpenNhds TopologicalSpace.OpenNhds.partialOrder TopologicalSpace.OpenNhds.inclusion Opposite.unop CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.carrier TopCat.str Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Limits.colimit.ι CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_forgetStalk_hom
ι_forgetStalk_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory TopCat.Sheaf.presheaf TopCat.of smoothSheafCommRing Opposite.op TopologicalSpace.OpenNhds TopologicalSpace.OpenNhds.partialOrder TopologicalSpace.OpenNhds.inclusion Opposite.unop CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CommRingCat.Colimits.hasColimits_commRingCat TopCat.carrier TopCat.str DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Limits.colimit.ι TopCat.Presheaf.stalk CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf CategoryTheory.Iso.hom forgetStalk CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_forgetStalk_hom
ι_forgetStalk_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite TopologicalSpace.OpenNhds TopCat.of CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion TopCat.Sheaf.presheaf smoothSheaf CategoryTheory.Limits.colimit CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat smoothSheafCommRing CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv CategoryTheory.Limits.Types.hasColimitsOfSize forgetStalk DFunLike.coe CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfSize CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Iso.comp_inv_eq ι_forgetStalk_hom
ι_forgetStalk_inv_apply 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat TopCat.of TopCat.Sheaf.presheaf smoothSheafCommRing CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self smoothSheaf forgetStalk CategoryTheory.Limits.colimit.ι Opposite TopologicalSpace.OpenNhds CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.comp TopologicalSpace.Opens TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small TopCat.carrier TopCat.str DFunLike.coe RingHom CategoryTheory.Functor.obj Opposite.op Opposite.unop CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise ι_forgetStalk_inv
ι_forgetStalk_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Sheaf.presheaf TopCat.of smoothSheaf TopologicalSpace.OpenNhds TopologicalSpace.OpenNhds.partialOrder CategoryTheory.Functor.op TopologicalSpace.OpenNhds.inclusion CategoryTheory.Limits.colimit CategoryTheory.Functor.comp CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self TopCat.carrier TopCat.str CategoryTheory.Limits.colimit.ι CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat smoothSheafCommRing CategoryTheory.Iso.inv CategoryTheory.Limits.Types.hasColimitsOfSize forgetStalk DFunLike.coe RingHom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.Types.hasColimit Opposite.small UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfSize CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_forgetStalk_inv

---

← Back to Index