feat(AlgebraicGeometry): universal property of relative normalization (leanprover-community#33476)

Author: erdOne

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -363,6 +363,12 @@ lemma Scheme.Opens.toSpecΓ_naturality {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens
     eqToHom_op, Hom.app_eq_appLE, Category.assoc, ← Spec.map_comp, Hom.appLE_map,
     toSpecΓ_naturality_assoc, TopologicalSpace.Opens.map_top, morphismRestrict_appLE, Hom.map_appLE]
 
+@[reassoc (attr := simp)]
+lemma Scheme.Opens.toSpecΓ_SpecMap_appLE
+    {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (hUV) :
+    V.toSpecΓ ≫ Spec.map (f.appLE U V hUV) = f.resLE U V hUV ≫ U.toSpecΓ := by
+  simp [Hom.appLE, Hom.resLE]
+
 namespace IsAffineOpen
 
 variable {X Y : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (f : Γ(X, U))
@@ -998,6 +1004,22 @@ theorem of_affine_open_cover {X : Scheme} {P : X.affineOpens → Prop}
   rw [iSup_range', SetLike.mem_coe, Opens.mem_iSup]
   exact ⟨_, hf₁ ⟨x, hx⟩⟩
 
+/-- If `φ` is a monomorphism in `CommRingCat`, it is not in general true that `Spec φ` is epi.
+(`ℤ ⊆ ℤ[1/2]` but `Spec ℤ[1/2] ⟶ Spec ℤ` is not epi, since epi open immersions are isomorphisms)
+But if the range of `f g : Spec R ⟶ X` are contained in an common affine open `U`, one can still
+cancel `Spec.map φ ≫ f = Spec.map φ ≫ g` to get `f = g`. -/
+lemma eq_of_SpecMap_comp_eq_of_isAffineOpen {R S : CommRingCat} {X : Scheme}
+    (φ : R ⟶ S) (hφ : Function.Injective φ)
+    {f g : Spec R ⟶ X} (U : X.Opens) (hU : IsAffineOpen U) (hUf : f ⁻¹ᵁ U = ⊤) (hUg : g ⁻¹ᵁ U = ⊤)
+    (H : Spec.map φ ≫ f = Spec.map φ ≫ g) : f = g := by
+  have : Mono φ := ConcreteCategory.mono_of_injective _ hφ
+  rw [← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),
+    ← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)]
+  congr 1
+  rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
+    ← cancel_mono φ, ← Spec.map_injective.eq_iff]
+  simp [← cancel_mono U.ι, H]
+
 section ZeroLocus
 
 namespace Scheme

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -52,6 +52,10 @@ theorem quasiCompact_iff_isSpectralMap : QuasiCompact f ↔ IsSpectralMap f :=
 theorem Scheme.Hom.isSpectralMap [QuasiCompact f] : IsSpectralMap f := by
   rwa [← quasiCompact_iff_isSpectralMap]
 
+lemma Scheme.Hom.isCompact_preimage [QuasiCompact f] {U : Opens Y}
+    (hU : IsCompact (U : Set Y)) : IsCompact (f ⁻¹ᵁ U : Set X) :=
+  f.isSpectralMap.2 U.2 hU
+
 @[deprecated (since := "2025-10-07")]
 alias quasiCompact_iff_spectral := quasiCompact_iff_isSpectralMap
 

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -159,6 +159,12 @@ theorem quasiSeparatedSpace_of_quasiSeparated (f : X ⟶ Y)
   rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]
   infer_instance
 
+lemma Scheme.Hom.isQuasiSeparated_preimage [QuasiSeparated f] {U : Opens Y}
+    (hU : IsQuasiSeparated (U : Set Y)) : IsQuasiSeparated (f ⁻¹ᵁ U : Set X) := by
+  have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
+  exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
+    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))
+
 instance quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] : QuasiSeparatedSpace X :=
   (quasiSeparatedSpace_congr X.isoSpec.hom.homeomorph).2 PrimeSpectrum.instQuasiSeparatedSpace
 

Mathlib/AlgebraicGeometry/Normalization.lean

@@ -17,8 +17,12 @@ along with the maps that `f` factor into:
 - `f.toNormalization : X ⟶ f.normalization`: a dominant morphism
 - `f.fromNormalization : f.normalization ⟶ Y`: an integral morphism
 
-## TODO
-- show the universal property of relative normalization
+It satisfies the universal property:
+For any factorization `X ⟶ T ⟶ Y` with `T ⟶ Y` integral,
+the map `X ⟶ T` factors through `f.normalization` uniquely.
+The factorization map is `AlgebraicGeometry.Scheme.Hom.normalizationDesc`, and the uniqueness result
+is `AlgebraicGeometry.Scheme.Hom.normalization.hom_ext`.
+
 -/
 
 @[expose] public noncomputable section
