From 22092a2aaa2dc2a12f20161a54f315fafeb748f3 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Sun, 14 Apr 2024 18:26:07 +0000
Subject: [PATCH] chore(RingTheory/FinitePresentation): make
 `Algebra.FinitePresentation` a class (#12057)

Makes `Algebra.FinitePresentation` a class, matching `Algebra.FiniteType`. Changes theorems to instances where possible.
---
 Mathlib/RingTheory/FinitePresentation.lean | 104 ++++++++++++---------
 1 file changed, 61 insertions(+), 43 deletions(-)

diff --git a/Mathlib/RingTheory/FinitePresentation.lean b/Mathlib/RingTheory/FinitePresentation.lean
index c5ef763451788..0397cf8dbd8b2 100644
--- a/Mathlib/RingTheory/FinitePresentation.lean
+++ b/Mathlib/RingTheory/FinitePresentation.lean
@@ -40,8 +40,8 @@ variable (R : Type w₁) (A : Type w₂) (B : Type w₃)
 
 /-- An algebra over a commutative semiring is `Algebra.FinitePresentation` if it is the quotient of
 a polynomial ring in `n` variables by a finitely generated ideal. -/
-def Algebra.FinitePresentation [CommSemiring R] [Semiring A] [Algebra R A] : Prop :=
-  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Surjective f ∧ f.toRingHom.ker.FG
+class Algebra.FinitePresentation [CommSemiring R] [Semiring A] [Algebra R A] : Prop where
+  out : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A), Surjective f ∧ f.toRingHom.ker.FG
 #align algebra.finite_presentation Algebra.FinitePresentation
 
 namespace Algebra
@@ -53,8 +53,8 @@ namespace FiniteType
 variable {R A B}
 
 /-- A finitely presented algebra is of finite type. -/
-theorem of_finitePresentation : FinitePresentation R A → FiniteType R A := by
-  rintro ⟨n, f, hf⟩
+instance of_finitePresentation [FinitePresentation R A] : FiniteType R A := by
+  obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
   apply FiniteType.iff_quotient_mvPolynomial''.2
   exact ⟨n, f, hf.1⟩
 #align algebra.finite_type.of_finite_presentation Algebra.FiniteType.of_finitePresentation
@@ -68,7 +68,7 @@ variable {R A B}
 /-- An algebra over a Noetherian ring is finitely generated if and only if it is finitely
 presented. -/
 theorem of_finiteType [IsNoetherianRing R] : FiniteType R A ↔ FinitePresentation R A := by
-  refine' ⟨fun h => _, Algebra.FiniteType.of_finitePresentation⟩
+  refine' ⟨fun h => _, fun hfp => Algebra.FiniteType.of_finitePresentation⟩
   obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h
   refine' ⟨n, f, hf, _⟩
   have hnoet : IsNoetherianRing (MvPolynomial (Fin n) R) := by infer_instance
@@ -80,8 +80,8 @@ theorem of_finiteType [IsNoetherianRing R] : FiniteType R A ↔ FinitePresentati
 #align algebra.finite_presentation.of_finite_type Algebra.FinitePresentation.of_finiteType
 
 /-- If `e : A ≃ₐ[R] B` and `A` is finitely presented, then so is `B`. -/
-theorem equiv (hfp : FinitePresentation R A) (e : A ≃ₐ[R] B) : FinitePresentation R B := by
-  obtain ⟨n, f, hf⟩ := hfp
+theorem equiv [FinitePresentation R A] (e : A ≃ₐ[R] B) : FinitePresentation R B := by
+  obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
   use n, AlgHom.comp (↑e) f
   constructor
   · rw [AlgHom.coe_comp]
@@ -102,45 +102,49 @@ theorem equiv (hfp : FinitePresentation R A) (e : A ≃ₐ[R] B) : FinitePresent
 variable (R)
 
 /-- The ring of polynomials in finitely many variables is finitely presented. -/
-protected theorem mvPolynomial (ι : Type u_2) [Finite ι] :
-    FinitePresentation R (MvPolynomial ι R) := by
-  cases nonempty_fintype ι
-  let eqv := (MvPolynomial.renameEquiv R <| Fintype.equivFin ι).symm
-  exact
-    ⟨Fintype.card ι, eqv, eqv.surjective,
-      ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩
+protected instance mvPolynomial (ι : Type u_2) [Finite ι] :
+    FinitePresentation R (MvPolynomial ι R) where
+  out := by
+    cases nonempty_fintype ι
+    let eqv := (MvPolynomial.renameEquiv R <| Fintype.equivFin ι).symm
+    exact
+      ⟨Fintype.card ι, eqv, eqv.surjective,
+        ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩
 #align algebra.finite_presentation.mv_polynomial Algebra.FinitePresentation.mvPolynomial
 
 /-- `R` is finitely presented as `R`-algebra. -/
-theorem self : FinitePresentation R R :=
+instance self : FinitePresentation R R :=
   -- Porting note: replaced `PEmpty` with `Empty`
-  equiv (FinitePresentation.mvPolynomial R Empty) (MvPolynomial.isEmptyAlgEquiv R Empty)
+  equiv (MvPolynomial.isEmptyAlgEquiv R Empty)
 #align algebra.finite_presentation.self Algebra.FinitePresentation.self
 
 /-- `R[X]` is finitely presented as `R`-algebra. -/
-theorem polynomial : FinitePresentation R R[X] :=
+instance polynomial : FinitePresentation R R[X] :=
   -- Porting note: replaced `PUnit` with `Unit`
-  equiv (FinitePresentation.mvPolynomial R Unit) (MvPolynomial.pUnitAlgEquiv R)
+  letI := FinitePresentation.mvPolynomial R Unit
+  equiv (MvPolynomial.pUnitAlgEquiv R)
 #align algebra.finite_presentation.polynomial Algebra.FinitePresentation.polynomial
 
 variable {R}
 
 /-- The quotient of a finitely presented algebra by a finitely generated ideal is finitely
 presented. -/
-protected theorem quotient {I : Ideal A} (h : I.FG) (hfp : FinitePresentation R A) :
-    FinitePresentation R (A ⧸ I) := by
-  obtain ⟨n, f, hf⟩ := hfp
-  refine' ⟨n, (Ideal.Quotient.mkₐ R I).comp f, _, _⟩
-  · exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1
-  · refine' Ideal.fg_ker_comp _ _ hf.2 _ hf.1
-    simp [h]
+protected theorem quotient {I : Ideal A} (h : I.FG) [FinitePresentation R A] :
+    FinitePresentation R (A ⧸ I) where
+  out := by
+    obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
+    refine' ⟨n, (Ideal.Quotient.mkₐ R I).comp f, _, _⟩
+    · exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1
+    · refine' Ideal.fg_ker_comp _ _ hf.2 _ hf.1
+      simp [h]
 #align algebra.finite_presentation.quotient Algebra.FinitePresentation.quotient
 
 /-- If `f : A →ₐ[R] B` is surjective with finitely generated kernel and `A` is finitely presented,
 then so is `B`. -/
 theorem of_surjective {f : A →ₐ[R] B} (hf : Function.Surjective f) (hker : f.toRingHom.ker.FG)
-    (hfp : FinitePresentation R A) : FinitePresentation R B :=
-  equiv (hfp.quotient hker) (Ideal.quotientKerAlgEquivOfSurjective hf)
+    [FinitePresentation R A] : FinitePresentation R B :=
+  letI : FinitePresentation R (A ⧸ RingHom.ker f) := FinitePresentation.quotient hker
+  equiv (Ideal.quotientKerAlgEquivOfSurjective hf)
 #align algebra.finite_presentation.of_surjective Algebra.FinitePresentation.of_surjective
 
 theorem iff :
@@ -150,7 +154,8 @@ theorem iff :
   · rintro ⟨n, f, hf⟩
     exact ⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩
   · rintro ⟨n, I, e, hfg⟩
-    exact equiv ((FinitePresentation.mvPolynomial R _).quotient hfg) e
+    letI := (FinitePresentation.mvPolynomial R _).quotient hfg
+    exact equiv e
 #align algebra.finite_presentation.iff Algebra.FinitePresentation.iff
 
 /-- An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose
