Commit 2025-01-18 20:53 da939cc7

View on Github →

feat(AlgebraicGeometry): flat morphisms of schemes (#19790) ... and show that Flat can be checked on stalks. The latter is shown more generally for any morphism property of schemes associated to a property of ring maps satisfying RingHom.OfLocalizationPrime.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.Spec.map_surjective

Created Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

added theorem AlgebraicGeometry.Flat.iff_flat_stalkMap

added theorem AlgebraicGeometry.Flat.of_stalkMap

added theorem AlgebraicGeometry.Flat.stalkMap

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem AlgebraicGeometry.HasRingHomProperty.of_stalkMap

added theorem AlgebraicGeometry.HasRingHomProperty.stalkMap

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Hom.coe_resLE_base

added def AlgebraicGeometry.Scheme.Hom.resLEStalkMap

added theorem AlgebraicGeometry.Scheme.Opens.stalkIso_inv

added theorem AlgebraicGeometry.Scheme.Opens.ι_base_apply

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/RingTheory/RingHom/Flat.lean

added theorem RingHom.Flat.localRingHom

added theorem RingHom.Flat.ofLocalizationPrime

Modified Mathlib/RingTheory/RingHomProperties.lean

added theorem RingHom.RespectsIso.arrow_mk_iso_iff