Subterminal

📁 Source: Mathlib/CategoryTheory/Subterminal.lean

Statistics

Metric	Count
Definitions IsSubterminal, isoDiag, Subterminals, instCategorySubterminals, instInhabitedSubterminalsOfHasTerminal, subterminalInclusion, subterminalsEquivMonoOverTerminal	7
Theorems def, isIso_diag, isoDiag_hom, isoDiag_inv, mono_isTerminal_from, mono_terminal_from, instFaithfulSubterminalsSubterminalInclusion, instFullSubterminalsSubterminalInclusion, isSubterminal_of_isIso_diag, isSubterminal_of_isTerminal, isSubterminal_of_mono_isTerminal_from, isSubterminal_of_mono_terminal_from, isSubterminal_of_terminal, monoOver_terminal_to_subterminals_comp, subterminalInclusion_map, subterminalInclusion_obj, subterminalsEquivMonoOverTerminal_counitIso, subterminalsEquivMonoOverTerminal_functor_map, subterminalsEquivMonoOverTerminal_functor_obj_obj, subterminalsEquivMonoOverTerminal_inverse_map, subterminalsEquivMonoOverTerminal_inverse_obj_obj, subterminalsEquivMonoOverTerminal_unitIso, subterminals_thin, subterminals_to_monoOver_terminal_comp_forget	24
Total	31

CategoryTheory

Definitions

