FunctorOfCocone

📁 Source: Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

Statistics

Metric	Count
Definitions isColimitCoconeOfLEOfCocone, ofCocone, map, obj, objIso, objIsoPt, ofCoconeObjIso, ofCoconeObjIsoPt, restrictionLTOfCoconeIso	9
Theorems arrowMap_ofCocone, arrowMap_ofCocone_to_top, map_comp, map_id, ofCoconeObjIso_hom_naturality, ofCoconeObjIso_hom_naturality_assoc, ofCocone_map, ofCocone_map_assoc, ofCocone_map_to_top, ofCocone_obj_eq, ofCocone_obj_eq_pt, restrictionLTOfCoconeIso_hom_app, restrictionLTOfCoconeIso_inv_app	13
Total	22

CategoryTheory.SmallObject.SuccStruct

Definitions

Name	Category	Theorems
isColimitCoconeOfLEOfCocone 📖	CompOp	—
ofCocone 📖	CompOp	11 math math: ofCocone_map_assoc, restrictionLTOfCoconeIso_inv_app, ofCoconeObjIso_hom_naturality, ofCoconeObjIso_hom_naturality_assoc, restrictionLTOfCoconeIso_hom_app, arrowMap_ofCocone_to_top, ofCocone_obj_eq_pt, ofCocone_map_to_top, ofCocone_obj_eq, arrowMap_ofCocone, ofCocone_map
ofCoconeObjIso 📖	CompOp	7 math math: ofCocone_map_assoc, restrictionLTOfCoconeIso_inv_app, ofCoconeObjIso_hom_naturality, ofCoconeObjIso_hom_naturality_assoc, restrictionLTOfCoconeIso_hom_app, ofCocone_map_to_top, ofCocone_map
ofCoconeObjIsoPt 📖	CompOp	1 math math: ofCocone_map_to_top
restrictionLTOfCoconeIso 📖	CompOp	2 math math: restrictionLTOfCoconeIso_inv_app, restrictionLTOfCoconeIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowMap_ofCocone 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	arrowMap ofCocone LT.lt.le CategoryTheory.Functor.obj Set.Elem Set.Iio Preorder.smallCategory Subtype.preorder Set Set.instMembership lt_of_le_of_lt CategoryTheory.Functor.map CategoryTheory.homOfLE	—	CategoryTheory.Arrow.ext LT.lt.le lt_of_le_of_lt ofCocone_obj_eq ofCocone_map
arrowMap_ofCocone_to_top 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	arrowMap ofCocone LT.lt.le CategoryTheory.Functor.obj Set.Elem Set.Iio Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	LT.lt.le arrowMap.eq_1 ofCocone_map_to_top CategoryTheory.Arrow.ext ofCocone_obj_eq ofCocone_obj_eq_pt
ofCoconeObjIso_hom_naturality 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LE.le.trans LT.lt.le Set.Iio CategoryTheory.Functor.map CategoryTheory.homOfLE CategoryTheory.Iso.hom ofCoconeObjIso lt_of_le_of_lt	—	LE.le.trans LT.lt.le lt_of_le_of_lt ofCocone_map CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
ofCoconeObjIso_hom_naturality_assoc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LE.le.trans LT.lt.le CategoryTheory.Functor.map CategoryTheory.homOfLE Set.Iio CategoryTheory.Iso.hom ofCoconeObjIso lt_of_le_of_lt	—	LE.le.trans LT.lt.le lt_of_le_of_lt CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofCoconeObjIso_hom_naturality
ofCocone_map 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	CategoryTheory.Functor.map Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LE.le.trans LT.lt.le CategoryTheory.homOfLE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj lt_of_le_of_lt Set.Iio CategoryTheory.Iso.hom ofCoconeObjIso CategoryTheory.Iso.inv	—	LE.le.trans LT.lt.le lt_of_le_of_lt
ofCocone_map_assoc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LE.le.trans LT.lt.le CategoryTheory.Functor.map CategoryTheory.homOfLE Set.Iio lt_of_le_of_lt CategoryTheory.Iso.hom ofCoconeObjIso CategoryTheory.Iso.inv	—	LT.lt.le LE.le.trans lt_of_le_of_lt CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofCocone_map
ofCocone_map_to_top 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.map Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LT.lt.le CategoryTheory.homOfLE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Iio CategoryTheory.Iso.hom ofCoconeObjIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv ofCoconeObjIsoPt	—	LT.lt.le CategoryTheory.Category.comp_id
ofCocone_obj_eq 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone LT.lt.le Set.Iio	—	LT.lt.le
ofCocone_obj_eq_pt 📖	mathematical	—	CategoryTheory.Functor.obj Set.Elem Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Set Set.instMembership ofCocone CategoryTheory.Limits.Cocone.pt Set.Iio	—	—
restrictionLTOfCoconeIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Set.Elem Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.SmallObject.restrictionLT ofCocone CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category le_refl restrictionLTOfCoconeIso CategoryTheory.Functor.obj ofCoconeObjIso	—	le_refl
restrictionLTOfCoconeIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Set.Elem Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.SmallObject.restrictionLT ofCocone CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category le_refl restrictionLTOfCoconeIso CategoryTheory.Functor.obj ofCoconeObjIso	—	le_refl

CategoryTheory.SmallObject.SuccStruct.ofCocone

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: map_comp, map_id
obj 📖	CompOp	2 math math: map_comp, map_id
objIso 📖	CompOp	—
objIsoPt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	map LE.le.trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj	—	LE.le.trans LE.le.lt_or_eq LT.lt.trans CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.homOfLE_comp CategoryTheory.eqToHom_refl CategoryTheory.Category.comp_id CategoryTheory.Limits.Cocone.w_assoc map_id CategoryTheory.Category.id_comp
map_id 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	—

---

← Back to Index