StrictInitial

📁 Source: Mathlib/CategoryTheory/Comma/Over/StrictInitial.lean

Statistics

Metric	Count
Definitions overEquivOfIsInitial, underEquivOfIsTerminal, overEquivOfIsInitial, underEquivOfIsTerminal	4
Theorems overEquivOfIsInitial_counitIso, overEquivOfIsInitial_functor, overEquivOfIsInitial_inverse, overEquivOfIsInitial_unitIso, underEquivOfIsTerminal_counitIso, underEquivOfIsTerminal_functor, underEquivOfIsTerminal_inverse, underEquivOfIsTerminal_unitIso, overEquivOfIsInitial_counitIso, overEquivOfIsInitial_functor, overEquivOfIsInitial_inverse, overEquivOfIsInitial_unitIso, underEquivOfIsTerminal_counitIso, underEquivOfIsTerminal_functor, underEquivOfIsTerminal_inverse, underEquivOfIsTerminal_unitIso	16
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
overEquivOfIsInitial 📖	CompOp	4 math math: overEquivOfIsInitial_functor, overEquivOfIsInitial_inverse, overEquivOfIsInitial_unitIso, overEquivOfIsInitial_counitIso
underEquivOfIsTerminal 📖	CompOp	4 math math: underEquivOfIsTerminal_unitIso, underEquivOfIsTerminal_functor, underEquivOfIsTerminal_inverse, underEquivOfIsTerminal_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
overEquivOfIsInitial_counitIso 📖	mathematical	—	Equivalence.counitIso Over Discrete instCategoryOver discreteCategory overEquivOfIsInitial Iso.refl Functor Functor.category Functor.comp Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct Functor.star	—	—
overEquivOfIsInitial_functor 📖	mathematical	—	Equivalence.functor Over Discrete instCategoryOver discreteCategory overEquivOfIsInitial Functor.star	—	—
overEquivOfIsInitial_inverse 📖	mathematical	—	Equivalence.inverse Over Discrete instCategoryOver discreteCategory overEquivOfIsInitial Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct	—	—
overEquivOfIsInitial_unitIso 📖	mathematical	—	Equivalence.unitIso Over Discrete instCategoryOver discreteCategory overEquivOfIsInitial NatIso.ofComponents Functor.id Functor.comp Functor.star Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct Over.isoMk Functor.obj asIso Comma.left Comma.hom	—	—
underEquivOfIsTerminal_counitIso 📖	mathematical	—	Equivalence.counitIso Under Discrete instCategoryUnder discreteCategory underEquivOfIsTerminal Iso.refl Functor Functor.category Functor.comp Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct Functor.star	—	—
underEquivOfIsTerminal_functor 📖	mathematical	—	Equivalence.functor Under Discrete instCategoryUnder discreteCategory underEquivOfIsTerminal Functor.star	—	—
underEquivOfIsTerminal_inverse 📖	mathematical	—	Equivalence.inverse Under Discrete instCategoryUnder discreteCategory underEquivOfIsTerminal Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct	—	—
underEquivOfIsTerminal_unitIso 📖	mathematical	—	Equivalence.unitIso Under Discrete instCategoryUnder discreteCategory underEquivOfIsTerminal NatIso.ofComponents Functor.id Functor.comp Functor.star Functor.fromPUnit CategoryStruct.id Category.toCategoryStruct Under.isoMk Functor.obj Iso.symm Comma.left Comma.right asIso Comma.hom	—	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
overEquivOfIsInitial 📖	CompOp	4 math math: overEquivOfIsInitial_counitIso, overEquivOfIsInitial_inverse, overEquivOfIsInitial_functor, overEquivOfIsInitial_unitIso
underEquivOfIsTerminal 📖	CompOp	4 math math: underEquivOfIsTerminal_inverse, underEquivOfIsTerminal_counitIso, underEquivOfIsTerminal_unitIso, underEquivOfIsTerminal_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
overEquivOfIsInitial_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Over CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop overEquivOfIsInitial CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.id id_mem CategoryTheory.Functor.star	—	id_mem IsMultiplicative.instTop
overEquivOfIsInitial_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Over CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop overEquivOfIsInitial CategoryTheory.Functor.star	—	IsMultiplicative.instTop
overEquivOfIsInitial_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Over CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop overEquivOfIsInitial CategoryTheory.CategoryStruct.id id_mem	—	IsMultiplicative.instTop
overEquivOfIsInitial_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Over CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop overEquivOfIsInitial CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp CategoryTheory.Functor.star CategoryTheory.CategoryStruct.id id_mem Over.isoMk CategoryTheory.Functor.obj CategoryTheory.asIso CategoryTheory.Comma.left Comma.toComma CategoryTheory.Comma.hom	—	id_mem IsMultiplicative.instTop
underEquivOfIsTerminal_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Under CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop underEquivOfIsTerminal CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.id id_mem CategoryTheory.Functor.star	—	id_mem IsMultiplicative.instTop
underEquivOfIsTerminal_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Under CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop underEquivOfIsTerminal CategoryTheory.Functor.star	—	IsMultiplicative.instTop
underEquivOfIsTerminal_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Under CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop underEquivOfIsTerminal CategoryTheory.CategoryStruct.id id_mem	—	IsMultiplicative.instTop
underEquivOfIsTerminal_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Under CategoryTheory.Discrete Comma.instCategory CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra IsMultiplicative.instTop underEquivOfIsTerminal CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp CategoryTheory.Functor.star CategoryTheory.CategoryStruct.id id_mem Under.isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.symm CategoryTheory.Comma.left Comma.toComma CategoryTheory.Comma.right CategoryTheory.asIso CategoryTheory.Comma.hom	—	id_mem IsMultiplicative.instTop

---

← Back to Index