Terminal

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

Statistics

Metric	Count
Definitions HasInitial, HasTerminal, colimitConstInitial, colimitOfInitial, colimitOfTerminal, initial, to, initialComparison, initialIsInitial, initialIsoIsInitial, limitConstTerminal, limitOfInitial, limitOfTerminal, terminal, from, terminalComparison, terminalIsTerminal, terminalIsoIsTerminal, uniqueFromInitial, uniqueToTerminal, «term⊤__», «term⊥__»	22
Theorems of_initial, of_terminal, hasInitial, hasTerminal, colimitConstInitial_inv, hasColimit_of_domain_hasInitial, hasColimit_of_domain_hasTerminal, hasInitialChangeDiagram, hasInitialChangeUniverse, hasInitial_of_hasTerminal_op, hasInitial_of_unique, hasInitial_op_of_hasTerminal, hasLimit_of_domain_hasInitial, hasLimit_of_domain_hasTerminal, hasTerminalChangeDiagram, hasTerminalChangeUniverse, hasTerminal_of_hasInitial_op, hasTerminal_of_unique, hasTerminal_op_of_hasInitial, hom_ext, hom_ext_iff, isSplitEpi_to, mono_from, to_comp, to_comp_assoc, initialIsoIsInitial_hom, initialIsoIsInitial_inv, instHasColimitObjFunctorConstInitial, instHasLimitObjFunctorConstTerminal, isIso_ι_initial, isIso_ι_of_isInitial, isIso_ι_of_isTerminal, isIso_ι_terminal, isIso_π_initial, isIso_π_of_isInitial, isIso_π_of_isTerminal, isIso_π_terminal, limitConstTerminal_hom, limitConstTerminal_inv_π, limitConstTerminal_inv_π_assoc, comp_from, comp_from_assoc, hom_ext, hom_ext_iff, isSplitMono_from, terminalIsoIsTerminal_hom, terminalIsoIsTerminal_inv, ι_colimitConstInitial_hom, ι_colimitConstInitial_hom_assoc	49
Total	71

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasInitial 📖	MathDef	27 math math: CategoryTheory.hasInitial_of_equivalence, CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers, CategoryTheory.Grp.instHasInitial, CategoryTheory.Factorisation.instHasInitial, CategoryTheory.CategoryOfElements.instHasInitialElementsOppositeOfIsRepresentable, AugmentedSimplexCategory.instHasInitial, CategoryTheory.Equivalence.hasInitial_iff, Preorder.instHasInitialOfOrderBot, hasInitial_of_unique, AlgebraicGeometry.instHasInitialScheme, CategoryTheory.Bicategory.HasLeftKanLift.hasInitial, CategoryTheory.WithInitial.instHasInitial, IsInitial.hasInitial, CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow, CategoryTheory.CategoryOfElements.instHasInitialElementsOfIsCorepresentable, CategoryTheory.Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension, hasInitial_of_hasInitial_of_preservesColimit, CategoryTheory.Bicategory.HasLeftKanExtension.hasInitial, CategoryTheory.CommGrp.instHasInitial, hasColimit_iff_hasInitial_cocone, CategoryTheory.Bicategory.instHasInitialLeftLiftOfHasLeftKanLift, CategoryTheory.CommMon.instHasInitial, hasInitial_of_hasTerminal_op, HasZeroObject.hasInitial, CategoryTheory.hasInitial_of_isCoseparating, hasInitial_op_of_hasTerminal, CategoryTheory.Mon.instHasInitial
HasTerminal 📖	MathDef	25 math math: CategoryTheory.Over.instHasTerminal, hasLimit_iff_hasTerminal_cone, CategoryTheory.Equivalence.hasTerminal_iff, CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities, SimplexCategory.instHasTerminal, HasZeroObject.hasTerminal, hasTerminal_of_hasInitial_op, CategoryTheory.CostructuredArrow.hasTerminal, CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow, CategoryTheory.Cat.instHasTerminal, CategoryTheory.Comon.instHasTerminal, Preorder.instHasTerminalOfOrderTop, CategoryTheory.hasTerminal_of_isSeparating, CategoryTheory.PreGaloisCategory.hasTerminal, hasTerminal_of_unique, hasTerminal_of_hasTerminal_of_preservesLimit, CategoryTheory.Over.over_hasTerminal, FormalCoproduct.instHasTerminal, AlgebraicGeometry.instHasTerminalScheme, CategoryTheory.WithTerminal.instHasTerminal, CategoryTheory.Factorisation.instHasTerminal, hasTerminal_op_of_hasInitial, CategoryTheory.Classifier.SubobjectRepresentableBy.hasTerminal, IsTerminal.hasTerminal, CategoryTheory.hasTerminal_of_equivalence
colimitConstInitial 📖	CompOp	3 math math: colimitConstInitial_inv, ι_colimitConstInitial_hom, ι_colimitConstInitial_hom_assoc
colimitOfInitial 📖	CompOp	—
colimitOfTerminal 📖	CompOp	—
initial 📖	CompOp	57 math math: initialMul_inv, CategoryTheory.Initial.mono_to, CategoryTheory.to_initial_isIso, inl_coprodIsoPushout_hom, initialIsoIsInitial_hom, CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan, CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_apply, CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply, CategoryTheory.Functor.initial_const_initial, CategoryTheory.Subobject.bot_eq_initial_to, CategoryTheory.isPullback_of_cofan_isVanKampen, instHasColimitObjFunctorConstInitial, coprod.leftUnitor_hom, inr_coprodIsoPushout_hom_assoc, initialIsoIsInitial_inv, CategoryTheory.WithInitial.starIsoInitial_inv, initial.mono_from, CategoryTheory.MonoOver.bot_left, initial.isSplitEpi_to, CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen, initial.to_comp_assoc, mulInitial_inv, coprod.leftUnitor_inv, isIso_ι_initial, PreservesInitial.iso_hom, CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι, CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom, HasZeroObject.zeroIsoInitial_inv, instIsIsoInitialComparison, HomotopicalAlgebra.isCofibrant_iff, colimitConstInitial_inv, coprod.rightUnitor_inv, inr_coprodIsoPushout_hom, CategoryTheory.IsPushout.of_hasBinaryCoproduct', coprod.rightUnitor_hom, CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom, initial_isIso_to, initialMul_hom, coprod.triangle, inl_coprodIsoPushout_inv, CategoryTheory.WithInitial.starIsoInitial_hom, CategoryTheory.MonoOver.initialTo_b_eq_zero, ι_colimitConstInitial_hom, inr_coprodIsoPushout_inv, inl_coprodIsoPushout_hom_assoc, isIso_π_initial, mulInitial_hom, inl_coprodIsoPushout_inv_assoc, CategoryTheory.FinitaryExtensive.isPullback_initial_to, inr_coprodIsoPushout_inv_assoc, AlgebraicGeometry.initial_isEmpty, HasZeroObject.zeroIsoInitial_hom, initial.to_comp, CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen, initial.subsingleton_to, ι_colimitConstInitial_hom_assoc, SSet.instFiniteInitial
initialComparison 📖	CompOp	2 math math: PreservesInitial.iso_hom, instIsIsoInitialComparison
initialIsInitial 📖	CompOp	2 math math: initialIsoIsInitial_hom, CategoryTheory.WithInitial.starIsoInitial_inv
initialIsoIsInitial 📖	CompOp	2 math math: initialIsoIsInitial_hom, initialIsoIsInitial_inv
limitConstTerminal 📖	CompOp	3 math math: limitConstTerminal_inv_π_assoc, limitConstTerminal_hom, limitConstTerminal_inv_π
limitOfInitial 📖	CompOp	—
limitOfTerminal 📖	CompOp	—
terminal 📖	CompOp	108 math math: prod.rightUnitor_hom, isIso_ι_terminal, terminal.subsingleton_to, skyscraperPresheaf_obj, prodIsoPullback_inv_fst, CategoryTheory.Dial.tensorUnit_src, CategoryTheory.Dial.rightUnitor_hom_f, CategoryTheory.Dial.rightUnitorImpl_inv_f, prod.rightUnitor_hom_naturality, prod.rightUnitor_hom_naturality_assoc, limitConstTerminal_inv_π_assoc, skyscraperPresheafCocone_pt, prod.rightUnitor_inv, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, PreservesTerminal.iso_hom, prodIsoPullback_inv_fst_assoc, isIso_π_terminal, HasZeroObject.zeroIsoTerminal_inv, instIsIsoTerminalComparison, limitConstTerminal_hom, CategoryTheory.Dial.leftUnitor_hom_f, HasZeroObject.zeroIsoTerminal_hom, CategoryTheory.Dial.rightUnitor_hom_F, AlgebraicGeometry.instIsOverTerminalScheme, CategoryTheory.Dial.rightUnitorImpl_inv_F, prodIsoPullback_hom_fst_assoc, terminal.isSplitMono_from, prod.leftUnitor_inv_naturality_assoc, SSet.Augmented.stdSimplex_map_right, prod_rightUnitor_inv_naturality_assoc, prod.leftUnitor_hom_naturality_assoc, CategoryTheory.Dial.rightUnitorImpl_hom_F, CategoryTheory.monoOver_terminal_to_subterminals_comp, prod.leftUnitor_inv, CategoryTheory.Dial.leftUnitor_inv_f, AlgebraicGeometry.instSubsingletonOverTerminalScheme, limitConstTerminal_inv_π, AlgebraicGeometry.compactSpace_iff_quasiCompact, prod.triangle, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, CategoryTheory.monoidalOfHasFiniteProducts.tensorUnit, CategoryTheory.Dial.rightUnitor_inv_f, CategoryTheory.Dial.tensorUnitImpl_src, terminal.comp_from, SSet.Augmented.stdSimplex_obj_right, CategoryTheory.WithTerminal.starIsoTerminal_inv, CategoryTheory.Dial.leftUnitor_hom_F, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, skyscraperPresheafCocone_ι_app, CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_apply, prodIsoPullback_hom_snd, CategoryTheory.WithTerminal.starIsoTerminal_hom, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj, terminalIsoIsTerminal_hom, CategoryTheory.Dial.tensorUnit_rel, prodIsoPullback_hom_snd_assoc, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, prod.leftUnitor_hom, prodIsoPullback_hom_fst, CategoryTheory.CechNerveTerminalFrom.hasWidePullback', CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, SSet.Augmented.stdSimplex_obj_hom_app, Types.instSubsingletonTerminalType, CategoryTheory.Dial.tensorUnit_tgt, AlgebraicGeometry.instIsAffineTerminalScheme, CategoryTheory.Dial.leftUnitorImpl_hom_F, AlgebraicGeometry.Scheme.isSeparated_iff, prodIsoPullback_inv_snd, terminal_isIso_from, CategoryTheory.Functor.final_const_terminal, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.CechNerveTerminalFrom.hasWidePullback, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, SSet.Augmented.stdSimplex_map_left, CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_symm_apply, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.Dial.leftUnitor_inv_F, AlgebraicGeometry.AffineSpace.over_over, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, terminal.comp_from_assoc, HomotopicalAlgebra.isFibrant_iff, CategoryTheory.Dial.leftUnitorImpl_inv_f, CategoryTheory.Dial.rightUnitor_inv_F, AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from, prodIsoPullback_inv_snd_assoc, CategoryTheory.isSubterminal_of_terminal, terminalIsoIsTerminal_inv, CategoryTheory.IsSubterminal.mono_terminal_from, SkyscraperPresheafFunctor.map'_app, CategoryTheory.IsPullback.of_hasBinaryProduct', prod.leftUnitor_inv_naturality, prod.leftUnitor_hom_naturality, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, CategoryTheory.Dial.tensorUnitImpl_rel, CategoryTheory.subterminals_to_monoOver_terminal_comp_forget, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi, CategoryTheory.Dial.leftUnitorImpl_hom_f, CategoryTheory.Dial.rightUnitorImpl_hom_f, instHasLimitObjFunctorConstTerminal, CategoryTheory.Dial.leftUnitorImpl_inv_F, germ_skyscraperPresheafStalkOfSpecializes_hom, prod_rightUnitor_inv_naturality, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, CategoryTheory.Dial.tensorUnitImpl_tgt
terminalComparison 📖	CompOp	3 math math: PreservesTerminal.iso_hom, instIsIsoTerminalComparison, CategoryTheory.monoidalOfHasFiniteProducts.η_eq
terminalIsTerminal 📖	CompOp	5 math math: CategoryTheory.WithTerminal.starIsoTerminal_hom, terminalIsoIsTerminal_inv, SkyscraperPresheafFunctor.map'_app, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app
terminalIsoIsTerminal 📖	CompOp	2 math math: terminalIsoIsTerminal_hom, terminalIsoIsTerminal_inv
uniqueFromInitial 📖	CompOp	—
uniqueToTerminal 📖	CompOp	—
«term⊤__» 📖	CompOp	—
«term⊥__» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitConstInitial_inv 📖	mathematical	—	CategoryTheory.Iso.inv colimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const initial instHasColimitObjFunctorConstInitial colimitConstInitial initial.to	—	instHasColimitObjFunctorConstInitial
hasColimit_of_domain_hasInitial 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	HasColimit	—	—
hasColimit_of_domain_hasTerminal 📖	mathematical	—	HasColimit	—	—
hasInitialChangeDiagram 📖	mathematical	—	HasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Category.comp_id CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
hasInitialChangeUniverse 📖	mathematical	—	HasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	hasInitialChangeDiagram HasColimitsOfShape.has_colimit
hasInitial_of_hasTerminal_op 📖	mathematical	—	HasInitial	—	IsInitial.hasInitial
hasInitial_of_unique 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasInitial	—	—
hasInitial_op_of_hasTerminal 📖	mathematical	—	HasInitial Opposite CategoryTheory.Category.opposite	—	IsInitial.hasInitial
hasLimit_of_domain_hasInitial 📖	mathematical	—	HasLimit	—	—
hasLimit_of_domain_hasTerminal 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	HasLimit	—	—
hasTerminalChangeDiagram 📖	mathematical	—	HasLimit CategoryTheory.Discrete CategoryTheory.discreteCategory	—	CategoryTheory.Category.id_comp CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
hasTerminalChangeUniverse 📖	mathematical	—	HasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory	—	hasTerminalChangeDiagram HasLimitsOfShape.has_limit
hasTerminal_of_hasInitial_op 📖	mathematical	—	HasTerminal	—	IsTerminal.hasTerminal
hasTerminal_of_unique 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	HasTerminal	—	—
hasTerminal_op_of_hasInitial 📖	mathematical	—	HasTerminal Opposite CategoryTheory.Category.opposite	—	IsTerminal.hasTerminal
initialIsoIsInitial_hom 📖	mathematical	—	CategoryTheory.Iso.hom initial initialIsoIsInitial IsInitial.to initialIsInitial	—	—
initialIsoIsInitial_inv 📖	mathematical	—	CategoryTheory.Iso.inv initial initialIsoIsInitial IsInitial.to	—	—
instHasColimitObjFunctorConstInitial 📖	mathematical	—	HasColimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const initial	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id initial.to_comp Unique.instSubsingleton
instHasLimitObjFunctorConstTerminal 📖	mathematical	—	HasLimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const terminal	—	terminal.comp_from CategoryTheory.Category.comp_id Unique.instSubsingleton
isIso_ι_initial 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	initial colimit hasColimit_of_domain_hasInitial colimit.ι	—	isIso_ι_of_isInitial hasColimit_of_domain_hasInitial
isIso_ι_of_isInitial 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	colimit colimit.ι	—	IsInitial.to_self colimit.ι_desc CategoryTheory.inv.congr_simp colimit.hom_ext colimit.ι_desc_assoc CategoryTheory.Category.comp_id colimit.w
isIso_ι_of_isTerminal 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj colimit colimit.ι	—	colimit.ι_desc IsTerminal.from_self CategoryTheory.Functor.map_id colimit.hom_ext colimit.ι_desc_assoc colimit.w CategoryTheory.Category.comp_id
isIso_ι_terminal 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj terminal colimit hasColimit_of_domain_hasTerminal colimit.ι	—	isIso_ι_of_isTerminal hasColimit_of_domain_hasTerminal
isIso_π_initial 📖	mathematical	—	CategoryTheory.IsIso limit hasLimit_of_domain_hasInitial CategoryTheory.Functor.obj initial limit.π	—	isIso_π_of_isInitial hasLimit_of_domain_hasInitial
isIso_π_of_isInitial 📖	mathematical	—	CategoryTheory.IsIso limit CategoryTheory.Functor.obj limit.π	—	limit.hom_ext CategoryTheory.Category.assoc limit.lift_π limit.w CategoryTheory.Category.id_comp IsInitial.to_self CategoryTheory.Functor.map_id
isIso_π_of_isTerminal 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	limit limit.π	—	limit.hom_ext CategoryTheory.Category.assoc limit.lift_π CategoryTheory.Category.id_comp limit.w IsTerminal.from_self CategoryTheory.Functor.map_id CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_id
isIso_π_terminal 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	limit hasLimit_of_domain_hasTerminal terminal limit.π	—	isIso_π_of_isTerminal hasLimit_of_domain_hasTerminal
limitConstTerminal_hom 📖	mathematical	—	CategoryTheory.Iso.hom limit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const terminal instHasLimitObjFunctorConstTerminal limitConstTerminal terminal.from	—	instHasLimitObjFunctorConstTerminal
limitConstTerminal_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct terminal limit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const instHasLimitObjFunctorConstTerminal CategoryTheory.Iso.inv limitConstTerminal limit.π terminal.from	—	instHasLimitObjFunctorConstTerminal Unique.instSubsingleton
limitConstTerminal_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct terminal limit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const instHasLimitObjFunctorConstTerminal CategoryTheory.Iso.inv limitConstTerminal limit.π terminal.from	—	instHasLimitObjFunctorConstTerminal CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitConstTerminal_inv_π
terminalIsoIsTerminal_hom 📖	mathematical	—	CategoryTheory.Iso.hom terminal terminalIsoIsTerminal IsTerminal.from	—	—
terminalIsoIsTerminal_inv 📖	mathematical	—	CategoryTheory.Iso.inv terminal terminalIsoIsTerminal IsTerminal.from terminalIsTerminal	—	—
ι_colimitConstInitial_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const initial colimit instHasColimitObjFunctorConstInitial colimit.ι CategoryTheory.Iso.hom colimitConstInitial initial.to	—	instHasColimitObjFunctorConstInitial Unique.instSubsingleton
ι_colimitConstInitial_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const initial colimit instHasColimitObjFunctorConstInitial colimit.ι CategoryTheory.Iso.hom colimitConstInitial initial.to	—	instHasColimitObjFunctorConstInitial CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitConstInitial_hom

