feat(AlgebraicGeometry): geometrically-P morphisms (#35246)

We define the basic interface for properties like geometrically reduced, geometrically irreducible, geometrically
connected etc. In this file we treat an abstract property of schemes `P` and derive the general properties that are
shared by all of these variants.

This contribution was created as part of the Formalising Algebraic Geometry workshop 2025 in
Heidelberg

Co-authored by: Timo Kränzle <timokraenzle03@gmail.com>
Co-authored by: Judith Ludwig <ludwig@mathi.uni-heidelberg.de>
Co-authored by: Bryan Wang Peng Jun <bwangpengjun@math.harvard.edu>
Co-authored by: Yannis Monbru <yannis.monbru@orange.fr>
Co-authored by: Alireza Shavali <a.shavali74@gmail.com>
Co-authored by: Chenyi Yang

Author: chrisflav

Mathlib.lean

@@ -1296,6 +1296,7 @@ public import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 public import Mathlib.AlgebraicGeometry.Fiber
 public import Mathlib.AlgebraicGeometry.FunctionField
 public import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
+public import Mathlib.AlgebraicGeometry.Geometrically.Basic
 public import Mathlib.AlgebraicGeometry.Gluing
 public import Mathlib.AlgebraicGeometry.GluingOneHypercover
 public import Mathlib.AlgebraicGeometry.Group.Smooth

Mathlib/AlgebraicGeometry/Geometrically/Basic.lean

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Timo Kraenzle, Judith Ludwig, Bryan Wang, Christian Merten,
+  Yannis Monbru, Alireza Shavali, Chenyi Yang
+-/
+module
+
+public import Mathlib.AlgebraicGeometry.Properties
+public import Mathlib.AlgebraicGeometry.Fiber
+
+/-!
+# Geometrically-`P` schemes over a field
+
+In this file we define the basic interface for properties like geometrically reduced,
+geometrically irreducible, geometrically connected etc. In this file
+we treat an abstract property of schemes `P` and derive the general properties that are
+shared by all of these variants.
+
+A morphism of schemes `f : X ⟶ Y` is geometrically `P` if for any field `K` and
+morphism `Spec K ⟶ Y`, the base change `X ×[Y] Spec K` satisfies `P`.
+
+## Main definitions and results
+
+- `AlgebraicGeometry.geometrically`: The morphism property of geometrically-`P` morphisms
+- `AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField`: `f : X ⟶ Y` is
+  geometrically-`P` if and only if for every `y : Y`, the fiber `f ⁻¹ {y}` is geometrically-`P`
+  over `Spec κ(y)`.
+
+## Notes
+
+This contribution was created as part of the Formalising Algebraic Geometry workshop 2025 in
+Heidelberg.
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Limits CommRingCat
+
+namespace AlgebraicGeometry
+
+/-- A morphism of schemes `f : X ⟶ Y` is geometrically `P` if for any field `K` and
+morphism `Spec K ⟶ Y`, the base change `X ×[Y] Spec K` satisfies `P`. -/
+def geometrically (P : ObjectProperty Scheme.{u}) : MorphismProperty Scheme.{u} :=
+  fun X Y f ↦ ∀ ⦃K : Type u⦄ [Field K] (y : Spec (.of K) ⟶ Y)
+    ⦃Z : Scheme.{u}⦄ (fst : Z ⟶ X) (snd : Z ⟶ Spec (.of K)),
+    IsPullback fst snd f y → P Z
+
+lemma geometrically_eq_universally (P : ObjectProperty Scheme.{u}) :
+    geometrically P = .universally fun X Y _ ↦ IsIntegral Y → Subsingleton Y → P X := by
+  ext X Y f
+  refine ⟨fun hf Z W snd q fst h _ _ ↦ ?_, fun hf aK y Z W fst snd h ↦ ?_⟩
+  · let := (isField_of_isIntegral_of_subsingleton W).toField
+    apply hf (W.isoSpec.inv ≫ q) snd (fst ≫ W.isoSpec.hom)
+    apply h.flip.of_iso (.refl _) (.refl _) W.isoSpec (.refl _) <;> simp
+  · exact hf _ _ _ h.flip inferInstance inferInstance
+
+variable (P : ObjectProperty Scheme.{u})
+
+instance : (geometrically P).IsStableUnderBaseChange := by
+  rw [geometrically_eq_universally]
+  infer_instance
+
+instance [P.IsClosedUnderIsomorphisms] : IsZariskiLocalAtTarget (geometrically P) := by
+  rw [geometrically_eq_universally]
+  refine universally_isZariskiLocalAtTarget _ fun {X} Y f ι U hU H _ _ ↦ ?_
+  obtain ⟨y⟩ := (inferInstance : Nonempty Y)
+  obtain ⟨i, hy⟩ := hU.exists_mem y
+  have heq : U i = ⊤ := eq_top_iff.mpr fun z _ ↦ by rwa [Subsingleton.elim z y]
+  let e : ↑(U i) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
+  let e' : ↑(f ⁻¹ᵁ U i) ≅ X := X.isoOfEq (by simp [heq]) ≪≫ X.topIso
+  exact P.prop_of_iso e' <| H i (.of_isIso e.inv) (e.hom.homeomorph.subsingleton_congr.mpr ‹_›)
+
+section geometrically
+
+variable {P : ObjectProperty Scheme.{u}} {X Y : Scheme.{u}} {f : X ⟶ Y}
+
+lemma pullback_of_geometrically (hf : geometrically P f) (K : Type u) [Field K]
+    (y : Spec (.of K) ⟶ Y) : P (Limits.pullback f y) :=
+  hf _ _ _ (.of_hasPullback _ _)
+
+lemma pullback_of_geometrically' (hf : geometrically P f) (K : Type u) [Field K]
+    (y : Spec (.of K) ⟶ Y) : P (Limits.pullback y f) :=
+  hf _ _ _ (.flip <| .of_hasPullback _ _)
+
+lemma geometrically_iff_of_isClosedUnderIsomorphisms [P.IsClosedUnderIsomorphisms] :
+    geometrically P f ↔
+      ∀ (K : Type u) [Field K] (y : Spec (.of K) ⟶ Y), P (Limits.pullback f y) := by
+  refine ⟨fun h K _ _ ↦ pullback_of_geometrically h _ _, fun H K _ _ Y fst snd h ↦ ?_⟩
+  exact P.prop_of_iso h.isoPullback.symm (H _ _)
+
+lemma fiber_of_geometrically (hf : geometrically P f) (y : Y) : P (f.fiber y) :=
+  pullback_of_geometrically hf _ _
+
+/-- `P` holds geometrically for `f` if and only if all fibers are geometrically `P`. -/
+lemma geometrically_iff_forall_fiberToSpecResidueField :
+    geometrically P f ↔ ∀ (y : Y), geometrically P (f.fiberToSpecResidueField y) := by
+  refine ⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun H ↦ ?_⟩
+  intro K _ y Z fst snd h
+  obtain ⟨⟨y, φ⟩, rfl⟩ := (Scheme.SpecToEquivOfField _ _).symm.surjective y
+  let p : Z ⟶ f.fiber y :=
+    pullback.lift fst (snd ≫ Spec.map φ) (by simp [h.w, Scheme.SpecToEquivOfField])
+  apply H y (Spec.map φ) p snd
+  simp only [Scheme.SpecToEquivOfField, Equiv.coe_fn_symm_mk] at h
+  refine .flip (.of_bot (.flip ?_) ?_ (IsPullback.of_hasPullback f (Y.fromSpecResidueField y)).flip)
+  · convert h
+    simp [p]
+  · simp [p, Scheme.Hom.fiberToSpecResidueField]
+
+/-- This holds in particular if `Y = Spec K`. -/
+lemma self_of_isIntegral_of_geometrically [IsIntegral Y] [Subsingleton Y] (hf : geometrically P f) :
+    P X := by
+  rw [geometrically_eq_universally] at hf
+  exact MorphismProperty.universally_le _ _ hf ‹_› ‹_›
+
+variable {P : ObjectProperty Scheme.{u}} {R : Type u} [CommRing R] {f : X ⟶ Spec (.of R)}
+
+lemma geometrically_iff_of_commRing :
+    geometrically P f ↔ ∀ ⦃K : Type u⦄ [Field K] [Algebra R K] ⦃Y : Scheme.{u}⦄ (fst : Y ⟶ X)
+      (snd : Y ⟶ Spec (.of K)), IsPullback fst snd f (Spec.map <| ofHom (algebraMap R K)) →
+      P Y := by
+  refine ⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩
+  obtain ⟨φ, rfl⟩ := Spec.map_surjective y
+  algebraize [φ.hom]
+  exact H fst snd h
+
+lemma geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms [P.IsClosedUnderIsomorphisms] :
+    geometrically P f ↔ ∀ (K : Type u) [Field K] [Algebra R K],
+      P (Limits.pullback f (Spec.map <| ofHom <| algebraMap R K)) := by
+  refine ⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩
+  rw [geometrically_iff_of_isClosedUnderIsomorphisms]
+  intro K _ y
+  obtain ⟨φ, rfl⟩ := Spec.map_surjective y
+  algebraize [φ.hom]
+  exact H K
+
+end geometrically
+
+end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

@@ -76,7 +76,8 @@ lemma Surjective.of_comp [Surjective (f ≫ g)] : Surjective g where
 lemma Surjective.comp_iff [Surjective f] : Surjective (f ≫ g) ↔ Surjective g :=
   ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩
 
-instance : MorphismProperty.IsStableUnderComposition @Surjective.{u} where
+instance : MorphismProperty.IsMultiplicative @Surjective.{u} where
+  id_mem _ := inferInstance
   comp_mem _ _ hf hg := ⟨hg.1.comp hf.1⟩
 
 instance : MorphismProperty.RespectsIso @Surjective :=

Mathlib/AlgebraicGeometry/Properties.lean

@@ -6,6 +6,7 @@ Authors: Andrew Yang
 module
 
 public import Mathlib.AlgebraicGeometry.AffineScheme
+public import Mathlib.AlgebraicGeometry.Limits
 public import Mathlib.RingTheory.LocalProperties.Reduced
 
 /-!
@@ -280,6 +281,11 @@ theorem isIntegral_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmers
   exact (asIso <| f.app (f ''ᵁ U) :
     Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
 
+lemma IsIntegral.of_isIso {X Y : Scheme.{u}} [h : IsIntegral X] (f : X ⟶ Y) [IsIso f] :
+    IsIntegral Y := by
+  suffices Nonempty Y from isIntegral_of_isOpenImmersion (inv f)
+  exact Nonempty.map f inferInstance
+
 instance {R : CommRingCat} [IsDomain R] : IrreducibleSpace (Spec R) := by
   convert PrimeSpectrum.irreducibleSpace (R := R)
 
@@ -312,4 +318,9 @@ instance [IsIntegral X] : OrderTop X where
   top := genericPoint X
   le_top a := genericPoint_specializes a
 
+lemma isField_of_isIntegral_of_subsingleton (X : Scheme.{u}) [IsIntegral X] [Subsingleton X] :
+    IsField Γ(X, ⊤) := by
+  rw [← PrimeSpectrum.t1Space_iff_isField]
+  apply X.isoSpec.hom.homeomorph.t1Space
+
 end AlgebraicGeometry

Mathlib/Topology/Irreducible.lean

@@ -471,3 +471,16 @@ lemma IsDiscrete.subsingleton_of_isPreirreducible (hs : IsDiscrete s) (hs' : IsP
   exact (hUx.le (by grind)).symm.trans (b := z) (hVy.le (by grind))
 
 end Preirreducible
+
+lemma Function.Surjective.preirreducibleSpace {f : X → Y} (hfc : Continuous f)
+    (hf : Function.Surjective f) [PreirreducibleSpace X] : PreirreducibleSpace Y where
+  isPreirreducible_univ := by
+    rw [← hf.range_eq, ← Set.image_univ]
+    exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn
+
+lemma Function.Surjective.irreducibleSpace {f : X → Y} (hfc : Continuous f)
+    (hf : Function.Surjective f) [IrreducibleSpace X] : IrreducibleSpace Y where
+  isPreirreducible_univ := by
+    rw [← hf.range_eq, ← Set.image_univ]
+    exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn
+  toNonempty := Nonempty.map f inferInstance