@@ -64,16 +68,6 @@ def normalizationDiagramMap : Y.presheaf ⟶ f.normalizationDiagram where
       CommRingCat.ofHom (algebraMap Γ(Y, U.unop) (integralClosure Γ(Y, U.unop) Γ(X, f ⁻¹ᵁ U.unop)))
     naturality {U V} i := by ext x; exact Subtype.ext congr($(f.naturality i) x)
 
-lemma isCompact_preimage [QuasiCompact f] {U : Opens Y}
-    (hU : IsCompact (U : Set Y)) : IsCompact (f ⁻¹ᵁ U : Set X) :=
-  f.isSpectralMap.2 U.2 hU
-
-lemma isQuasiSeparated_preimage [QuasiSeparated f] {U : Opens Y}
-    (hU : IsQuasiSeparated (U : Set Y)) : IsQuasiSeparated (f ⁻¹ᵁ U : Set X) := by
-  have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
-  exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
-    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))
-
 variable [QuasiCompact f] [QuasiSeparated f]
 
 lemma preservesLocalization_normalizationDiagramMap :
@@ -312,4 +306,120 @@ instance [IsIntegral X] : IsIntegral f.normalization :=
     simpa using f.toNormalization.denseRange.closure_range.symm
   isIntegral_of_irreducibleSpace_of_isReduced _
 