Name	Category	Theorems
IsSubterminal 📖	MathDef	14 math math: isSubterminal_of_isIso_diag, IsSubterminal.def, subterminalsEquivMonoOverTerminal_inverse_map, isSubterminal_of_isTerminal, isSubterminal_of_mono_terminal_from, subterminalsEquivMonoOverTerminal_inverse_obj_obj, isSubterminal_of_mono_isTerminal_from, subterminalsEquivMonoOverTerminal_functor_map, subterminalsEquivMonoOverTerminal_unitIso, subterminalsEquivMonoOverTerminal_counitIso, isSubterminal_of_terminal, subterminalInclusion_obj, subterminalInclusion_map, subterminalsEquivMonoOverTerminal_functor_obj_obj
Subterminals 📖	CompOp	14 math math: monoOver_terminal_to_subterminals_comp, instFullSubterminalsSubterminalInclusion, instFaithfulSubterminalsSubterminalInclusion, subterminalsEquivMonoOverTerminal_inverse_map, subterminalsEquivMonoOverTerminal_inverse_obj_obj, instExponentialIdealSubterminalsSubterminalInclusion, subterminalsEquivMonoOverTerminal_functor_map, subterminalsEquivMonoOverTerminal_unitIso, subterminalsEquivMonoOverTerminal_counitIso, subterminals_thin, subterminalInclusion_obj, subterminalInclusion_map, subterminalsEquivMonoOverTerminal_functor_obj_obj, subterminals_to_monoOver_terminal_comp_forget
instCategorySubterminals 📖	CompOp	14 math math: monoOver_terminal_to_subterminals_comp, instFullSubterminalsSubterminalInclusion, instFaithfulSubterminalsSubterminalInclusion, subterminalsEquivMonoOverTerminal_inverse_map, subterminalsEquivMonoOverTerminal_inverse_obj_obj, instExponentialIdealSubterminalsSubterminalInclusion, subterminalsEquivMonoOverTerminal_functor_map, subterminalsEquivMonoOverTerminal_unitIso, subterminalsEquivMonoOverTerminal_counitIso, subterminals_thin, subterminalInclusion_obj, subterminalInclusion_map, subterminalsEquivMonoOverTerminal_functor_obj_obj, subterminals_to_monoOver_terminal_comp_forget
instInhabitedSubterminalsOfHasTerminal 📖	CompOp	—
subterminalInclusion 📖	CompOp	7 math math: monoOver_terminal_to_subterminals_comp, instFullSubterminalsSubterminalInclusion, instFaithfulSubterminalsSubterminalInclusion, instExponentialIdealSubterminalsSubterminalInclusion, subterminalInclusion_obj, subterminalInclusion_map, subterminals_to_monoOver_terminal_comp_forget
subterminalsEquivMonoOverTerminal 📖	CompOp	8 math math: monoOver_terminal_to_subterminals_comp, subterminalsEquivMonoOverTerminal_inverse_map, subterminalsEquivMonoOverTerminal_inverse_obj_obj, subterminalsEquivMonoOverTerminal_functor_map, subterminalsEquivMonoOverTerminal_unitIso, subterminalsEquivMonoOverTerminal_counitIso, subterminalsEquivMonoOverTerminal_functor_obj_obj, subterminals_to_monoOver_terminal_comp_forget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSubterminalsSubterminalInclusion 📖	mathematical	—	Functor.Faithful Subterminals instCategorySubterminals subterminalInclusion	—	ObjectProperty.faithful_ι
instFullSubterminalsSubterminalInclusion 📖	mathematical	—	Functor.Full Subterminals instCategorySubterminals subterminalInclusion	—	ObjectProperty.full_ι
isSubterminal_of_isIso_diag 📖	mathematical	—	IsSubterminal	—	cancel_epi epi_of_strongEpi strongEpi_of_isIso Limits.limit.lift_π Limits.prod.lift_fst Limits.prod.lift_snd
isSubterminal_of_isTerminal 📖	mathematical	—	IsSubterminal	—	Limits.IsTerminal.hom_ext
isSubterminal_of_mono_isTerminal_from 📖	mathematical	—	IsSubterminal	—	cancel_mono Limits.IsTerminal.hom_ext
isSubterminal_of_mono_terminal_from 📖	mathematical	—	IsSubterminal	—	cancel_mono Unique.instSubsingleton
isSubterminal_of_terminal 📖	mathematical	—	IsSubterminal Limits.terminal	—	Unique.instSubsingleton
monoOver_terminal_to_subterminals_comp 📖	mathematical	—	Functor.comp MonoOver Limits.terminal ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono Subterminals instCategorySubterminals Equivalence.inverse subterminalsEquivMonoOverTerminal subterminalInclusion MonoOver.forget Over.forget	—	—
subterminalInclusion_map 📖	mathematical	—	Functor.map Subterminals instCategorySubterminals subterminalInclusion InducedCategory.Hom.hom ObjectProperty.FullSubcategory IsSubterminal ObjectProperty.FullSubcategory.obj	—	—
subterminalInclusion_obj 📖	mathematical	—	Functor.obj Subterminals instCategorySubterminals subterminalInclusion ObjectProperty.FullSubcategory.obj IsSubterminal	—	—
subterminalsEquivMonoOverTerminal_counitIso 📖	mathematical	—	Equivalence.counitIso Subterminals MonoOver Limits.terminal instCategorySubterminals ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono subterminalsEquivMonoOverTerminal NatIso.ofComponents Functor.comp IsSubterminal Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit ObjectProperty.FullSubcategory.obj ObjectProperty.homMk CommaMorphism.left InducedCategory.Hom.hom ObjectProperty.FullSubcategory Limits.terminal.from MonoOver.homMk MonoOver.isoMk Functor.obj Iso.refl	—	—
subterminalsEquivMonoOverTerminal_functor_map 📖	mathematical	—	Functor.map Subterminals instCategorySubterminals MonoOver Limits.terminal ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono Equivalence.functor subterminalsEquivMonoOverTerminal MonoOver.homMk ObjectProperty.FullSubcategory.obj IsSubterminal Limits.terminal.from InducedCategory.Hom.hom ObjectProperty.FullSubcategory	—	—
subterminalsEquivMonoOverTerminal_functor_obj_obj 📖	mathematical	—	ObjectProperty.FullSubcategory.obj Over Limits.terminal instCategoryOver Over.isMono Functor.obj Subterminals instCategorySubterminals MonoOver ObjectProperty.FullSubcategory.category Equivalence.functor subterminalsEquivMonoOverTerminal IsSubterminal Limits.terminal.from	—	—
subterminalsEquivMonoOverTerminal_inverse_map 📖	mathematical	—	Functor.map MonoOver Limits.terminal ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono Subterminals instCategorySubterminals Equivalence.inverse subterminalsEquivMonoOverTerminal ObjectProperty.homMk IsSubterminal Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit ObjectProperty.FullSubcategory.obj CommaMorphism.left InducedCategory.Hom.hom ObjectProperty.FullSubcategory	—	—
subterminalsEquivMonoOverTerminal_inverse_obj_obj 📖	mathematical	—	ObjectProperty.FullSubcategory.obj IsSubterminal Functor.obj MonoOver Limits.terminal ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono Subterminals instCategorySubterminals Equivalence.inverse subterminalsEquivMonoOverTerminal Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit	—	—
subterminalsEquivMonoOverTerminal_unitIso 📖	mathematical	—	Equivalence.unitIso Subterminals MonoOver Limits.terminal instCategorySubterminals ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono subterminalsEquivMonoOverTerminal NatIso.ofComponents Functor.id Functor.comp ObjectProperty.FullSubcategory.obj IsSubterminal Limits.terminal.from MonoOver.homMk InducedCategory.Hom.hom ObjectProperty.FullSubcategory Comma.left Discrete discreteCategory Functor.fromPUnit ObjectProperty.homMk CommaMorphism.left Iso.refl	—	—
subterminals_thin 📖	mathematical	—	Quiver.Hom Subterminals CategoryStruct.toQuiver Category.toCategoryStruct instCategorySubterminals	—	ObjectProperty.hom_ext ObjectProperty.FullSubcategory.property
subterminals_to_monoOver_terminal_comp_forget 📖	mathematical	—	Functor.comp Subterminals instCategorySubterminals MonoOver Limits.terminal ObjectProperty.FullSubcategory.category Over instCategoryOver Over.isMono Equivalence.functor subterminalsEquivMonoOverTerminal MonoOver.forget Over.forget subterminalInclusion	—	—

CategoryTheory.IsSubterminal

Definitions

Name	Category	Theorems
isoDiag 📖	CompOp	2 math math: isoDiag_inv, isoDiag_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	mathematical	—	CategoryTheory.IsSubterminal	—	—
isIso_diag 📖	mathematical	CategoryTheory.IsSubterminal	CategoryTheory.IsIso CategoryTheory.Limits.prod CategoryTheory.Limits.diag	—	CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.hom_ext CategoryTheory.Category.id_comp def
isoDiag_hom 📖	mathematical	CategoryTheory.IsSubterminal	CategoryTheory.Iso.hom CategoryTheory.Limits.prod isoDiag CategoryTheory.inv CategoryTheory.Limits.diag isIso_diag	—	—
isoDiag_inv 📖	mathematical	CategoryTheory.IsSubterminal	CategoryTheory.Iso.inv CategoryTheory.Limits.prod isoDiag CategoryTheory.Limits.diag	—	—
mono_isTerminal_from 📖	mathematical	CategoryTheory.IsSubterminal	CategoryTheory.Mono CategoryTheory.Limits.IsTerminal.from	—	—
mono_terminal_from 📖	mathematical	CategoryTheory.IsSubterminal	CategoryTheory.Mono CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from	—	mono_isTerminal_from

---

← Back to Index