IsTerminal

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

Statistics

Metric	Count
Definitions IsTerminal, InitialMonoClass, IsInitial, equivOfIso, ofIso, ofUnique, ofUniqueHom, to, uniqueUpToIso, IsTerminal, equivOfIso, from, ofIso, ofUnique, ofUniqueHom, uniqueUpToIso, asEmptyCocone, asEmptyCone, coconeOfDiagramInitial, coconeOfDiagramTerminal, colimitOfDiagramInitial, colimitOfDiagramTerminal, coneOfDiagramInitial, coneOfDiagramTerminal, initialOpOfTerminal, initialUnopOfTerminal, isColimitChangeEmptyCocone, isColimitEmptyCoconeEquiv, isColimitEquivIsInitialOfIsEmpty, isInitialBot, isInitialEquivUnique, isLimitChangeEmptyCone, isLimitEmptyConeEquiv, isLimitEquivIsTerminalOfIsEmpty, isTerminalEquivUnique, isTerminalTop, limitOfDiagramInitial, limitOfDiagramTerminal, terminalOpOfInitial, terminalUnopOfInitial	40
Theorems isInitial_mono_from, of_isInitial, of_isTerminal, isIso_ι_app_of_isTerminal, epi_to, hom_ext, isSplitEpi_to, mono_from, to_comp, to_self, uniqueUpToIso_hom, uniqueUpToIso_inv, isIso_π_app_of_isInitial, comp_from, from_self, hom_ext, isSplitMono_from, mono_from, uniqueUpToIso_hom, uniqueUpToIso_inv, asEmptyCocone_pt, asEmptyCocone_ι_app, asEmptyCone_pt, asEmptyCone_π_app, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app, coconeOfDiagramTerminal_pt, coconeOfDiagramTerminal_ι_app, coneOfDiagramInitial_pt, coneOfDiagramInitial_π_app, coneOfDiagramTerminal_pt, coneOfDiagramTerminal_π_app, isIso_of_isInitial, isIso_of_isTerminal	34
Total	74

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram

Definitions

Name	Category	Theorems
IsTerminal 📖	CompData	1 math math: IsTerminal.instSubsingleton

CategoryTheory.Limits

Definitions

