Commit 2024-07-09 17:23 384c2eb7

View on Github →

feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API (#14328) Adds a MorphismProperty.stalkwise constructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for properties local at the target.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

added def AlgebraicGeometry.AffineTargetMorphismProperty.of

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.of_isLocal_of_isLocalAtTarget

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.stableUnderBaseChange_of_stableUnderBaseChangeOnAffine_of_isLocalAtTarget

added theorem AlgebraicGeometry.AffineTargetMorphismProperty.targetAffineLocally_of_eq_of_isLocalAtTarget

added def AlgebraicGeometry.MorphismProperty.stalkwise

added theorem AlgebraicGeometry.MorphismProperty.stalkwiseIsLocalAtTarget_of_respectsIso

added theorem AlgebraicGeometry.MorphismProperty.stalkwise_respectsIso

modified def AlgebraicGeometry.MorphismProperty.topologically

modified theorem AlgebraicGeometry.MorphismProperty.topologically_isStableUnderComposition

modified theorem AlgebraicGeometry.MorphismProperty.topologically_iso_le

modified theorem AlgebraicGeometry.MorphismProperty.topologically_propertyIsLocalAtTarget

modified theorem AlgebraicGeometry.MorphismProperty.topologically_respectsIso

Modified Mathlib/RingTheory/RingHomProperties.lean

added def RingHom.toMorphismProperty

added theorem RingHom.toMorphismProperty_respectsIso_iff