CategoryTheory.Limits.InitialMonoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_initial 📖	mathematical	CategoryTheory.Mono CategoryTheory.Limits.initial CategoryTheory.Limits.initial.to	CategoryTheory.Limits.InitialMonoClass	—	of_isInitial
of_terminal 📖	mathematical	—	CategoryTheory.Limits.InitialMonoClass	—	of_isTerminal

CategoryTheory.Limits.IsInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial	—	CategoryTheory.Category.comp_id CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty

CategoryTheory.Limits.IsTerminal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal	—	CategoryTheory.Category.id_comp CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty

CategoryTheory.Limits.initial

Definitions

Name	Category	Theorems
to 📖	CompOp	32 math math: CategoryTheory.Limits.initialMul_inv, CategoryTheory.Initial.mono_to, inl_coprodIsoPushout_hom, CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan, CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply, CategoryTheory.Subobject.bot_eq_initial_to, CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Limits.coprod.leftUnitor_hom, inr_coprodIsoPushout_hom_assoc, CategoryTheory.MonoOver.bot_arrow, CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen, to_comp_assoc, CategoryTheory.Limits.mulInitial_inv, CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι, CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom, HomotopicalAlgebra.isCofibrant_iff, CategoryTheory.Limits.colimitConstInitial_inv, inr_coprodIsoPushout_hom, CategoryTheory.IsPushout.of_hasBinaryCoproduct', CategoryTheory.Limits.coprod.rightUnitor_hom, CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom, inl_coprodIsoPushout_inv, CategoryTheory.MonoOver.initialTo_b_eq_zero, CategoryTheory.Limits.ι_colimitConstInitial_hom, inr_coprodIsoPushout_inv, inl_coprodIsoPushout_hom_assoc, inl_coprodIsoPushout_inv_assoc, CategoryTheory.FinitaryExtensive.isPullback_initial_to, inr_coprodIsoPushout_inv_assoc, to_comp, CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen, CategoryTheory.Limits.ι_colimitConstInitial_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.colimit.hom_ext
hom_ext_iff 📖	—	—	—	—	hom_ext
isSplitEpi_to 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Limits.initial	—	CategoryTheory.Limits.IsInitial.isSplitEpi_to
mono_from 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.initial	—	CategoryTheory.Limits.IsInitial.mono_from
to_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.initial to	—	Unique.instSubsingleton
to_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.initial to	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' to_comp

