[Merged by Bors] - feat(AlgebraicGeometry): define integral morphisms

Mathlib.lean

@@ -937,6 +937,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Finite
 import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.Morphisms.Immersion
+import Mathlib.AlgebraicGeometry.Morphisms.Integral
 import Mathlib.AlgebraicGeometry.Morphisms.IsIso
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

@@ -3,9 +3,8 @@ Copyright (c) 2024 Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
-import Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
-import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
-import Mathlib.RingTheory.RingHom.Finite
+import Mathlib.AlgebraicGeometry.Morphisms.Integral
+import Mathlib.Algebra.Category.Ring.Epi
 
 /-!
 
@@ -65,15 +64,52 @@ instance (priority := 900) [IsIso f] : IsFinite f := of_isIso @IsFinite f
 instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsFinite f] [IsFinite g] : IsFinite (f ≫ g) :=
   IsStableUnderComposition.comp_mem f g ‹IsFinite f› ‹IsFinite g›
 
-instance (priority := 900) [hf : IsFinite f] : LocallyOfFiniteType f := by
-  have : targetAffineLocally (affineAnd @RingHom.FiniteType) f := by
-    rw [HasAffineProperty.eq_targetAffineLocally (P := @IsFinite)] at hf
-    apply targetAffineLocally_affineAnd_le RingHom.Finite.finiteType
-    exact hf
-  rw [targetAffineLocally_affineAnd_eq_affineLocally
-    (HasRingHomProperty.isLocal_ringHomProperty @LocallyOfFiniteType)] at this
-  rw [HasRingHomProperty.eq_affineLocally (P := @LocallyOfFiniteType)]
-  exact this.2
+lemma iff_isIntegralHom_and_locallyOfFiniteType :
+    IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f := by
+  wlog hY : IsAffine Y
+  · rw [IsLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
+      IsLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
+      IsLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
+    simp_rw [this, forall_and]
+  rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite),
+    HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
+    RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]
+  refine and_congr_right fun ⟨_, _⟩ ↦
+    (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm
+
+lemma eq_inf :
+    @IsFinite = (@IsIntegralHom ⊓ @LocallyOfFiniteType : MorphismProperty Scheme) := by
+  ext; exact IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _
+
+instance (priority := 900) [IsFinite f] : IsIntegralHom f :=
+  ((IsFinite.iff_isIntegralHom_and_locallyOfFiniteType f).mp ‹_›).1
+
+instance (priority := 900) [hf : IsFinite f] : LocallyOfFiniteType f :=
+  ((IsFinite.iff_isIntegralHom_and_locallyOfFiniteType f).mp ‹_›).2
+
+lemma _root_.AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono :
+    IsClosedImmersion f ↔ IsFinite f ∧ Mono f := by
+  wlog hY : IsAffine Y
+  · show _ ↔ _ ∧ monomorphisms _ f
+    rw [IsLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
+      IsLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) Y.affineCover,
+      IsLocalAtTarget.iff_of_openCover (P := monomorphisms _) Y.affineCover]
+    simp_rw [this, forall_and, monomorphisms]
+  rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),
+    HasAffineProperty.iff_of_isAffine (P := @IsFinite),
+    RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]
+  refine and_congr_right fun ⟨_, _⟩ ↦
+    Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)
+  trans Mono (f.app ⊤).op
+  · exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩
+  exact (Functor.mono_map_iff_mono Scheme.Spec _).symm
+
+lemma _root_.AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono :
+    @IsClosedImmersion = (@IsFinite ⊓ monomorphisms Scheme : MorphismProperty _) := by
+  ext; exact IsClosedImmersion.iff_isFinite_and_mono _
+
+instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsFinite f :=
+  ((IsClosedImmersion.iff_isFinite_and_mono f).mp ‹_›).1
 
 end IsFinite
 

Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
+import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
+import Mathlib.RingTheory.RingHom.Integral
+
+/-!
+
+# Integral morphisms of schemes
+
+A morphism of schemes `f : X ⟶ Y` is integral if the preimage
+of an arbitrary affine open subset of `Y` is affine and the induced ring map is integral.
+
+It is equivalent to ask only that `Y` is covered by affine opens whose preimage is affine
+and the induced ring map is integral.
+
+## TODO
+
+- Show integral = universally closed + affine
+
+-/
+
+universe v u
+
+open CategoryTheory TopologicalSpace Opposite MorphismProperty
+
+namespace AlgebraicGeometry
+
+/-- A morphism of schemes `X ⟶ Y` is finite if
+the preimage of any affine open subset of `Y` is affine and the induced ring
+hom is finite. -/
+@[mk_iff]
+class IsIntegralHom {X Y : Scheme} (f : X ⟶ Y) extends IsAffineHom f : Prop where
+  integral_app (U : Y.Opens) (hU : IsAffineOpen U) : (f.app U).IsIntegral
+
+namespace IsIntegralHom
+
+instance hasAffineProperty : HasAffineProperty @IsIntegralHom
+    fun X _ f _ ↦ IsAffine X ∧ RingHom.IsIntegral (f.app ⊤) := by
+  show HasAffineProperty @IsIntegralHom (affineAnd RingHom.IsIntegral)
+  rw [HasAffineProperty.affineAnd_iff _ RingHom.isIntegral_respectsIso
+    RingHom.isIntegral_isStableUnderBaseChange.localizationPreserves
+    RingHom.isIntegral_ofLocalizationSpan]
+  simp [isIntegralHom_iff]
+
+instance : IsStableUnderComposition @IsIntegralHom :=
+  HasAffineProperty.affineAnd_isStableUnderComposition (Q := RingHom.IsIntegral) hasAffineProperty
+    RingHom.isIntegral_stableUnderComposition
+
+instance : IsStableUnderBaseChange @IsIntegralHom :=
+  HasAffineProperty.affineAnd_isStableUnderBaseChange (Q := RingHom.IsIntegral) hasAffineProperty
+    RingHom.isIntegral_respectsIso RingHom.isIntegral_isStableUnderBaseChange
+
+instance : ContainsIdentities @IsIntegralHom :=
+  ⟨fun X ↦ ⟨fun _ _ ↦ by simpa using RingHom.isIntegral_of_surjective _ (Equiv.refl _).surjective⟩⟩
+
+instance : IsMultiplicative @IsIntegralHom where
+
+end IsIntegralHom
+
+end AlgebraicGeometry

