Commit 2024-11-15 02:04 e69ec59a

View on Github →

chore(CategoryTheory/MorphismProperty): split HasTwoOutOfThreeProperty (#18877) Splits the HasTwoOutOfThreeProperty typeclass into HasOfPrecompProperty and HasOfPostcompProperty. This allows more automation when working with P.Over Q X categories. Also shows that under suitable assumptions, HasOfPostcompProperty P is equivalent to P ≤ P.diagonal.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

deleted theorem CategoryTheory.MorphismProperty.Over.hasPullbacks

Modified Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

added theorem CategoryTheory.Limits.pullback_lift_diagonal_isPullback

Modified Mathlib/CategoryTheory/Localization/Bousfield.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Composition.lean

modified theorem CategoryTheory.MorphismProperty.of_postcomp

modified theorem CategoryTheory.MorphismProperty.of_precomp

modified theorem CategoryTheory.MorphismProperty.postcomp_iff

modified theorem CategoryTheory.MorphismProperty.precomp_iff

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal

Modified Mathlib/CategoryTheory/Sites/PreservesSheafification.lean