CategoryTheory.Limits.terminal

Definitions

Name	Category	Theorems
from 📖	CompOp	47 math math: prodIsoPullback_inv_fst, CategoryTheory.Dial.rightUnitorImpl_inv_f, CategoryTheory.Limits.limitConstTerminal_inv_π_assoc, CategoryTheory.Limits.prod.rightUnitor_inv, prodIsoPullback_inv_fst_assoc, CategoryTheory.Limits.limitConstTerminal_hom, CategoryTheory.Dial.rightUnitor_hom_F, prodIsoPullback_hom_fst_assoc, SSet.Augmented.stdSimplex_map_right, CategoryTheory.Dial.rightUnitorImpl_hom_F, CategoryTheory.Limits.prod.leftUnitor_inv, CategoryTheory.Dial.leftUnitor_inv_f, CategoryTheory.Limits.limitConstTerminal_inv_π, AlgebraicGeometry.compactSpace_iff_quasiCompact, CategoryTheory.Dial.rightUnitor_inv_f, comp_from, CategoryTheory.Dial.leftUnitor_hom_F, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, skyscraperPresheafCocone_ι_app, CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_apply, prodIsoPullback_hom_snd, prodIsoPullback_hom_snd_assoc, prodIsoPullback_hom_fst, CategoryTheory.CechNerveTerminalFrom.hasWidePullback', CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, SSet.Augmented.stdSimplex_obj_hom_app, CategoryTheory.Dial.leftUnitorImpl_hom_F, AlgebraicGeometry.Scheme.isSeparated_iff, prodIsoPullback_inv_snd, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.CechNerveTerminalFrom.hasWidePullback, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, SSet.Augmented.stdSimplex_map_left, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, AlgebraicGeometry.AffineSpace.over_over, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, comp_from_assoc, HomotopicalAlgebra.isFibrant_iff, CategoryTheory.Dial.leftUnitorImpl_inv_f, AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from, prodIsoPullback_inv_snd_assoc, CategoryTheory.IsSubterminal.mono_terminal_from, CategoryTheory.IsPullback.of_hasBinaryProduct', CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_from 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal from	—	Unique.instSubsingleton
comp_from_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal from	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_from
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.limit.hom_ext
hom_ext_iff 📖	—	—	—	—	hom_ext
isSplitMono_from 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Limits.terminal	—	CategoryTheory.Limits.IsTerminal.isSplitMono_from

---

← Back to Index