feat(RingTheory/FinitePresentation): a finite product of finitely presented algebras is finitely presented (leanprover-community#32758)

From Pi1.

Author: chrisflav

Mathlib/Algebra/BigOperators/Pi.lean

@@ -197,19 +197,19 @@ def Pi.monoidHomMulEquiv {ι : Type*} [Fintype ι] [DecidableEq ι] (M : ι →
 
 end MulEquiv
 
-variable [Finite ι] [DecidableEq ι] {M : Type*}
+variable [Finite ι] [DecidableEq ι] {M : ι → Type*}
 
 -- manually additivized to fix variable names
 -- See https://github.com/leanprover-community/mathlib4/issues/11462
-lemma Pi.single_induction [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
+lemma Pi.single_induction [∀ i, AddCommMonoid (M i)] (p : (Π i, M i) → Prop) (f : Π i, M i)
     (zero : p 0) (add : ∀ f g, p f → p g → p (f + g))
     (single : ∀ i m, p (Pi.single i m)) : p f := by
   cases nonempty_fintype ι
   rw [← Finset.univ_sum_single f]
   exact Finset.sum_induction _ _ add zero (by simp [single])
 
 @[to_additive existing (attr := elab_as_elim)]
-lemma Pi.mulSingle_induction [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
+lemma Pi.mulSingle_induction [∀ i, CommMonoid (M i)] (p : (Π i, M i) → Prop) (f : Π i, M i)
     (one : p 1) (mul : ∀ f g, p f → p g → p (f * g))
     (mulSingle : ∀ i m, p (Pi.mulSingle i m)) : p f := by
   cases nonempty_fintype ι

Mathlib/RingTheory/Ideal/Basic.lean

@@ -200,6 +200,17 @@ theorem prod_mem {ι : Type*} {f : ι → α} {s : Finset ι}
   rw [Finset.prod_eq_prod_diff_singleton_mul hi]
   exact Ideal.mul_mem_left _ _ hfi
 
+lemma span_single_eq_top {ι : Type*} [DecidableEq ι] [Finite ι] (R : ι → Type*)
+    [∀ i, Semiring (R i)] : Ideal.span (Set.range fun i ↦ (Pi.single i 1 : Π i, R i)) = ⊤ := by
+  rw [_root_.eq_top_iff]
+  rintro x -
+  induction x using Pi.single_induction with
+  | zero => simp
+  | add f g hf hg => exact Ideal.add_mem _ hf hg
+  | single i r =>
+      rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
+      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)
+
 end Ideal
 
 end CommSemiring

Mathlib/RingTheory/Ideal/Maps.lean

@@ -1257,3 +1257,12 @@ instance {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal R) [
       Ideal.submodule_span_eq]⟩
 
 end PrincipalIdeal
+
+lemma RingHom.ker_evalRingHom {ι : Type*} [DecidableEq ι] (R : ι → Type*)
+    [∀ i, CommRing (R i)] (i : ι) :
+    RingHom.ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1} := by
+  refine le_antisymm (fun x hx ↦ ?_) (by simp [Ideal.span_le])
+  simp only [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
+  rw [Ideal.mem_span_singleton]
+  use x + Pi.single i 1
+  simp [mul_add, sub_mul, one_mul, ← Pi.single_mul_left, hx]

Mathlib/RingTheory/RingHom/FinitePresentation.lean

@@ -118,6 +118,28 @@ lemma of_span_eq_top_target (s : Set S) (hs : Ideal.span (s : Set S) = ⊤)
     apply h
   exact of_span_eq_top_target_aux f' hf' t ht Ht
 
+/-- Finite-presentation can be checked on a standard covering of the target. -/
+lemma of_span_eq_top_target_of_isLocalizationAway {ι : Type*} (s : ι → S)
+    (hs : Ideal.span (Set.range s) = ⊤) (T : ι → Type*) [∀ i, CommRing (T i)] [∀ i, Algebra R (T i)]
+    [∀ i, Algebra S (T i)] [∀ i, IsScalarTower R S (T i)] [∀ i, IsLocalization.Away (s i) (T i)]
+    [∀ i, Algebra.FinitePresentation R (T i)] :
+    Algebra.FinitePresentation R S := by
+  apply of_span_eq_top_target _ hs
+  rintro - ⟨i, rfl⟩
+  exact .equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R
+
+instance pi {ι : Type*} [Finite ι] (S : ι → Type*) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
+    [∀ i, Algebra.FinitePresentation R (S i)] :
+    Algebra.FinitePresentation R (∀ a, S a) := by
+  classical
+  let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra
+  have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
+    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
+      ((Pi.evalRingHom S i).surjective)
+    simp [IsIdempotentElem, ← Pi.single_mul_left]
+  exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
+    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)
+
 end Algebra.FinitePresentation
 
 namespace RingHom