MorphismProperty

📁 Source: Mathlib/CategoryTheory/PathCategory/MorphismProperty.lean

Statistics

Metric	Count
Definitions liftNatIso, liftNatTrans	2
Theorems liftNatIso_hom_app, liftNatIso_inv_app, liftNatTrans_app, morphismProperty_eq_top, morphismProperty_eq_top', morphismProperty_eq_top_of_isMultiplicative	6
Total	8

CategoryTheory.Paths

Definitions

Name	Category	Theorems
liftNatIso 📖	CompOp	2 math math: liftNatIso_inv_app, liftNatIso_hom_app
liftNatTrans 📖	CompOp	1 math math: liftNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftNatIso_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Paths categoryPaths CategoryTheory.Functor.map Quiver.Hom.toPath CategoryTheory.Iso.hom	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso	—	—
liftNatIso_inv_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Paths categoryPaths CategoryTheory.Functor.map Quiver.Hom.toPath CategoryTheory.Iso.hom	CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso	—	—
liftNatTrans_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Paths categoryPaths CategoryTheory.Functor.map Quiver.Hom.toPath	CategoryTheory.NatTrans.app liftNatTrans	—	—
morphismProperty_eq_top 📖	mathematical	Prefunctor.obj CategoryTheory.Paths CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryPaths of CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.comp Prefunctor.map	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.ext induction
morphismProperty_eq_top' 📖	mathematical	Prefunctor.obj CategoryTheory.Paths CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryPaths of CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.comp Prefunctor.map	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.ext induction'
morphismProperty_eq_top_of_isMultiplicative 📖	mathematical	Prefunctor.obj CategoryTheory.Paths CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryPaths of Prefunctor.map	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	morphismProperty_eq_top CategoryTheory.MorphismProperty.id_mem CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition

---

← Back to Index