Commit 2025-02-07 21:51 c935b3d0

View on Github →

chore(AlgebraicGeometry): more API for local at source (#21390) In particular P.diagonal is local at the source if P is and P is sufficiently compatible with open immersions.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.preimage_opensRange

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

added theorem CategoryTheory.Limits.pullback.comp_diagonal

modified theorem CategoryTheory.Limits.pullback.diagonal_comp

Modified Mathlib/CategoryTheory/MorphismProperty/Composition.lean

added theorem CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le

added theorem CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_le

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean