Documentation Verification Report

TransfiniteCompositionLifting

📁 Source: Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

Statistics

Metric	Count
Definitions `SqStruct`, `f'`, `map`, `sqFunctor`, `wellOrderInductionData`, `liftHom`	6
Theorems `ext`, `ext_iff`, `map_f'`, `sq`, `w`, `w_assoc`, `w₁`, `w₁_assoc`, `w₂`, `w₂_assoc`, `hasLift`, `hasLiftingPropertyFixedBot_ι_app_bot`, `hasLiftingProperty_ι_app_bot`, `sqFunctor_map`, `sqFunctor_obj`, `liftHom_fac`, `liftHom_fac_assoc`, `lift_f'`, `map_lift`, `isStableUnderTransfiniteCompositionOfShape_llp`, `retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp`, `retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `transfiniteCompositionsOfShape_le_llp_rlp`, `transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `transfiniteCompositions_le_llp_rlp`, `transfiniteCompositions_pushouts_coproducts_le_llp_rlp`	26
Total	32

CategoryTheory.HasLiftingProperty.transfiniteComposition

Definitions

Name	Category	Theorems
`SqStruct` 📖	CompData	1 math math: `sqFunctor_obj`
`sqFunctor` 📖	CompOp	5 math math: `wellOrderInductionData.liftHom_fac_assoc`, `wellOrderInductionData.liftHom_fac`, `sqFunctor_obj`, `wellOrderInductionData.map_lift`, `sqFunctor_map`
`wellOrderInductionData` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLift` 📖	mathematical	`CategoryTheory.HasLiftingPropertyFixedBot` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `CategoryTheory.CommSq` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	`CategoryTheory.CommSq.HasLift`	—	`Order.le_succ` `bot_le` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.CommSq.w` `CategoryTheory.Functor.WellOrderInductionData.surjective` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `SqStruct.w₂`
`hasLiftingPropertyFixedBot_ι_app_bot` 📖	mathematical	`CategoryTheory.HasLiftingPropertyFixedBot` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`Order.le_succ` `hasLift`
`hasLiftingProperty_ι_app_bot` 📖	mathematical	`CategoryTheory.HasLiftingProperty` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`Order.le_succ` `hasLift` `CategoryTheory.sq_hasLift_of_hasLiftingProperty`
`sqFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.types` `sqFunctor` `SqStruct.map` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`sqFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.types` `sqFunctor` `SqStruct` `Opposite.unop`	—	—

CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct

Definitions

Name	Category	Theorems
`f'` 📖	CompOp	10 math math: `CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc`, `CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac`, `map_f'`, `sq`, `w₁`, `CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift_f'`, `w₂`, `w₁_assoc`, `w₂_assoc`, `ext_iff`
`map` 📖	CompOp	3 math math: `map_f'`, `CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift`, `CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`f'`	—	—	`bot_le`
`ext_iff` 📖	mathematical	—	`f'`	—	`ext`
`map_f'` 📖	mathematical	—	`f'` `map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.Functor.map`	—	—
`sq` 📖	mathematical	—	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.succ` `f'` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`Order.le_succ` `w₂` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.id_comp`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`bot_le` `w₁` `CategoryTheory.Category.assoc` `w₂` `CategoryTheory.Limits.Cocone.w_assoc`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`
`w₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `bot_le` `f'`	—	—
`w₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `bot_le` `f'`	—	`bot_le` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₁`
`w₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `f'` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	—
`w₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `f'` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₂`

CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData

Definitions

Name	Category	Theorems
`liftHom` 📖	CompOp	3 math math: `liftHom_fac_assoc`, `liftHom_fac`, `lift_f'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftHom_fac` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `LT.lt.le` `liftHom` `CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f'` `Opposite.unop` `Opposite` `Set` `Set.instMembership` `Set.Iio` `CategoryTheory.Category.opposite` `Subtype.preorder` `CategoryTheory.Functor.op` `Monotone.functor` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHom.Subtype.val` `OrderHom.monotone` `Opposite.op` `CategoryTheory.Functor.sections` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor`	—	`OrderHom.monotone` `CategoryTheory.Limits.IsColimit.fac` `PrincipalSeg.monotone`
`liftHom_fac_assoc` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `LT.lt.le` `liftHom` `CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f'` `Opposite.unop` `Opposite` `Set` `Set.instMembership` `Set.Iio` `CategoryTheory.Category.opposite` `Subtype.preorder` `CategoryTheory.Functor.op` `Monotone.functor` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHom.Subtype.val` `OrderHom.monotone` `Opposite.op` `CategoryTheory.Functor.sections` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor`	—	`OrderHom.monotone` `LT.lt.le` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `liftHom_fac`
`lift_f'` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f'` `Opposite.unop` `Opposite.op` `lift` `liftHom`	—	`OrderHom.monotone`
`map_lift` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map` `Opposite.unop` `Opposite.op` `lift` `CategoryTheory.homOfLE` `LT.lt.le` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Opposite` `Set.Iio` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Subtype.preorder` `CategoryTheory.Functor.comp` `CategoryTheory.types` `CategoryTheory.Functor.op` `Monotone.functor` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHom.Subtype.val` `OrderHom.monotone` `CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor`	—	`OrderHom.monotone` `CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.ext` `LT.lt.le` `liftHom_fac`

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStableUnderTransfiniteCompositionOfShape_llp` 📖	mathematical	—	`IsStableUnderTransfiniteCompositionOfShape` `llp`	—	`isStableUnderTransfiniteCompositionOfShape_iff` `CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot` `CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous` `TransfiniteCompositionOfShape.map_mem` `arrow_mk_iso_iff` `instRespectsIsoOfIsStableUnderRetracts` `llp_isStableUnderRetracts` `CategoryTheory.TransfiniteCompositionOfShape.fac` `CategoryTheory.Category.comp_id`
`retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts` `transfiniteCompositions` `pushouts` `coproducts` `llp` `rlp`	—	`le_llp_iff_le_rlp` `rlp_retracts` `transfiniteCompositions_pushouts_coproducts_le_llp_rlp`
`retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts` `transfiniteCompositionsOfShape` `pushouts` `coproducts` `llp` `rlp`	—	`le_llp_iff_le_rlp` `rlp_retracts` `transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`
`transfiniteCompositionsOfShape_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape` `llp` `rlp`	—	`isStableUnderTransfiniteCompositionOfShape_llp` `le_trans` `transfiniteCompositionsOfShape_monotone` `le_llp_rlp` `isStableUnderTransfiniteCompositionOfShape_iff`
`transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape` `pushouts` `coproducts` `llp` `rlp`	—	`rlp_pushouts` `rlp_coproducts` `transfiniteCompositionsOfShape_le_llp_rlp`
`transfiniteCompositions_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions` `llp` `rlp`	—	`transfiniteCompositions_iff` `transfiniteCompositionsOfShape_le_llp_rlp`
`transfiniteCompositions_pushouts_coproducts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions` `pushouts` `coproducts` `llp` `rlp`	—	`rlp_pushouts` `rlp_coproducts` `transfiniteCompositions_le_llp_rlp`

---

← Back to Index