HasColimits

📁 Source: Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Statistics

Metric	Count
Definitions imageBasicOpen, coequalizer, coequalizerCofork, coequalizerCoforkIsColimit, coproduct, coproductCofan, coproductCofanIsColimit	7
Theorems coequalizer_π_app_isLocalHom, coequalizer_π_stalk_isLocalHom, imageBasicOpen_image_open, imageBasicOpen_image_preimage, instHasCoequalizer, instHasCoequalizers, instHasColimits, instHasColimitsOfShapeDiscrete, instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, isLocalHom_stalkMap_congr, preservesCoequalizer, preservesColimits_forgetToSheafedSpace, colimit_exists_rep, instEpiTopCatBaseHomPresheafedSpaceπ, isColimit_exists_rep	15
Total	22

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
coequalizer 📖	CompOp	—
coequalizerCofork 📖	CompOp	—
coequalizerCoforkIsColimit 📖	CompOp	—
coproduct 📖	CompOp	—
coproductCofan 📖	CompOp	—
coproductCofanIsColimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasCoequalizer 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizer AlgebraicGeometry.LocallyRingedSpace instCategory	—	—
instHasCoequalizers 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizers AlgebraicGeometry.LocallyRingedSpace instCategory	—	CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair instHasCoequalizer
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits AlgebraicGeometry.LocallyRingedSpace instCategory	—	CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts instHasColimitsOfShapeDiscrete UnivLE.small UnivLE.self instHasCoequalizers
instHasColimitsOfShapeDiscrete 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory AlgebraicGeometry.LocallyRingedSpace instCategory	—	—
instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory forgetToSheafedSpace	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Category.comp_id
isLocalHom_stalkMap_congr 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace 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.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom CommRingCat.isLocalHom_comp isLocalHom_of_isIso CategoryTheory.instIsIsoEqToHom
preservesCoequalizer 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory forgetToSheafedSpace	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone HasCoequalizer.coequalizer_π_stalk_isLocalHom CategoryTheory.Limits.preservesColimit_of_iso_diagram
preservesColimits_forgetToSheafedSpace 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory forgetToSheafedSpace	—	CategoryTheory.Limits.preservesColimits_of_preservesCoequalizers_and_coproducts instHasCoequalizers instHasColimitsOfShapeDiscrete UnivLE.small UnivLE.self preservesCoequalizer instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace

AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer

Definitions

Name	Category	Theorems
imageBasicOpen 📖	CompOp	2 math math: imageBasicOpen_image_open, imageBasicOpen_image_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coequalizer_π_app_isLocalHom 📖	mathematical	—	IsLocalHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.Limits.coequalizer AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.parallelPair TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.coequalizer.π RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.ι_comp_coequalizerComparison CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.Limits.PreservesCoequalizer.iso_hom AlgebraicGeometry.PresheafedSpace.comp_c_app CategoryTheory.Limits.hasLimitOfHasLimitsOfShape AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π RingHom.isLocalHom_comp CommRingCat.equalizer_ι_isLocalHom' isLocalHom_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.NatIso.isIso_app_of_isIso AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso
coequalizer_π_stalk_isLocalHom 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.Limits.coequalizer AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.parallelPair 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.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.coequalizer.π RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small TopCat.Presheaf.germ_exist CommRingCat.FilteredColimits.forget_preservesFilteredColimits imageBasicOpen_image_preimage TopologicalSpace.Opens.is_open' SetLike.ext' imageBasicOpen_image_open Set.image_subset_iff AlgebraicGeometry.RingedSpace.basicOpen_le AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply Set.mem_image_of_mem TopCat.Presheaf.germ_res_apply RingHom.isUnit_map isUnit_map_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coequalizer_π_app_isLocalHom CommRingCat.comp_apply CategoryTheory.NatTrans.naturality isLocalHom_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom CategoryTheory.Functor.map_comp AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
imageBasicOpen_image_open 📖	mathematical	—	IsOpen TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.Limits.coequalizer AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.parallelPair AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.coequalizer.π TopologicalSpace.Opens.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat imageBasicOpen	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite Homeomorph.isOpen_preimage TopCat.coequalizer_isOpen_iff Set.preimage_comp TopCat.coe_comp CategoryTheory.Limits.PreservesCoequalizer.iso_hom CategoryTheory.Limits.ι_comp_coequalizerComparison imageBasicOpen_image_preimage TopologicalSpace.Opens.is_open'
imageBasicOpen_image_preimage 📖	mathematical	—	Set.preimage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace CategoryTheory.Limits.coequalizer AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.parallelPair DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.coequalizer.π Set.image TopologicalSpace.Opens.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat imageBasicOpen	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq CategoryTheory.types_ext CategoryTheory.Functor.congr_map CategoryTheory.Limits.coequalizer.condition CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits TopCat.forget_preservesColimits AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen CategoryTheory.ConcreteCategory.comp_apply AlgebraicGeometry.PresheafedSpace.comp_c_app CommRingCat.comp_apply AlgebraicGeometry.SheafedSpace.congr_hom_app AlgebraicGeometry.RingedSpace.basicOpen_res inf_eq_right LE.le.trans AlgebraicGeometry.RingedSpace.basicOpen_le le_refl

AlgebraicGeometry.SheafedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimit_exists_rep 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace instCategory CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.colimit.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.Concrete.isColimit_exists_rep CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite
instEpiTopCatBaseHomPresheafedSpaceπ 📖	mathematical	—	CategoryTheory.Epi TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace CategoryTheory.Limits.coequalizer AlgebraicGeometry.SheafedSpace instCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits Opposite CategoryTheory.Category.opposite CategoryTheory.finCategoryOpposite CategoryTheory.Limits.instFinCategoryWalkingParallelPair CategoryTheory.Limits.parallelPair AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.coequalizer.π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.ι_comp_coequalizerComparison CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.PreservesCoequalizer.iso_hom CategoryTheory.epi_comp CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom
isColimit_exists_rep 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.Concrete.isColimit_exists_rep CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite

---

← Back to Index