feat(ring_theory/mv_polynomial/basic): add polynomial.basis_monomials (…

…#7728)

We add `polynomial.basis_monomials` : the monomials form a basis on `polynomial R`.

Because of the structure of the import, it seems to me a little complicated to do it directly, so I use `mv_polynomial.punit_alg_equiv`

src/data/finsupp/basic.lean

@@ -170,7 +170,7 @@ by simp only [set.subset_def, mem_coe, mem_support_iff];
 
 /-- Given `fintype α`, `equiv_fun_on_fintype` is the `equiv` between `α →₀ β` and `α → β`.
   (All functions on a finite type are finitely supported.) -/
-@[simps apply] def equiv_fun_on_fintype [fintype α] : (α →₀ M) ≃ (α → M) :=
+@[simps] def equiv_fun_on_fintype [fintype α] : (α →₀ M) ≃ (α → M) :=
 ⟨λf a, f a, λf, mk (finset.univ.filter $ λa, f a ≠ 0) f (by simp only [true_and, finset.mem_univ,
   iff_self, finset.mem_filter, finset.filter_congr_decidable, forall_true_iff]),
   begin intro f, ext a, refl end,

src/data/polynomial/algebra_map.lean

@@ -53,10 +53,25 @@ When we have `[comm_ring R]`, the function `C` is the same as `algebra_map R (po
 (But note that `C` is defined when `R` is not necessarily commutative, in which case
 `algebra_map` is not available.)
 -/
-lemma C_eq_algebra_map {R : Type*} [comm_ring R] (r : R) :
+lemma C_eq_algebra_map {R : Type*} [comm_semiring R] (r : R) :
   C r = algebra_map R (polynomial R) r :=
 rfl
 
+variable (R)
+
+/-- Algebra isomorphism between `polynomial R` and `add_monoid_algebra R ℕ`. This is just an
+implementation detail, but it can be useful to transfer results from `finsupp` to polynomials. -/
+@[simps]
+def to_finsupp_iso_alg : polynomial R ≃ₐ[R] add_monoid_algebra R ℕ :=
+{ commutes' := λ r,
+  begin
+    simp only [add_monoid_algebra.coe_algebra_map, algebra.id.map_eq_self, function.comp_app],
+    rw [←C_eq_algebra_map, ←monomial_zero_left, ring_equiv.to_fun_eq_coe, to_finsupp_iso_monomial],
+  end,
+  ..to_finsupp_iso R }
+
+variable {R}
+
 instance [nontrivial A] : nontrivial (subalgebra R (polynomial A)) :=
 ⟨⟨⊥, ⊤, begin
   rw [ne.def, set_like.ext_iff, not_forall],

src/data/polynomial/basic.lean

@@ -42,7 +42,7 @@ equal to `0`.
 The raw implementation of the equivalence between `polynomial R` and `add_monoid_algebra R ℕ` is
 done through `of_finsupp` and `to_finsupp` (or, equivalently, `rcases p` when `p` is a polynomial
 gives an element `q` of `add_monoid_algebra R ℕ`, and conversely `⟨q⟩` gives back `p`). The
-equivalence is also registered as an algebra equiv in `polynomial.to_finsupp_iso`. These should
+equivalence is also registered as a ring equiv in `polynomial.to_finsupp_iso`. These should
 in general not be used once the basic API for polynomials is constructed.
 -/
 
@@ -148,15 +148,16 @@ instance [subsingleton R] : unique (polynomial R) :=
 
 variable (R)
 
-/-- Algebra isomorphism between `polynomial R` and `add_monoid_algebra R ℕ`. This is just an
+/-- Ring isomorphism between `polynomial R` and `add_monoid_algebra R ℕ`. This is just an
 implementation detail, but it can be useful to transfer results from `finsupp` to polynomials. -/
+@[simps]
 def to_finsupp_iso : polynomial R ≃+* add_monoid_algebra R ℕ :=
-{ to_fun := λ ⟨p⟩, p,
+{ to_fun := λ p, p.to_finsupp,
   inv_fun := λ p, ⟨p⟩,
   left_inv := λ ⟨p⟩, rfl,
   right_inv := λ p, rfl,
-  map_mul' := by { rintros ⟨⟩ ⟨⟩, simp [mul_to_finsupp], refl },
-  map_add' := by { rintros ⟨⟩ ⟨⟩, simp [add_to_finsupp], refl } }
+  map_mul' := by { rintros ⟨⟩ ⟨⟩, simp [mul_to_finsupp] },
+  map_add' := by { rintros ⟨⟩ ⟨⟩, simp [add_to_finsupp] } }
 
 variable {R}
 
@@ -264,11 +265,12 @@ by simp only [←monomial_zero_left, monomial_mul_monomial, zero_add]
 @[simp] lemma monomial_mul_C : monomial n a * C b = monomial n (a * b) :=
 by simp only [←monomial_zero_left, monomial_mul_monomial, add_zero]
 
-/-- `X` is the polynomial variable (aka indeterminant). -/
+/-- `X` is the polynomial variable (aka indeterminate). -/
 def X : polynomial R := monomial 1 1
 
 lemma monomial_one_one_eq_X : monomial 1 (1 : R) = X := rfl
-lemma monomial_one_right_eq_X_pow (n : ℕ) : monomial n 1 = X^n :=
+
+lemma monomial_one_right_eq_X_pow (n : ℕ) : monomial n (1 : R) = X^n :=
 begin
   induction n with n ih,
   { simp [monomial_zero_one], },
@@ -387,8 +389,12 @@ begin
   set g' : add_monoid_algebra R ℕ →+ M := g.comp (to_finsupp_iso R).symm with hg',
   have : ∀ n a, f' (single n a) = g' (single n a) := λ n, by simp [hf', hg', h n],
   have A : f' = g' := finsupp.add_hom_ext this,
-  have B : f = f'.comp (to_finsupp_iso R), by { rw [hf', add_monoid_hom.comp_assoc], ext x, simp },
-  have C : g = g'.comp (to_finsupp_iso R), by { rw [hg', add_monoid_hom.comp_assoc], ext x, simp },
+  have B : f = f'.comp (to_finsupp_iso R), by { rw [hf', add_monoid_hom.comp_assoc], ext x,
+  simp only [ring_equiv.symm_apply_apply, add_monoid_hom.coe_comp, function.comp_app,
+    ring_hom.coe_add_monoid_hom, ring_equiv.coe_to_ring_hom, coe_coe]},
+  have C : g = g'.comp (to_finsupp_iso R), by { rw [hg', add_monoid_hom.comp_assoc], ext x,
+  simp only [ring_equiv.symm_apply_apply, add_monoid_hom.coe_comp, function.comp_app,
+    ring_hom.coe_add_monoid_hom, ring_equiv.coe_to_ring_hom, coe_coe]},
   rw [B, C, A],
 end
 

src/data/polynomial/monomial.lean

@@ -60,9 +60,13 @@ begin
     { simp [h₁, ring_equiv.to_ring_hom_eq_coe] },
     { simpa [ring_equiv.to_ring_hom_eq_coe] using h₂, } },
   have B : f = f'.comp (to_finsupp_iso R),
-    by { rw [hf', ring_hom.comp_assoc], ext x, simp [ring_equiv.to_ring_hom_eq_coe] },
+    by { rw [hf', ring_hom.comp_assoc], ext x, simp only [ring_equiv.to_ring_hom_eq_coe,
+      ring_equiv.symm_apply_apply, function.comp_app, ring_hom.coe_comp,
+      ring_equiv.coe_to_ring_hom] },
   have C : g = g'.comp (to_finsupp_iso R),
-    by { rw [hg', ring_hom.comp_assoc], ext x, simp [ring_equiv.to_ring_hom_eq_coe] },
+    by { rw [hg', ring_hom.comp_assoc], ext x, simp only [ring_equiv.to_ring_hom_eq_coe,
+      ring_equiv.symm_apply_apply, function.comp_app, ring_hom.coe_comp,
+      ring_equiv.coe_to_ring_hom] },
   rw [B, C, A]
 end
 

src/ring_theory/mv_polynomial/basic.lean

@@ -117,3 +117,17 @@ rfl
 end degree
 
 end mv_polynomial
+
+
+/- this is here to avoid import cycle issues -/
+namespace polynomial
+
+/-- The monomials form a basis on `polynomial R`. -/
+noncomputable def basis_monomials : basis ℕ R (polynomial R) :=
+finsupp.basis_single_one.map (to_finsupp_iso_alg R).to_linear_equiv.symm
+
+@[simp] lemma coe_basis_monomials :
+  (basis_monomials R : ℕ → polynomial R) = λ s, monomial s 1 :=
+_root_.funext $ λ n, to_finsupp_iso_symm_single
+
+end polynomial