@@ -185,9 +190,10 @@ theorem iff_quotient_mvPolynomial' :
 -- Porting note: make universe level explicit to ensure `ι, ι'` has the same universe level
 /-- If `A` is a finitely presented `R`-algebra, then `MvPolynomial (Fin n) A` is finitely presented
 as `R`-algebra. -/
-theorem mvPolynomial_of_finitePresentation (hfp : FinitePresentation.{w₁, w₂} R A)
+theorem mvPolynomial_of_finitePresentation [FinitePresentation.{w₁, w₂} R A]
     (ι : Type v) [Finite ι] :
     FinitePresentation.{w₁, max v w₂} R (MvPolynomial ι A) := by
+  have hfp : FinitePresentation.{w₁, w₂} R A := inferInstance
   rw [iff_quotient_mvPolynomial'] at hfp ⊢
   classical
   -- Porting note: use the same universe level
@@ -207,12 +213,17 @@ theorem mvPolynomial_of_finitePresentation (hfp : FinitePresentation.{w₁, w₂
     exact hf_ker.map MvPolynomial.C
 #align algebra.finite_presentation.mv_polynomial_of_finite_presentation Algebra.FinitePresentation.mvPolynomial_of_finitePresentation
 
+variable (R A B)
+
 /-- If `A` is an `R`-algebra and `S` is an `A`-algebra, both finitely presented, then `S` is
   finitely presented as `R`-algebra. -/
-theorem trans [Algebra A B] [IsScalarTower R A B] (hfpA : FinitePresentation R A)
-    (hfpB : FinitePresentation A B) : FinitePresentation R B := by
+theorem trans [Algebra A B] [IsScalarTower R A B] [FinitePresentation R A]
+    [FinitePresentation A B] : FinitePresentation R B := by
+  have hfpB : FinitePresentation A B := inferInstance
   obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB
-  exact equiv ((mvPolynomial_of_finitePresentation hfpA _).quotient hfg) (e.restrictScalars R)
+  letI : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) :=
+    (mvPolynomial_of_finitePresentation _).quotient hfg
+  exact equiv (e.restrictScalars R)
 #align algebra.finite_presentation.trans Algebra.FinitePresentation.trans
 
 open MvPolynomial
@@ -220,10 +231,10 @@ open MvPolynomial
 -- We follow the proof of https://stacks.math.columbia.edu/tag/0561
 -- TODO: extract out helper lemmas and tidy proof.
 theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A B]
-    (hRB : FinitePresentation.{w₁, w₃} R B) [hRA : FiniteType R A] :
+    [FinitePresentation.{w₁, w₃} R B] [FiniteType R A] :
     FinitePresentation.{w₂, w₃} A B := by
   classical
-  obtain ⟨n, f, hf, s, hs⟩ := hRB
+  obtain ⟨n, f, hf, s, hs⟩ := FinitePresentation.out (R := R) (A := B)
   letI RX := MvPolynomial (Fin n) R
   letI AX := MvPolynomial (Fin n) A
   refine' ⟨n, MvPolynomial.aeval (f ∘ X), _, _⟩
@@ -231,7 +242,7 @@ theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A
       Set.range_comp f MvPolynomial.X, eq_top_iff, ← @adjoin_adjoin_of_tower R A B,
       adjoin_image, adjoin_range_X, Algebra.map_top, (Algebra.range_top_iff_surjective _).mpr hf]
     exact fun {x} => subset_adjoin ⟨⟩
-  · obtain ⟨t, ht⟩ := hRA.out
+  · obtain ⟨t, ht⟩ := FiniteType.out (R := R) (A := A)
     have := fun i : t => hf (algebraMap A B i)
     choose t' ht' using this
     have ht'' : Algebra.adjoin R (algebraMap A AX '' t ∪ Set.range (X : _ → AX)) = ⊤ := by
@@ -305,12 +316,14 @@ theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A
     exact Set.mem_image_of_mem _ hx
 #align algebra.finite_presentation.of_restrict_scalars_finite_presentation Algebra.FinitePresentation.of_restrict_scalars_finitePresentation
 
