From fc4a489c2af75f687338fe85c8901335360f8541 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 15 Mar 2023 10:05:12 +0000
Subject: [PATCH] feat: port RingTheory.MvPolynomial.Tower (#2897)

---
 Mathlib.lean                               |  1 +
 Mathlib/RingTheory/MvPolynomial/Tower.lean | 94 ++++++++++++++++++++++
 2 files changed, 95 insertions(+)
 create mode 100644 Mathlib/RingTheory/MvPolynomial/Tower.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index a68755a8761c2..06080d2498448 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1243,6 +1243,7 @@ import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.Localization.Integer
+import Mathlib.RingTheory.MvPolynomial.Tower
 import Mathlib.RingTheory.Nilpotent
 import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
diff --git a/Mathlib/RingTheory/MvPolynomial/Tower.lean b/Mathlib/RingTheory/MvPolynomial/Tower.lean
new file mode 100644
index 0000000000000..d6525333d1ddf
--- /dev/null
+++ b/Mathlib/RingTheory/MvPolynomial/Tower.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2022 Yuyang Zhao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuyang Zhao
+
+! This file was ported from Lean 3 source module ring_theory.mv_polynomial.tower
+! leanprover-community/mathlib commit bb168510ef455e9280a152e7f31673cabd3d7496
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Algebra.Tower
+import Mathlib.Data.MvPolynomial.Basic
+
+/-!
+# Algebra towers for multivariate polynomial
+
+This file proves some basic results about the algebra tower structure for the type
+`MvPolynomial σ R`.
+
+This structure itself is provided elsewhere as `MvPolynomial.isScalarTower`
+
+When you update this file, you can also try to make a corresponding update in
+`RingTheory.Polynomial.Tower`.
+-/
+
+
+variable (R A B : Type _) {σ : Type _}
+
+namespace MvPolynomial
+
+section Semiring
+
+variable [CommSemiring R] [CommSemiring A] [CommSemiring B]
+
+variable [Algebra R A] [Algebra A B] [Algebra R B]
+
+variable [IsScalarTower R A B]
+
+variable {R B}
+
+theorem aeval_map_algebraMap (x : σ → B) (p : MvPolynomial σ R) :
+    aeval x (map (algebraMap R A) p) = aeval x p := by
+  rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
+#align mv_polynomial.aeval_map_algebra_map MvPolynomial.aeval_map_algebraMap
+
+end Semiring
+
+section CommSemiring
+
+variable [CommSemiring R] [CommSemiring A] [CommSemiring B]
+
+variable [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
+
+variable {R A}
+
+theorem aeval_algebraMap_apply (x : σ → A) (p : MvPolynomial σ R) :
+    aeval (algebraMap A B ∘ x) p = algebraMap A B (MvPolynomial.aeval x p) := by
+  rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
+    IsScalarTower.algebraMap_eq]
+  -- Porting note: added
+  simp only [Function.comp]
+#align mv_polynomial.aeval_algebra_map_apply MvPolynomial.aeval_algebraMap_apply
+
+theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : σ → A)
+    (p : MvPolynomial σ R) : aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 := by
+  rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
+    iff_false_intro (one_ne_zero' B), or_false_iff]
+#align mv_polynomial.aeval_algebra_map_eq_zero_iff MvPolynomial.aeval_algebraMap_eq_zero_iff
+
+theorem aeval_algebraMap_eq_zero_iff_of_injective {x : σ → A} {p : MvPolynomial σ R}
+    (h : Function.Injective (algebraMap A B)) : aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0 :=
+  by rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
+#align mv_polynomial.aeval_algebra_map_eq_zero_iff_of_injective MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective
+
+end CommSemiring
+
+end MvPolynomial
+
+namespace Subalgebra
+
+open MvPolynomial
+
+section CommSemiring
+
+variable {R A} [CommSemiring R] [CommSemiring A] [Algebra R A]
+
+@[simp]
+theorem mvPolynomial_aeval_coe (S : Subalgebra R A) (x : σ → S) (p : MvPolynomial σ R) :
+    aeval (fun i => (x i : A)) p = aeval x p := by convert aeval_algebraMap_apply A x p
+#align subalgebra.mv_polynomial_aeval_coe Subalgebra.mvPolynomial_aeval_coe
+
+end CommSemiring
+
+end Subalgebra