Mathlib/RingTheory/RingHom/Integral.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.RingHomProperties
-import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
+import Mathlib.RingTheory.LocalProperties.Basic
+import Mathlib.RingTheory.Localization.Integral
 
 /-!
 
@@ -36,4 +36,32 @@ theorem isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun f => f.
   · intro x y; exact IsIntegral.tmul x (h y)
   · intro x y hx hy; exact IsIntegral.add hx hy
 
+open Polynomial in
+/-- `S` is an integral `R`-algebra if there exists a set `{ r }` that
+  spans `R` such that each `Sᵣ` is an integral `Rᵣ`-algebra. -/
+theorem isIntegral_ofLocalizationSpan :
+    OfLocalizationSpan (RingHom.IsIntegral ·) := by
+  introv R hs H r
+  letI := f.toAlgebra
+  show r ∈ (integralClosure R S).toSubmodule
+  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hs
+  rintro ⟨t, ht⟩
+  letI := (Localization.awayMap f t).toAlgebra
+  haveI : IsScalarTower R (Localization.Away t) (Localization.Away (f t)) := .of_algebraMap_eq'
+    (IsLocalization.lift_comp _).symm
+  have : _root_.IsIntegral (Localization.Away t) (algebraMap S (Localization.Away (f t)) r) :=
+    H ⟨t, ht⟩ (algebraMap _ _ r)
+  obtain ⟨⟨_, n, rfl⟩, p, hp, hp'⟩ := this.exists_multiple_integral_of_isLocalization (.powers t)
+  rw [IsScalarTower.algebraMap_eq R S, Submonoid.smul_def, Algebra.smul_def,
+    IsScalarTower.algebraMap_apply R S, ← map_mul, ← hom_eval₂,
+    IsLocalization.map_eq_zero_iff (.powers (f t))] at hp'
+  obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp'
+  by_cases hp' : 1 ≤ p.natDegree; swap
+  · obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by nlinarith)
+    exact ⟨m, by simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]⟩
+  refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩
+  have := p.scaleRoots_eval₂_mul (algebraMap R S) (t ^ n • r) (t ^ m)
+  simp only [pow_add, ← Algebra.smul_def, mul_smul, ← map_pow] at e this ⊢
+  rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
+
 end RingHom