Commit 2025-02-10 05:59 942265ab

View on Github →

feat(CategoryTheory/MorphismProperty/LiftingProperty): more API for llp and rlp (#21597) We show that rlp and llp form a Galois connection, and we deduce some consequences.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

added theorem CategoryTheory.MorphismProperty.antitone_llp

added theorem CategoryTheory.MorphismProperty.antitone_rlp

added theorem CategoryTheory.MorphismProperty.colimitsOfShape_discrete_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.coproducts_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.gc_llp_rlp

added theorem CategoryTheory.MorphismProperty.le_llp_iff_le_rlp

added theorem CategoryTheory.MorphismProperty.le_llp_rlp

deleted theorem CategoryTheory.MorphismProperty.llp_IsStableUnderCoproductsOfShape

added theorem CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape

deleted theorem CategoryTheory.MorphismProperty.llp_isStableUnderRetracts

added theorem CategoryTheory.MorphismProperty.llp_rlp_llp

added theorem CategoryTheory.MorphismProperty.pushouts_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.retracts_le_llp_rlp

deleted theorem CategoryTheory.MorphismProperty.rlp_IsStableUnderProductsOfShape

added theorem CategoryTheory.MorphismProperty.rlp_coproducts

added theorem CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape

deleted theorem CategoryTheory.MorphismProperty.rlp_isStableUnderRetracts

added theorem CategoryTheory.MorphismProperty.rlp_llp_rlp

added theorem CategoryTheory.MorphismProperty.rlp_pushouts

added theorem CategoryTheory.MorphismProperty.rlp_retracts