Name	Category	Theorems
InitialMonoClass 📖	CompData	7 math math: initial_mono_of_strict_initial_objects, initialMonoClass_of_coproductsDisjoint, InitialMonoClass.of_isTerminal, InitialMonoClass.of_terminal, HasZeroObject.initialMonoClass, InitialMonoClass.of_initial, InitialMonoClass.of_isInitial
IsInitial 📖	CompOp	8 math math: CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, Types.initial_iff_empty, IsInitial.to_eq_descCoconeMorphism, AlgebraicGeometry.isInitial_iff_isEmpty, IsColimit.descCoconeMorphism_eq_isInitial_to, CoproductDisjoint.nonempty_isInitial_of_ne, Concrete.initial_of_empty_of_reflects, Concrete.initial_iff_empty_of_preserves_of_reflects
IsTerminal 📖	CompOp	9 math math: IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.PreGaloisCategory.isGalois_iff_aux, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal, SkyscraperPresheafFunctor.map'_app, IsTerminal.from_eq_liftConeMorphism, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app
asEmptyCocone 📖	CompOp	3 math math: asEmptyCocone_pt, CategoryTheory.IsInitial.isVanKampenColimit, asEmptyCocone_ι_app
asEmptyCone 📖	CompOp	3 math math: CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, asEmptyCone_pt, asEmptyCone_π_app
coconeOfDiagramInitial 📖	CompOp	2 math math: coconeOfDiagramInitial_ι_app, coconeOfDiagramInitial_pt
coconeOfDiagramTerminal 📖	CompOp	3 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, coconeOfDiagramTerminal_ι_app, coconeOfDiagramTerminal_pt
colimitOfDiagramInitial 📖	CompOp	—
colimitOfDiagramTerminal 📖	CompOp	2 math math: CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit
coneOfDiagramInitial 📖	CompOp	2 math math: coneOfDiagramInitial_π_app, coneOfDiagramInitial_pt
coneOfDiagramTerminal 📖	CompOp	2 math math: coneOfDiagramTerminal_π_app, coneOfDiagramTerminal_pt
initialOpOfTerminal 📖	CompOp	—
initialUnopOfTerminal 📖	CompOp	—
isColimitChangeEmptyCocone 📖	CompOp	—
isColimitEmptyCoconeEquiv 📖	CompOp	—
isColimitEquivIsInitialOfIsEmpty 📖	CompOp	—
isInitialBot 📖	CompOp	—
isInitialEquivUnique 📖	CompOp	—
isLimitChangeEmptyCone 📖	CompOp	—
isLimitEmptyConeEquiv 📖	CompOp	—
isLimitEquivIsTerminalOfIsEmpty 📖	CompOp	—
isTerminalEquivUnique 📖	CompOp	—
isTerminalTop 📖	CompOp	1 math math: CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit
limitOfDiagramInitial 📖	CompOp	—
limitOfDiagramTerminal 📖	CompOp	—
terminalOpOfInitial 📖	CompOp	—
terminalUnopOfInitial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asEmptyCocone_pt 📖	mathematical	—	Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty asEmptyCocone	—	—
asEmptyCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι asEmptyCocone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
asEmptyCone_pt 📖	mathematical	—	Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty asEmptyCone	—	—
asEmptyCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.empty Cone.π asEmptyCone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coconeOfDiagramInitial_pt 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	Cocone.pt coconeOfDiagramInitial	—	—
coconeOfDiagramInitial_ι_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι coconeOfDiagramInitial CategoryTheory.inv IsInitial.to	—	—
coconeOfDiagramTerminal_pt 📖	mathematical	—	Cocone.pt coconeOfDiagramTerminal CategoryTheory.Functor.obj	—	—
coconeOfDiagramTerminal_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι coconeOfDiagramTerminal CategoryTheory.Functor.map IsTerminal.from	—	—
coneOfDiagramInitial_pt 📖	mathematical	—	Cone.pt coneOfDiagramInitial CategoryTheory.Functor.obj	—	—
coneOfDiagramInitial_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.π coneOfDiagramInitial CategoryTheory.Functor.map IsInitial.to	—	—
coneOfDiagramTerminal_pt 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	Cone.pt coneOfDiagramTerminal	—	—
coneOfDiagramTerminal_π_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.π coneOfDiagramTerminal CategoryTheory.inv IsTerminal.from	—	—
isIso_of_isInitial 📖	mathematical	—	CategoryTheory.IsIso	—	IsInitial.to_comp IsInitial.to_self IsInitial.hom_ext
isIso_of_isTerminal 📖	mathematical	—	CategoryTheory.IsIso	—	IsTerminal.comp_from IsTerminal.from_self IsTerminal.hom_ext

CategoryTheory.Limits.InitialMonoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInitial_mono_from 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.IsInitial.to	—	—
of_isInitial 📖	mathematical	CategoryTheory.Mono CategoryTheory.Limits.IsInitial.to	CategoryTheory.Limits.InitialMonoClass	—	CategoryTheory.Limits.IsInitial.hom_ext CategoryTheory.mono_comp CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom
of_isTerminal 📖	mathematical	—	CategoryTheory.Limits.InitialMonoClass	—	of_isInitial CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.IsInitial.hom_ext

CategoryTheory.Limits.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_ι_app_of_isTerminal 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Iso.isIso_hom

CategoryTheory.Limits.IsInitial

Definitions

