Stalks

📁 Source: Mathlib/Geometry/RingedSpace/Stalks.lean

Statistics

Metric	Count
Definitions stalkMap, restrictStalkIso, stalkIso	3
Theorems ofRestrict_stalkMap_isIso, restrictStalkIso_hom_eq_germ, restrictStalkIso_hom_eq_germ_apply, restrictStalkIso_hom_eq_germ_assoc, restrictStalkIso_inv_eq_germ, restrictStalkIso_inv_eq_germ_apply, restrictStalkIso_inv_eq_germ_assoc, restrictStalkIso_inv_eq_ofRestrict, comp, congr_hom, congr_point, id, isIso, stalkSpecializes_stalkMap, stalkSpecializes_stalkMap_apply, stalkSpecializes_stalkMap_assoc, stalkMap_germ, stalkMap_germ_apply, stalkMap_germ_assoc	19
Total	22

AlgebraicGeometry.PresheafedSpace

Definitions

Name	Category	Theorems
restrictStalkIso 📖	CompOp	7 math math: restrictStalkIso_hom_eq_germ, restrictStalkIso_inv_eq_germ_apply, restrictStalkIso_hom_eq_germ_apply, restrictStalkIso_inv_eq_germ, restrictStalkIso_inv_eq_ofRestrict, restrictStalkIso_hom_eq_germ_assoc, restrictStalkIso_inv_eq_germ_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofRestrict_stalkMap_isIso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.IsIso TopCat.Presheaf.stalk carrier presheaf DFunLike.coe restrict TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base ofRestrict Hom.stalkMap	—	restrictStalkIso_inv_eq_ofRestrict CategoryTheory.Iso.isIso_inv
restrictStalkIso_hom_eq_germ 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier restrict TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopCat.Presheaf.germ CategoryTheory.Iso.hom restrictStalkIso Topology.IsOpenEmbedding.functor Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike	—	CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
restrictStalkIso_hom_eq_germ_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe TopCat.Presheaf.stalk CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder carrier CategoryTheory.Functor.op Topology.IsOpenEmbedding.functor presheaf ContinuousMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier restrict CategoryTheory.Iso.hom restrictStalkIso CategoryTheory.Functor.obj Opposite.op TopCat.Presheaf.germ Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise restrictStalkIso_hom_eq_germ
restrictStalkIso_hom_eq_germ_assoc 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier restrict TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk TopCat.Presheaf.germ DFunLike.coe ContinuousMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom restrictStalkIso Topology.IsOpenEmbedding.functor Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictStalkIso_hom_eq_germ
restrictStalkIso_inv_eq_germ 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op Topology.IsOpenEmbedding.functor TopCat.Presheaf.stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier restrict TopCat.Presheaf.germ Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike CategoryTheory.Iso.inv restrictStalkIso	—	restrictStalkIso_hom_eq_germ CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
restrictStalkIso_inv_eq_germ_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe TopCat.Presheaf.stalk carrier presheaf ContinuousMap TopCat.carrier TopCat.str CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op Topology.IsOpenEmbedding.functor restrict CategoryTheory.Iso.inv restrictStalkIso CategoryTheory.Functor.obj Opposite.op TopCat.Presheaf.germ Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise restrictStalkIso_inv_eq_germ
restrictStalkIso_inv_eq_germ_assoc 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op Topology.IsOpenEmbedding.functor TopCat.Presheaf.stalk DFunLike.coe ContinuousMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopCat.Presheaf.germ Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike restrict CategoryTheory.Iso.inv restrictStalkIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictStalkIso_inv_eq_germ
restrictStalkIso_inv_eq_ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Iso.inv TopCat.Presheaf.stalk carrier restrict presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier restrictStalkIso Hom.stalkMap ofRestrict	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape Set.image_preimage_subset CategoryTheory.Iso.comp_inv_eq CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.colimit.ι_map_assoc CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.Limits.colimit.w
stalkMap_germ 📖	mathematical	TopCat.carrier carrier TopologicalSpace.Opens instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base TopCat.Presheaf.germ Hom.stalkMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app Hom.c TopologicalSpace.Opens.map	—	Hom.stalkMap.eq_1 TopCat.Presheaf.stalkFunctor_map_germ_assoc TopCat.Presheaf.stalkPushforward_germ
stalkMap_germ_apply 📖	mathematical	TopCat.carrier carrier TopologicalSpace.Opens instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base	DFunLike.coe TopCat.Presheaf.stalk carrier presheaf ContinuousMap TopCat.carrier TopCat.str CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base Hom.stalkMap CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ TopologicalSpace.Opens.map TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app Hom.c	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkMap_germ
stalkMap_germ_assoc 📖	mathematical	TopCat.carrier carrier TopologicalSpace.Opens instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk DFunLike.coe ContinuousMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Hom.base TopCat.Presheaf.germ Hom.stalkMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app Hom.c TopologicalSpace.Opens.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_germ

AlgebraicGeometry.PresheafedSpace.Hom

Definitions

Name	Category	Theorems
stalkMap 📖	CompOp	29 math math: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.PresheafedSpace.stalkMap.congr, AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.PresheafedSpace.stalkMap.id, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.PresheafedSpace.stalkMap.isIso, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point

AlgebraicGeometry.PresheafedSpace.stalkMap

Definitions

Name	Category	Theorems
stalkIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.map_id CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_pre_assoc
congr_hom 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.eqToHom	—	congr CategoryTheory.eqToHom_refl CategoryTheory.Category.comp_id
congr_point 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.eqToHom	—	congr
id 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.CategoryStruct.id AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf	—	TopCat.Presheaf.stalk_hom_ext TopCat.Presheaf.stalkPushforward.id TopCat.Presheaf.stalkFunctor_map_germ_assoc AlgebraicGeometry.PresheafedSpace.id_c_app CategoryTheory.Functor.map_id TopCat.Presheaf.stalkFunctor_map_germ CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
isIso 📖	mathematical	—	CategoryTheory.IsIso TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	CategoryTheory.IsIso.hom_inv_id AlgebraicGeometry.PresheafedSpace.id_base TopCat.id_app CategoryTheory.Category.assoc congr_point comp CategoryTheory.IsIso.inv_hom_id congr_hom id CategoryTheory.eqToHom_trans_assoc CategoryTheory.eqToHom_refl CategoryTheory.Category.id_comp
stalkSpecializes_stalkMap 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.base TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier	—	ContinuousMap.map_specializes CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.pre_desc CategoryTheory.Limits.colimit.map_desc CategoryTheory.Limits.colimit.ι_desc
stalkSpecializes_stalkMap_apply 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier	DFunLike.coe TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.ConcreteCategory.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes	—	ContinuousMap.map_specializes CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkSpecializes_stalkMap
stalkSpecializes_stalkMap_assoc 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.base TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	ContinuousMap.map_specializes CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkSpecializes_stalkMap

---

← Back to Index