ExtendToSucc

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

Statistics

Metric	Count
Definitions extendToSucc, map, obj, objIso, objSuccIso, extendToSuccObjIso, extendToSuccObjSuccIso, extendToSuccRestrictionLEIso	8
Theorems arrowMap_extendToSucc, arrowSucc_extendToSucc, map_comp, map_eq, map_id, map_self_succ, obj_eq, obj_succ_eq, extendToSuccObjIso_hom_naturality, extendToSuccObjIso_hom_naturality_assoc, extendToSuccRestrictionLEIso_hom_app, extendToSuccRestrictionLEIso_inv_app, extendToSucc_map, extendToSucc_map_le_succ, extendToSucc_obj_eq, extendToSucc_obj_succ_eq	16
Total	24

CategoryTheory.SmallObject.SuccStruct

Definitions

Name	Category	Theorems
extendToSucc 📖	CompOp	10 math math: extendToSucc_map_le_succ, extendToSuccObjIso_hom_naturality_assoc, extendToSuccObjIso_hom_naturality, extendToSuccRestrictionLEIso_hom_app, extendToSucc_obj_eq, extendToSuccRestrictionLEIso_inv_app, extendToSucc_map, extendToSucc_obj_succ_eq, arrowSucc_extendToSucc, arrowMap_extendToSucc
extendToSuccObjIso 📖	CompOp	6 math math: extendToSucc_map_le_succ, extendToSuccObjIso_hom_naturality_assoc, extendToSuccObjIso_hom_naturality, extendToSuccRestrictionLEIso_hom_app, extendToSuccRestrictionLEIso_inv_app, extendToSucc_map
extendToSuccObjSuccIso 📖	CompOp	1 math math: extendToSucc_map_le_succ
extendToSuccRestrictionLEIso 📖	CompOp	2 math math: extendToSuccRestrictionLEIso_hom_app, extendToSuccRestrictionLEIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowMap_extendToSucc 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	arrowMap Order.succ extendToSucc LE.le.trans Order.le_succ	—	LE.le.trans Order.le_succ extendToSucc.obj_eq extendToSucc_map CategoryTheory.Arrow.arrow_mk_eqToHom_comp CategoryTheory.Arrow.arrow_mk_comp_eqToHom
arrowSucc_extendToSucc 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	arrowSucc Order.succ extendToSucc Order.lt_succ_of_not_isMax CategoryTheory.Functor.obj Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership	—	Order.lt_succ_of_not_isMax extendToSucc.obj_succ_eq LE.le.trans Order.le_succ extendToSucc.obj_eq extendToSucc_map_le_succ CategoryTheory.Arrow.arrow_mk_eqToHom_comp CategoryTheory.Arrow.arrow_mk_comp_eqToHom
extendToSuccObjIso_hom_naturality 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc LE.le.trans Order.le_succ CategoryTheory.Functor.map CategoryTheory.homOfLE CategoryTheory.Iso.hom extendToSuccObjIso	—	LE.le.trans Order.le_succ extendToSucc.map_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
extendToSuccObjIso_hom_naturality_assoc 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc LE.le.trans Order.le_succ CategoryTheory.Functor.map CategoryTheory.homOfLE CategoryTheory.Iso.hom extendToSuccObjIso	—	LE.le.trans Order.le_succ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendToSuccObjIso_hom_naturality
extendToSuccRestrictionLEIso_hom_app 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.NatTrans.app Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.SmallObject.restrictionLE Order.succ extendToSucc CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Order.le_succ extendToSuccRestrictionLEIso CategoryTheory.Functor.obj extendToSuccObjIso	—	Order.le_succ
extendToSuccRestrictionLEIso_inv_app 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.NatTrans.app Set.Elem Set.Iic Preorder.smallCategory Subtype.preorder Set Set.instMembership CategoryTheory.SmallObject.restrictionLE Order.succ extendToSucc CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category Order.le_succ extendToSuccRestrictionLEIso CategoryTheory.Functor.obj extendToSuccObjIso	—	Order.le_succ
extendToSucc_map 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.map Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc LE.le.trans Order.le_succ CategoryTheory.homOfLE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.hom extendToSuccObjIso CategoryTheory.Iso.inv	—	LE.le.trans Order.le_succ extendToSuccObjIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
extendToSucc_map_le_succ 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.map Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc LE.le.trans Order.le_succ CategoryTheory.homOfLE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.hom extendToSuccObjIso CategoryTheory.Iso.inv extendToSuccObjSuccIso	—	extendToSucc.map_self_succ
extendToSucc_obj_eq 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.obj Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc LE.le.trans Order.le_succ	—	extendToSucc.obj_eq
extendToSucc_obj_succ_eq 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	CategoryTheory.Functor.obj Set.Elem Set.Iic Order.succ Preorder.smallCategory Subtype.preorder Set Set.instMembership extendToSucc	—	extendToSucc.obj_succ_eq

CategoryTheory.SmallObject.SuccStruct.extendToSucc

Definitions

Name	Category	Theorems
map 📖	CompOp	4 math math: map_self_succ, map_eq, map_comp, map_id
obj 📖	CompOp	6 math math: map_self_succ, obj_succ_eq, map_eq, map_comp, map_id, obj_eq
objIso 📖	CompOp	2 math math: map_self_succ, map_eq
objSuccIso 📖	CompOp	1 math math: map_self_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	map LE.le.trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership Set.Iic	—	LE.le.trans Order.le_succ map_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.homOfLE_comp LE.le.lt_or_eq Order.lt_succ_iff_of_not_isMax CategoryTheory.Category.comp_id map_id le_antisymm Order.succ_le_of_lt not_le
map_eq 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	map LE.le.trans Order.succ Order.le_succ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership Set.Iic CategoryTheory.Functor.obj Set.Elem Preorder.smallCategory Subtype.preorder CategoryTheory.Iso.hom objIso CategoryTheory.Functor.map CategoryTheory.homOfLE CategoryTheory.Iso.inv	—	LE.le.trans Order.le_succ
map_id 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership Set.Iic LE.le.trans	—	LE.le.trans CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id le_antisymm Order.succ_le_of_lt not_le
map_self_succ 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	map Order.succ Order.le_succ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Set Set.instMembership Set.Iic LE.le.trans CategoryTheory.Functor.obj Set.Elem Preorder.smallCategory Subtype.preorder CategoryTheory.Iso.hom objIso CategoryTheory.Iso.inv objSuccIso	—	LE.le.trans Order.le_succ le_refl CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
obj_eq 📖	mathematical	—	obj Set Set.instMembership Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.succ LE.le.trans Order.le_succ CategoryTheory.Functor.obj Set.Elem Preorder.smallCategory Subtype.preorder	—	LE.le.trans Order.le_succ
obj_succ_eq 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	obj Set Set.instMembership Set.Iic Order.succ	—	—

---

← Back to Index