Name	Category	Theorems
equivOfIso 📖	CompOp	—
ofIso 📖	CompOp	—
ofUnique 📖	CompOp	—
ofUniqueHom 📖	CompOp	—
to 📖	CompOp	50 math math: CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.Under.forgetMapInitial_inv_app, CategoryTheory.WithInitial.liftToInitialUnique_hom_app, CategoryTheory.Under.equivalenceOfIsInitial_counitIso, CategoryTheory.StructuredArrow.IsUniversal.uniq, CategoryTheory.Limits.initialIsoIsInitial_hom, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.Limits.coneOfDiagramInitial_π_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, CategoryTheory.initial_mono, to_eq_descCoconeMorphism, to_self, CategoryTheory.WithInitial.liftStar_lift_map, CategoryTheory.WithInitial.inclLiftToInitial_inv_app, CategoryTheory.WithInitial.mkCommaObject_hom_app, CategoryTheory.Limits.initialIsoIsInitial_inv, CategoryTheory.WithInitial.starIsoInitial_inv, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, to_comp, CategoryTheory.Under.forgetMapInitial_hom_app, CategoryTheory.WithInitial.equivComma_functor_obj_hom_app, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to, CategoryTheory.Under.equivalenceOfIsInitial_unitIso, CategoryTheory.Limits.coconeOfDiagramInitial_ι_app, AlgebraicGeometry.emptyIsInitial_to, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, CategoryTheory.WithInitial.inclLiftToInitial_hom_app, CategoryTheory.Limits.isInitialMul_inv, uniqueUpToIso_inv, CategoryTheory.zeroMul_inv, CategoryTheory.IsPushout.of_is_coproduct, uniqueUpToIso_hom, CategoryTheory.Limits.mulIsInitial_inv, CategoryTheory.WithInitial.starIsoInitial_hom, CategoryTheory.WithInitial.liftToInitial_map, CategoryTheory.Under.equivalenceOfIsInitial_inverse_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, CategoryTheory.Under.mkIdInitial_to_right, CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj, CategoryTheory.IsPushout.of_is_coproduct', CategoryTheory.WithInitial.opEquiv_inverse_map, CategoryTheory.WithInitial.liftToInitialUnique_inv_app, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.opEquiv_functor_map
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_inv, uniqueUpToIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_to 📖	mathematical	—	CategoryTheory.Epi	—	CategoryTheory.IsSplitEpi.epi isSplitEpi_to
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
isSplitEpi_to 📖	mathematical	—	CategoryTheory.IsSplitEpi	—	CategoryTheory.IsSplitEpi.mk' hom_ext
mono_from 📖	mathematical	—	CategoryTheory.Mono	—	hom_ext CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from
to_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct to	—	hom_ext
to_self 📖	mathematical	—	to CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso to	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso to	—	—

CategoryTheory.Limits.IsLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_π_app_of_isInitial 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Iso.isIso_hom

CategoryTheory.Limits.IsTerminal

Definitions

Name	Category	Theorems
equivOfIso 📖	CompOp	—
from 📖	CompOp	54 math math: CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.Over.forgetMapTerminal_hom_app, CategoryTheory.Over.equivalenceOfIsTerminal_counitIso, CategoryTheory.IsSubterminal.mono_isTerminal_from, CategoryTheory.WithInitial.opEquiv_functor_map, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, CategoryTheory.Limits.coneOfDiagramTerminal_π_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, CategoryTheory.WithTerminal.liftToTerminal_map, CategoryTheory.IsPullback.of_is_product', CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map, CategoryTheory.Over.forgetMapTerminal_inv_app, uniqueUpToIso_hom, CategoryTheory.Classifier.isTerminalFrom_eq_χ₀, CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app, CategoryTheory.WithTerminal.lift_map_liftStar, CategoryTheory.WithTerminal.inclLiftToTerminal_inv_app, CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj, CategoryTheory.WithTerminal.equivComma_functor_obj_hom_app, CategoryTheory.WithTerminal.starIsoTerminal_inv, CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app, comp_from, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.starIsoTerminal_hom, CategoryTheory.Limits.terminalIsoIsTerminal_hom, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, uniqueUpToIso_inv, CategoryTheory.WithTerminal.mkCommaObject_hom_app, CategoryTheory.Over.equivalenceOfIsTerminal_unitIso, CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app, AlgebraicGeometry.Scheme.emptyTo_c_app, from_self, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.CostructuredArrow.IsUniversal.uniq, CategoryTheory.Limits.terminalIsoIsTerminal_inv, SkyscraperPresheafFunctor.map'_app, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.Over.mkIdTerminal_from_left, CategoryTheory.constantPresheafAdj_counit_app_app, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, from_eq_liftConeMorphism, CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app, CategoryTheory.IsPullback.of_is_product, CategoryTheory.SemiCartesianMonoidalCategory.snd_def, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, CategoryTheory.WithTerminal.opEquiv_inverse_map
ofIso 📖	CompOp	—
ofUnique 📖	CompOp	—
ofUniqueHom 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_hom, uniqueUpToIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_from 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct from	—	hom_ext
from_self 📖	mathematical	—	from CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
isSplitMono_from 📖	mathematical	—	CategoryTheory.IsSplitMono	—	CategoryTheory.IsSplitMono.mk' hom_ext
mono_from 📖	mathematical	—	CategoryTheory.Mono	—	CategoryTheory.IsSplitMono.mono isSplitMono_from
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso from	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso from	—	—

---

← Back to Index