Commit 2024-11-01 10:29 c68aa108

View on Github →

feat(AlgebraicGeometry/Morphisms): affine + ring hom property (#18356) We add a constructor for properties of affine morphisms of schemes satisfying a given property of ring homomorphisms on sections.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMap

added theorem AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map

Created Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_iff

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom

added theorem AlgebraicGeometry.HasAffineProperty.affineAnd_stableUnderBaseChange

added def AlgebraicGeometry.affineAnd

added theorem AlgebraicGeometry.affineAnd_apply

added theorem AlgebraicGeometry.affineAnd_isLocal

added theorem AlgebraicGeometry.affineAnd_respectsIso

added theorem AlgebraicGeometry.affineAnd_stableUnderBaseChange

added theorem AlgebraicGeometry.targetAffineLocally_affineAnd_iff

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem RingHom.OfLocalizationSpan.ofIsLocalization'

added theorem RingHom.OfLocalizationSpan.ofIsLocalization