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 presheaf restrict 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 restrict CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk TopCat.Presheaf.germ CategoryTheory.Iso.hom restrictStalkIso IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize Topology.IsOpenEmbedding.isOpenMap
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	TopCat.Presheaf.stalk CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op IsOpenMap.functor presheaf CategoryTheory.Iso.hom restrictStalkIso CategoryTheory.Functor.obj Opposite.op TopCat.Presheaf.germ Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	Topology.IsOpenEmbedding.isOpenMap 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 restrict CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk TopCat.Presheaf.germ CategoryTheory.Iso.hom restrictStalkIso IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	Topology.IsOpenEmbedding.isOpenMap 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 CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.stalk restrict TopCat.Presheaf.germ Set Set.instMembership SetLike.coe CategoryTheory.Iso.inv restrictStalkIso	—	Topology.IsOpenEmbedding.isOpenMap 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	TopCat.Presheaf.stalk presheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op IsOpenMap.functor CategoryTheory.Iso.inv restrictStalkIso CategoryTheory.Functor.obj Opposite.op Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.germ Set Set.instMembership SetLike.coe	—	Topology.IsOpenEmbedding.isOpenMap 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 CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.stalk TopCat.Presheaf.germ Set Set.instMembership SetLike.coe restrict CategoryTheory.Iso.inv restrictStalkIso	—	Topology.IsOpenEmbedding.isOpenMap 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 restrict presheaf restrictStalkIso Hom.stalkMap ofRestrict	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape Topology.IsOpenEmbedding.isOpenMap 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 CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk 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	TopCat.Presheaf.stalk presheaf Hom.stalkMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ TopologicalSpace.Opens.map CategoryTheory.NatTrans.app TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward 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 CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.stalk 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	27 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.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.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.stalkPushforward.id CategoryTheory.Functor.map_comp TopCat.Presheaf.ext CategoryTheory.Category.id_comp CategoryTheory.Functor.map_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.presheaf DFunLike.coe ContinuousMap 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.presheaf ContinuousMap 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.presheaf DFunLike.coe ContinuousMap 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