+variable {R A B}
+
 -- TODO: extract out helper lemmas and tidy proof.
 /-- This is used to prove the strictly stronger `ker_fg_of_surjective`. Use it instead. -/
 theorem ker_fg_of_mvPolynomial {n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] A)
-    (hf : Function.Surjective f) (hfp : FinitePresentation R A) : f.toRingHom.ker.FG := by
+    (hf : Function.Surjective f) [FinitePresentation R A] : f.toRingHom.ker.FG := by
   classical
-    obtain ⟨m, f', hf', s, hs⟩ := hfp
+    obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)
     let RXn := MvPolynomial (Fin n) R
     let RXm := MvPolynomial (Fin m) R
     have := fun i : Fin n => hf' (f <| X i)
@@ -383,9 +396,9 @@ theorem ker_fg_of_mvPolynomial {n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] A
 /-- If `f : A →ₐ[R] B` is a surjection between finitely-presented `R`-algebras, then the kernel of
 `f` is finitely generated. -/
 theorem ker_fG_of_surjective (f : A →ₐ[R] B) (hf : Function.Surjective f)
-    (hRA : FinitePresentation R A) (hRB : FinitePresentation R B) : f.toRingHom.ker.FG := by
-  obtain ⟨n, g, hg, _⟩ := hRA
-  convert (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg) hRB).map g.toRingHom
+    [FinitePresentation R A] [FinitePresentation R B] : f.toRingHom.ker.FG := by
+  obtain ⟨n, g, hg, _⟩ := FinitePresentation.out (R := R) (A := A)
+  convert (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom
   simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
   rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]
 #align algebra.finite_presentation.ker_fg_of_surjective Algebra.FinitePresentation.ker_fG_of_surjective
@@ -428,12 +441,13 @@ theorem comp_surjective {f : A →+* B} {g : B →+* C} (hf : f.FinitePresentati
     (hker : g.ker.FG) : (g.comp f).FinitePresentation :=
   letI := f.toAlgebra
   letI := (g.comp f).toAlgebra
+  letI : Algebra.FinitePresentation A B := hf
   Algebra.FinitePresentation.of_surjective
     (f :=
       { g with
         toFun := g
         commutes' := fun _ => rfl })
-    hg hker hf
+    hg hker
 #align ring_hom.finite_presentation.comp_surjective RingHom.FinitePresentation.comp_surjective
 
 theorem of_surjective (f : A →+* B) (hf : Surjective f) (hker : f.ker.FG) :
@@ -454,7 +468,9 @@ theorem comp {g : B →+* C} {f : A →+* B} (hg : g.FinitePresentation) (hf : f
   letI ins3 := RingHom.toAlgebra (g.comp f)
   letI ins4 : IsScalarTower A B C :=
     { smul_assoc := fun a b c => by simp [Algebra.smul_def, mul_assoc]; rfl }
-  Algebra.FinitePresentation.trans hf hg
+  letI : Algebra.FinitePresentation A B := hf
+  letI : Algebra.FinitePresentation B C := hg
+  Algebra.FinitePresentation.trans A B C
 #align ring_hom.finite_presentation.comp RingHom.FinitePresentation.comp
 
 theorem of_comp_finiteType (f : A →+* B) {g : B →+* C} (hg : (g.comp f).FinitePresentation)
@@ -465,7 +481,9 @@ theorem of_comp_finiteType (f : A →+* B) {g : B →+* C} (hg : (g.comp f).Fini
   letI ins3 := RingHom.toAlgebra (g.comp f)
   letI ins4 : IsScalarTower A B C :=
     { smul_assoc := fun a b c => by simp [Algebra.smul_def, mul_assoc]; rfl }
-  Algebra.FinitePresentation.of_restrict_scalars_finitePresentation (hRA := hf) hg
+  letI : Algebra.FinitePresentation A C := hg
+  letI : Algebra.FiniteType A B := hf
+  Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C
 #align ring_hom.finite_presentation.of_comp_finite_type RingHom.FinitePresentation.of_comp_finiteType
 
 end FinitePresentation