+section UniversalProperty
+
+variable {T : Scheme.{u}} (f₁ : X ⟶ T) (f₂ : T ⟶ Y) [IsIntegralHom f₂]
+
+/-- Given an qcqs morphism `f : X ⟶ Y`, which factors into `X ⟶ T ⟶ Y` with `T ⟶ Y` integral,
+the map `X ⟶ T` factors through `f.normalization` uniquely.
+(See `normalization.hom_ext` for the uniqueness result) -/
+noncomputable
+def normalizationDesc (H : f = f₁ ≫ f₂) : f.normalization ⟶ T := by
+  refine colimit.desc _
+    { pt := _
+      ι.app U := Spec.map (CommRingCat.ofHom ((f₁.appLE _ _ (by simp [H])).hom.codRestrict _
+        fun x ↦ ?_)) ≫ (U.2.preimage f₂).fromSpec,
+      ι.naturality := ?_ }
+  · algebraize [(f.app U.1).hom, (f₂.app U.1).hom,
+      (f₁.appLE (f₂ ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) (by simp [H])).hom]
+    have : IsScalarTower Γ(Y, U.1) Γ(T, f₂ ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ U.1) := .of_algebraMap_eq' <| by
+      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
+        Hom.app_eq_appLE, Hom.appLE_comp_appLE, ← H]
+    exact .algebraMap (R := Γ(Y, U.1)) (B := Γ(X, f ⁻¹ᵁ U.1)) (f₂.isIntegral_app U.1 U.2 x)
+  · intros U V i
+    dsimp
+    rw [Category.comp_id, ← Spec.map_comp_assoc, ← (V.2.preimage f₂).map_fromSpec (U.2.preimage f₂)
+      (homOfLE (f₂.preimage_mono (Scheme.AffineZariskiSite.toOpens_mono i.le))).op,
+      ← Spec.map_comp_assoc]
+    congr 2
+    ext i
+    apply Subtype.ext
+    dsimp [normalizationDiagram]
+    simp only [← CommRingCat.comp_apply, appLE_map, map_appLE]
+
+@[reassoc (attr := simp)]
+lemma toNormalization_normalizationDesc (H : f = f₁ ≫ f₂) :
+    f.toNormalization ≫ f.normalizationDesc f₁ f₂ H = f₁ := by
+  refine Scheme.Cover.hom_ext (X.openCoverOfIsOpenCover _
+    (.comap (iSup_affineOpens_eq_top Y) f.base.hom)) _ _ fun U ↦ ?_
+  letI := (f.app U.1).hom.toAlgebra
+  refine (Scheme.Hom.ι_toNormalization_assoc ..).trans ?_
+  dsimp [normalizationOpenCover, normalizationDesc]
+  simp only [colimit.ι_desc, ← Spec.map_comp_assoc]
+  change (f ⁻¹ᵁ U.1).toSpecΓ ≫ Spec.map (f₁.appLE (f₂ ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) (by simp [H])) ≫
+    (U.2.preimage f₂).fromSpec = (f ⁻¹ᵁ U.1).ι ≫ f₁
+  simp
+
+@[reassoc (attr := simp)]
+lemma normalizationDesc_comp (H : f = f₁ ≫ f₂) :
+    f.normalizationDesc f₁ f₂ H ≫ f₂ = f.fromNormalization := by
+  refine colimit.hom_ext fun U ↦ ?_
+  dsimp [normalizationDesc, fromNormalization]
+  rw [colimit.ι_desc_assoc, colimit.ι_desc, Category.assoc,
+    ← IsAffineOpen.SpecMap_appLE_fromSpec _ U.2 _ le_rfl, ← Spec.map_comp_assoc]
+  congr 2
+  ext i
+  dsimp [normalizationDiagram, normalizationDiagramMap, RingHom.algebraMap_toAlgebra]
+  rw [← CommRingCat.comp_apply, Hom.appLE_comp_appLE, app_eq_appLE]
+  simp_rw [H]
+
+instance (H : f = f₁ ≫ f₂) : IsIntegralHom (f.normalizationDesc f₁ f₂ H) := by
+  have : IsIntegralHom (f.normalizationDesc f₁ f₂ H ≫ f₂) := by
+    rw [f.normalizationDesc_comp]; infer_instance
+  exact .of_comp _ f₂
+
+/-- The uniqueness part of the universal property for relative normalization.
+Suppose `f : X ⟶ Y` is qcqs and factors into `X ⟶ T ⟶ Y` with `T ⟶ Y` affine, then
+there is at most one map `f.normalization ⟶ T` that commutes with them. -/
+lemma normalization.hom_ext (f₁ f₂ : f.normalization ⟶ T) (g : T ⟶ Y) [IsAffineHom g]
+    (H₁ : f.toNormalization ≫ f₁ = f.toNormalization ≫ f₂)
+    (hf₁ : f₁ ≫ g = f.fromNormalization) (hf₂ : f₂ ≫ g = f.fromNormalization) : f₁ = f₂ := by
+  apply f.normalizationOpenCover.hom_ext _ _ fun U ↦ ?_
+  let := (f.app U.1).hom.toAlgebra
+  have : IsAffineHom f₁ := have : IsAffineHom (f₁ ≫ g) := hf₁ ▸ inferInstance; .of_comp _ g
+  have : IsAffineHom f₂ := have : IsAffineHom (f₂ ≫ g) := hf₂ ▸ inferInstance; .of_comp _ g
+  let f₀ := toNormalization f ≫ f₁
+  have hf₀ : f₀ = toNormalization f ≫ f₂ := H₁
+  refine eq_of_SpecMap_comp_eq_of_isAffineOpen
+    (CommRingCat.ofHom (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom)
+    Subtype.val_injective _ (U.2.preimage g) ?_ ?_ ?_
+  · simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₁, ι_fromNormalization]; simp
+  · simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₂, ι_fromNormalization]; simp
+  · have h₁ : f ⁻¹ᵁ U.1 ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
+      simp only [← Scheme.Hom.comp_preimage, f₀, Category.assoc,
+        hf₁, toNormalization_fromNormalization]; rfl
+    have h₁' : f ⁻¹ᵁ U.1 = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
+      simp only [← Scheme.Hom.comp_preimage, hf₂, toNormalization_fromNormalization]
+    have h₂ : fromNormalization f ⁻¹ᵁ U.1 = f₁ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
+      simp only [← Scheme.Hom.comp_preimage, hf₁]
+    have h₂' : fromNormalization f ⁻¹ᵁ U.1 = f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1 := by
+      simp only [← Scheme.Hom.comp_preimage, hf₂]
+    have h₃ : f ⁻¹ᵁ U.1 = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U.1 := by
+      simp [← Scheme.Hom.comp_preimage]
+    trans Spec.map (f₀.appLE _ _ h₁) ≫ (U.2.preimage g).fromSpec
+    · simp only [AlgHom.toRingHom_eq_coe, comp_appLE, Spec.map_comp, Category.assoc, f₀,
+        app_eq_appLE]
+      rw [IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]
+      have : (toNormalization f).appLE (f₁ ⁻¹ᵁ g ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) h₁ =
+        f.normalization.presheaf.map (eqToHom h₂).op ≫
+        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.1) ≫
+          X.presheaf.map (eqToHom h₃).op := by
+        simp [app_eq_appLE]
+      rw [this, f.toNormalization_app_preimage U]
+      simp [appIso_hom', IsAffineOpen.SpecMap_appLE_fromSpec_assoc _ _ (isAffineOpen_top (Spec _)),
+        IsAffineOpen.fromSpec_top]
+    · simp only [AlgHom.toRingHom_eq_coe, hf₀, comp_appLE, Spec.map_comp, Category.assoc,
+        app_eq_appLE]
+      rw [IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]
+      have : (toNormalization f).appLE (f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) h₁'.le =
+        f.normalization.presheaf.map (eqToHom h₂').op ≫
+        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.1) ≫
+          X.presheaf.map (eqToHom h₃).op := by
+        simp [app_eq_appLE]
+      rw [this, f.toNormalization_app_preimage U]
+      simp [appIso_hom', IsAffineOpen.SpecMap_appLE_fromSpec_assoc _ _ (isAffineOpen_top (Spec _)),
+        IsAffineOpen.fromSpec_top]
+
+end UniversalProperty
+
 end AlgebraicGeometry.Scheme.Hom