feat(RingTheory): finite type and finite presentation are stable unde…

…r base change (#13696)

Mathlib.lean

@@ -3528,6 +3528,7 @@ import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Filtration
 import Mathlib.RingTheory.FinitePresentation
+import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Finiteness
 import Mathlib.RingTheory.Fintype

Mathlib/RingTheory/FiniteStability.lean

@@ -0,0 +1,72 @@
+/-
+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.LinearAlgebra.TensorProduct.RightExactness
+import Mathlib.RingTheory.FinitePresentation
+import Mathlib.RingTheory.TensorProduct.MvPolynomial
+
+/-!
+
+# Stability of finiteness conditions in commutative algebra
+
+In this file we show that `Algebra.FiniteType` and `Algebra.FinitePresentation` are
+stable under base change.
+
+-/
+
+open scoped TensorProduct
+
+universe w₁ w₂ w₃
+
+variable {R : Type w₁} [CommRing R]
+variable {A : Type w₂} [CommRing A] [Algebra R A]
+variable (B : Type w₃) [CommRing B] [Algebra R B]
+
+namespace Algebra
+
+namespace FiniteType
+
+theorem baseChangeAux_surj {σ : Type*} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective f) :
+    Function.Surjective (Algebra.TensorProduct.map (AlgHom.id B B) f) := by
+  show Function.Surjective (TensorProduct.map (AlgHom.id R B) f)
+  apply TensorProduct.map_surjective
+  · exact Function.RightInverse.surjective (congrFun rfl)
+  · exact hf
+
+instance baseChange [hfa : FiniteType R A] : Algebra.FiniteType B (B ⊗[R] A) := by
+  rw [iff_quotient_mvPolynomial''] at *
+  obtain ⟨n, f, hf⟩ := hfa
+  let g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A :=
+    Algebra.TensorProduct.map (AlgHom.id B B) f
+  have : Function.Surjective g := baseChangeAux_surj B hf
+  use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
+  simpa
+
+end FiniteType
+
+namespace FinitePresentation
+
+instance baseChange [FinitePresentation R A] : FinitePresentation B (B ⊗[R] A) := by
+  obtain ⟨n, f, hsurj, hfg⟩ := ‹FinitePresentation R A›
+  let g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A :=
+    Algebra.TensorProduct.map (AlgHom.id B B) f
+  have hgsurj : Function.Surjective g := Algebra.FiniteType.baseChangeAux_surj B hsurj
+  have hker_eq : RingHom.ker g = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker f) :=
+    Algebra.TensorProduct.lTensor_ker f hsurj
+  have hfgg : Ideal.FG (RingHom.ker g) := by
+    rw [hker_eq]
+    exact Ideal.FG.map hfg _
+  let g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
+    AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
+  refine ⟨n, g', ?_, Ideal.fg_ker_comp _ _ ?_ hfgg ?_⟩
+  · simp_all [g, g']
+  · show Ideal.FG (RingHom.ker (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))
+    simp only [RingHom.ker_equiv]
+    exact Submodule.fg_bot
+  · simpa using EquivLike.surjective _
+
+end FinitePresentation
+
+end Algebra

Mathlib/RingTheory/RingHom/FiniteType.lean

@@ -3,6 +3,7 @@ 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.FiniteStability
 import Mathlib.RingTheory.LocalProperties
 import Mathlib.RingTheory.Localization.InvSubmonoid
 
@@ -19,7 +20,7 @@ The main result is `RingHom.finiteType_is_local`.
 
 namespace RingHom
 
-open scoped Pointwise
+open scoped Pointwise TensorProduct
 
 theorem finiteType_stableUnderComposition : StableUnderComposition @FiniteType := by
   introv R hf hg
@@ -100,4 +101,14 @@ theorem finiteType_respectsIso : RingHom.RespectsIso @RingHom.FiniteType :=
   RingHom.finiteType_is_local.respectsIso
 #align ring_hom.finite_type_respects_iso RingHom.finiteType_respectsIso
 
+theorem finiteType_stableUnderBaseChange : StableUnderBaseChange @FiniteType := by
+  apply StableUnderBaseChange.mk
+  · exact finiteType_respectsIso
+  · introv h
+    replace h : Algebra.FiniteType R T := by
+      rw [RingHom.FiniteType] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl
+    suffices Algebra.FiniteType S (S ⊗[R] T) by
+      rw [RingHom.FiniteType]; convert this; congr; ext; simp_rw [Algebra.smul_def]; rfl
+    infer_instance
+
 end RingHom

Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

@@ -186,6 +186,44 @@ noncomputable def scalarRTensorAlgEquiv :
     MvPolynomial σ R ⊗[R] N ≃ₐ[R] MvPolynomial σ N :=
   rTensorAlgEquiv.trans (mapAlgEquiv σ (Algebra.TensorProduct.lid R N))
 
+variable (R)
+variable (A : Type*) [CommSemiring A] [Algebra R A]
+
+/-- Tensoring `MvPolynomial σ R` on the left by an `R`-algebra `A` is algebraically
+equivalent to `M̀vPolynomial σ A`. -/
+noncomputable def algebraTensorAlgEquiv :
+    A ⊗[R] MvPolynomial σ R ≃ₐ[A] MvPolynomial σ A := AlgEquiv.ofAlgHom
+  (Algebra.TensorProduct.lift
+    (Algebra.ofId A (MvPolynomial σ A))
+    (MvPolynomial.mapAlgHom <| Algebra.ofId R A) (fun _ _ ↦ Commute.all _ _))
+  (aeval (fun s ↦ 1 ⊗ₜ X s))
+  (by ext s; simp)
+  (by ext s; simp)
+
+@[simp]
+lemma algebraTensorAlgEquiv_tmul (a : A) (p : MvPolynomial σ R) :
+    algebraTensorAlgEquiv R A (a ⊗ₜ p) = a • MvPolynomial.map (algebraMap R A) p := by
+  simp [algebraTensorAlgEquiv]
+  rw [Algebra.smul_def]
+  rfl
+
+@[simp]
+lemma algebraTensorAlgEquiv_symm_X (s : σ) :
+    (algebraTensorAlgEquiv R A).symm (X s) = 1 ⊗ₜ X s := by
+  simp [algebraTensorAlgEquiv]
+
+@[simp]
+lemma algebraTensorAlgEquiv_symm_monomial (m : σ →₀ ℕ) (a : A) :
+    (algebraTensorAlgEquiv R A).symm (monomial m a) = a ⊗ₜ monomial m 1 := by
+  apply @Finsupp.induction σ ℕ _ _ m
+  · simp [algebraTensorAlgEquiv]
+  · intro i n f _ _ hfa
+    simp only [algebraTensorAlgEquiv, AlgEquiv.ofAlgHom_symm_apply] at hfa ⊢
+    simp only [add_comm, monomial_add_single, _root_.map_mul, map_pow, aeval_X,
+      Algebra.TensorProduct.tmul_pow, one_pow, hfa]
+    nth_rw 2 [← mul_one a]
+    rw [Algebra.TensorProduct.tmul_mul_tmul]
+
 end Algebra
 
 end MvPolynomial