LiftingProperty

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

Statistics

Metric	Count
Definitions `llp`, `rlp`	2
Theorems `antitone_llp`, `antitone_rlp`, `colimitsOfShape_discrete_le_llp_rlp`, `coproducts_le_llp_rlp`, `gc_llp_rlp`, `le_llp_iff_le_rlp`, `le_llp_rlp`, `llp_isMultiplicative`, `llp_isStableUnderCobaseChange`, `llp_isStableUnderCoproductsOfShape`, `llp_isStableUnderRetracts`, `llp_of_isIso`, `llp_rlp_llp`, `pushouts_le_llp_rlp`, `retracts_le_llp_rlp`, `rlp_coproducts`, `rlp_isMultiplicative`, `rlp_isStableUnderBaseChange`, `rlp_isStableUnderProductsOfShape`, `rlp_isStableUnderRetracts`, `rlp_llp_rlp`, `rlp_of_isIso`, `rlp_pushouts`, `rlp_retracts`	24
Total	26

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`llp` 📖	CompOp	40 math math: `CategoryTheory.SmallObject.hasFunctorialFactorization`, `CategoryTheory.projective_iff_llp_epimorphisms_of_isZero`, `llp_of_isIso`, `llp_isStableUnderRetracts`, `CategoryTheory.SmallObject.functorialFactorizationData_i_app`, `isStableUnderTransfiniteCompositionOfShape_llp`, `transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `colimitsOfShape_discrete_le_llp_rlp`, `IsWeakFactorizationSystem.llp`, `llp_isStableUnderCobaseChange`, `llp_isStableUnderCoproductsOfShape`, `CategoryTheory.SmallObject.functorialFactorizationData_Z_obj`, `instHasFunctorialFactorizationLlpRlp`, `CategoryTheory.SmallObject.llp_rlp_ιObj`, `llp_rlp_of_hasSmallObjectArgument`, `CategoryTheory.projective_iff_llp_epimorphisms_zero`, `gc_llp_rlp`, `retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument`, `HomotopicalAlgebra.trivialFibrations_llp`, `llp_isMultiplicative`, `le_llp_rlp`, `le_llp_iff_le_rlp`, `rlp_llp_rlp`, `HomotopicalAlgebra.fibrations_llp`, `CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms`, `CategoryTheory.SmallObject.functorialFactorizationData_Z_map`, `coproducts_le_llp_rlp`, `transfiniteCompositionsOfShape_le_llp_rlp`, `llp_rlp_of_hasSmallObjectArgument'`, `retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `retracts_le_llp_rlp`, `antitone_llp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'`, `llp_rlp_llp`, `transfiniteCompositions_pushouts_coproducts_le_llp_rlp`, `pushouts_le_llp_rlp`, `llp_eq_of_wfs`, `CategoryTheory.SmallObject.functorialFactorizationData_p_app`, `transfiniteCompositions_le_llp_rlp`
`rlp` 📖	CompOp	49 math math: `CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp`, `CategoryTheory.SmallObject.hasFunctorialFactorization`, `rlp_coproducts`, `rlp_retracts`, `CategoryTheory.SmallObject.functorialFactorizationData_i_app`, `SSet.modelCategoryQuillen.fibrations_eq`, `transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `colimitsOfShape_discrete_le_llp_rlp`, `rlp_isStableUnderBaseChange`, `rlp_isStableUnderProductsOfShape`, `CategoryTheory.SmallObject.functorialFactorizationData_Z_obj`, `instHasFunctorialFactorizationLlpRlp`, `CategoryTheory.SmallObject.llp_rlp_ιObj`, `llp_rlp_of_hasSmallObjectArgument`, `rlp_isMultiplicative`, `rlp_eq_of_wfs`, `gc_llp_rlp`, `retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument`, `rlp_of_isIso`, `antitone_rlp`, `le_llp_rlp`, `le_llp_iff_le_rlp`, `rlp_llp_rlp`, `rlp_pushouts`, `CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms`, `CategoryTheory.SmallObject.functorialFactorizationData_Z_map`, `coproducts_le_llp_rlp`, `CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero`, `transfiniteCompositionsOfShape_le_llp_rlp`, `llp_rlp_of_hasSmallObjectArgument'`, `retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `CategoryTheory.SmallObject.rlp_πObj`, `CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom`, `HomotopicalAlgebra.trivialCofibrations_rlp`, `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp`, `HomotopicalAlgebra.cofibrations_rlp`, `retracts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'`, `llp_rlp_llp`, `CategoryTheory.IsGrothendieckAbelian.instHasFunctorialFactorizationMonomorphismsRlp`, `rlp_isStableUnderRetracts`, `transfiniteCompositions_pushouts_coproducts_le_llp_rlp`, `pushouts_le_llp_rlp`, `CategoryTheory.SmallObject.functorialFactorizationData_p_app`, `SSet.modelCategoryQuillen.fibration_iff`, `IsWeakFactorizationSystem.rlp`, `CategoryTheory.injective_iff_rlp_monomorphisms_zero`, `transfiniteCompositions_le_llp_rlp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_llp` 📖	mathematical	—	`Antitone` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `llp`	—	`GaloisConnection.monotone_l` `gc_llp_rlp`
`antitone_rlp` 📖	mathematical	—	`Antitone` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `rlp`	—	`GaloisConnection.monotone_u` `gc_llp_rlp`
`colimitsOfShape_discrete_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `colimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `llp` `rlp`	—	`colimitsOfShape_le` `llp_isStableUnderCoproductsOfShape` `colimitsOfShape_monotone` `le_llp_rlp`
`coproducts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `coproducts` `llp` `rlp`	—	`coproducts_iff` `colimitsOfShape_discrete_le_llp_rlp`
`gc_llp_rlp` 📖	mathematical	—	`GaloisConnection` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `OrderDual` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `llp` `rlp` `OrderDual.ofDual`	—	`le_llp_iff_le_rlp`
`le_llp_iff_le_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `llp` `rlp`	—	—
`le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `llp` `rlp`	—	`le_llp_iff_le_rlp` `le_refl`
`llp_isMultiplicative` 📖	mathematical	—	`IsMultiplicative` `llp`	—	`CategoryTheory.HasLiftingProperty.of_left_iso` `CategoryTheory.IsIso.id` `CategoryTheory.HasLiftingProperty.of_comp_left`
`llp_isStableUnderCobaseChange` 📖	mathematical	—	`IsStableUnderCobaseChange` `llp`	—	`CategoryTheory.IsPushout.hasLiftingProperty`
`llp_isStableUnderCoproductsOfShape` 📖	mathematical	—	`IsStableUnderCoproductsOfShape` `llp`	—	`instRespectsIsoOfIsStableUnderRetracts` `llp_isStableUnderRetracts` `CategoryTheory.instHasLiftingPropertyMap_1`
`llp_isStableUnderRetracts` 📖	mathematical	—	`IsStableUnderRetracts` `llp`	—	`CategoryTheory.RetractArrow.leftLiftingProperty`
`llp_of_isIso` 📖	mathematical	—	`llp`	—	`CategoryTheory.HasLiftingProperty.of_left_iso`
`llp_rlp_llp` 📖	mathematical	—	`llp` `rlp`	—	`GaloisConnection.l_u_l_eq_l` `gc_llp_rlp`
`pushouts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `pushouts` `llp` `rlp`	—	`isStableUnderCobaseChange_iff_pushouts_le` `llp_isStableUnderCobaseChange` `pushouts_monotone` `le_llp_rlp`
`retracts_le_llp_rlp` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts` `llp` `rlp`	—	`le_trans` `retracts_monotone` `le_llp_rlp` `retracts_le` `llp_isStableUnderRetracts`
`rlp_coproducts` 📖	mathematical	—	`rlp` `coproducts`	—	`le_antisymm` `antitone_rlp` `le_coproducts` `le_llp_iff_le_rlp` `coproducts_le_llp_rlp`
`rlp_isMultiplicative` 📖	mathematical	—	`IsMultiplicative` `rlp`	—	`CategoryTheory.HasLiftingProperty.of_right_iso` `CategoryTheory.IsIso.id` `CategoryTheory.HasLiftingProperty.of_comp_right`
`rlp_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `rlp`	—	`CategoryTheory.IsPullback.hasLiftingProperty`
`rlp_isStableUnderProductsOfShape` 📖	mathematical	—	`IsStableUnderProductsOfShape` `rlp`	—	`instRespectsIsoOfIsStableUnderRetracts` `rlp_isStableUnderRetracts` `CategoryTheory.instHasLiftingPropertyMap`
`rlp_isStableUnderRetracts` 📖	mathematical	—	`IsStableUnderRetracts` `rlp`	—	`CategoryTheory.RetractArrow.rightLiftingProperty`
`rlp_llp_rlp` 📖	mathematical	—	`rlp` `llp`	—	`GaloisConnection.u_l_u_eq_u` `gc_llp_rlp`
`rlp_of_isIso` 📖	mathematical	—	`rlp`	—	`CategoryTheory.HasLiftingProperty.of_right_iso`
`rlp_pushouts` 📖	mathematical	—	`rlp` `pushouts`	—	`le_antisymm` `antitone_rlp` `le_pushouts` `le_llp_iff_le_rlp` `pushouts_le_llp_rlp`
`rlp_retracts` 📖	mathematical	—	`rlp` `retracts`	—	`le_antisymm` `antitone_rlp` `le_retracts` `le_llp_iff_le_rlp` `retracts_le_llp_rlp`

---

← Back to Index