Monad operations on mv_polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines two monadic operations on mv_polynomial. Given p : mv_polynomial σ R,
mv_polynomial.bind₁andmv_polynomial.join₁operate on the variable typeσ.mv_polynomial.bind₂andmv_polynomial.join₂operate on the coefficient typeR.
mv_polynomial.bind₁ f φwithf : σ → mv_polynomial τ Randφ : mv_polynomial σ R, is the polynomialφ(f 1, ..., f i, ...) : mv_polynomial τ R.mv_polynomial.join₁ φwithφ : mv_polynomial (mv_polynomial σ R) Rcollapsesφto amv_polynomial σ R, by evaluatingφunder the mapX f ↦ fforf : mv_polynomial σ R. In other words, if you have a polynomialφin a set of variables indexed by a polynomial ring, you evaluate the polynomial in these indexing polynomials.mv_polynomial.bind₂ f φwithf : R →+* mv_polynomial σ Sandφ : mv_polynomial σ Ris themv_polynomial σ Sobtained fromφby mapping the coefficients ofφthroughfand considering the resulting polynomial as polynomial expression inmv_polynomial σ R.mv_polynomial.join₂ φwithφ : mv_polynomial σ (mv_polynomial σ R)collapsesφto amv_polynomial σ R, by consideringφas polynomial expression inmv_polynomial σ R.
These operations themselves have algebraic structure: mv_polynomial.bind₁
and mv_polynomial.join₁ are algebra homs and
mv_polynomial.bind₂ and mv_polynomial.join₂ are ring homs.
They interact in convenient ways with mv_polynomial.rename, mv_polynomial.map,
mv_polynomial.vars, and other polynomial operations.
Indeed, mv_polynomial.rename is the "map" operation for the (bind₁, join₁) pair,
whereas mv_polynomial.map is the "map" operation for the other pair.
Implementation notes #
We add an is_lawful_monad instance for the (bind₁, join₁) pair.
The second pair cannot be instantiated as a monad,
since it is not a monad in Type but in CommRing (or rather CommSemiRing).
noncomputable
def
mv_polynomial.bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R) :
mv_polynomial σ R →ₐ[R] mv_polynomial τ R
bind₁ is the "left hand side" bind operation on mv_polynomial, operating on the variable type.
Given a polynomial p : mv_polynomial σ R and a map f : σ → mv_polynomial τ R taking variables
in p to polynomials in the variable type τ, bind₁ f p replaces each variable in p with
its value under f, producing a new polynomial in τ. The coefficient type remains the same.
This operation is an algebra hom.
Equations
noncomputable
def
mv_polynomial.bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S) :
mv_polynomial σ R →+* mv_polynomial σ S
bind₂ is the "right hand side" bind operation on mv_polynomial,
operating on the coefficient type.
Given a polynomial p : mv_polynomial σ R and
a map f : R → mv_polynomial σ S taking coefficients in p to polynomials over a new ring S,
bind₂ f p replaces each coefficient in p with its value under f,
producing a new polynomial over S.
The variable type remains the same. This operation is a ring hom.
Equations
noncomputable
def
mv_polynomial.join₁
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R] :
mv_polynomial (mv_polynomial σ R) R →ₐ[R] mv_polynomial σ R
join₁ is the monadic join operation corresponding to mv_polynomial.bind₁. Given a polynomial p
with coefficients in R whose variables are polynomials in σ with coefficients in R,
join₁ p collapses p to a polynomial with variables in σ and coefficients in R.
This operation is an algebra hom.
Equations
noncomputable
def
mv_polynomial.join₂
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R] :
mv_polynomial σ (mv_polynomial σ R) →+* mv_polynomial σ R
join₂ is the monadic join operation corresponding to mv_polynomial.bind₂. Given a polynomial p
with variables in σ whose coefficients are polynomials in σ with coefficients in R,
join₂ p collapses p to a polynomial with variables in σ and coefficients in R.
This operation is a ring hom.
Equations
@[simp]
theorem
mv_polynomial.aeval_eq_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R) :
@[simp]
theorem
mv_polynomial.eval₂_hom_C_eq_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R) :
@[simp]
theorem
mv_polynomial.eval₂_hom_eq_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S) :
@[simp]
theorem
mv_polynomial.eval₂_hom_C_id_eq_join₁
(σ : Type u_1)
(R : Type u_3)
[comm_semiring R]
(φ : mv_polynomial (mv_polynomial σ R) R) :
@[simp]
@[simp]
theorem
mv_polynomial.bind₁_X_right
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(i : σ) :
⇑(mv_polynomial.bind₁ f) (mv_polynomial.X i) = f i
@[simp]
theorem
mv_polynomial.bind₂_X_right
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S)
(i : σ) :
⇑(mv_polynomial.bind₂ f) (mv_polynomial.X i) = mv_polynomial.X i
@[simp]
@[simp]
theorem
mv_polynomial.bind₁_C_right
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(x : R) :
@[simp]
theorem
mv_polynomial.bind₂_C_right
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S)
(r : R) :
⇑(mv_polynomial.bind₂ f) (⇑mv_polynomial.C r) = ⇑f r
@[simp]
@[simp]
theorem
mv_polynomial.bind₂_comp_C
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S) :
@[simp]
theorem
mv_polynomial.join₂_map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S)
(φ : mv_polynomial σ R) :
⇑mv_polynomial.join₂ (⇑(mv_polynomial.map f) φ) = ⇑(mv_polynomial.bind₂ f) φ
@[simp]
theorem
mv_polynomial.join₂_comp_map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S) :
theorem
mv_polynomial.aeval_id_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.aeval id) (⇑(mv_polynomial.rename f) p) = ⇑(mv_polynomial.aeval f) p
@[simp]
theorem
mv_polynomial.join₁_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑mv_polynomial.join₁ (⇑(mv_polynomial.rename f) φ) = ⇑(mv_polynomial.bind₁ f) φ
@[simp]
@[simp]
theorem
mv_polynomial.bind₁_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : σ → mv_polynomial τ R)
(g : τ → mv_polynomial υ R)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.bind₁ g) (⇑(mv_polynomial.bind₁ f) φ) = ⇑(mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.bind₁ g) (f i))) φ
theorem
mv_polynomial.bind₁_comp_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : σ → mv_polynomial τ R)
(g : τ → mv_polynomial υ R) :
(mv_polynomial.bind₁ g).comp (mv_polynomial.bind₁ f) = mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.bind₁ g) (f i))
theorem
mv_polynomial.bind₂_comp_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : R →+* mv_polynomial σ S)
(g : S →+* mv_polynomial σ T) :
(mv_polynomial.bind₂ g).comp (mv_polynomial.bind₂ f) = mv_polynomial.bind₂ ((mv_polynomial.bind₂ g).comp f)
theorem
mv_polynomial.bind₂_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : R →+* mv_polynomial σ S)
(g : S →+* mv_polynomial σ T)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.bind₂ g) (⇑(mv_polynomial.bind₂ f) φ) = ⇑(mv_polynomial.bind₂ ((mv_polynomial.bind₂ g).comp f)) φ
theorem
mv_polynomial.rename_comp_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : σ → mv_polynomial τ R)
(g : τ → υ) :
(mv_polynomial.rename g).comp (mv_polynomial.bind₁ f) = mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.rename g) (f i))
theorem
mv_polynomial.rename_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : σ → mv_polynomial τ R)
(g : τ → υ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.rename g) (⇑(mv_polynomial.bind₁ f) φ) = ⇑(mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.rename g) (f i))) φ
theorem
mv_polynomial.map_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : R →+* mv_polynomial σ S)
(g : S →+* T)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.map g) (⇑(mv_polynomial.bind₂ f) φ) = ⇑(mv_polynomial.bind₂ ((mv_polynomial.map g).comp f)) φ
theorem
mv_polynomial.bind₁_comp_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : τ → mv_polynomial υ R)
(g : σ → τ) :
(mv_polynomial.bind₁ f).comp (mv_polynomial.rename g) = mv_polynomial.bind₁ (f ∘ g)
theorem
mv_polynomial.bind₁_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
{υ : Type u_4}
(f : τ → mv_polynomial υ R)
(g : σ → τ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.bind₁ f) (⇑(mv_polynomial.rename g) φ) = ⇑(mv_polynomial.bind₁ (f ∘ g)) φ
theorem
mv_polynomial.bind₂_map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : S →+* mv_polynomial σ T)
(g : R →+* S)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.bind₂ f) (⇑(mv_polynomial.map g) φ) = ⇑(mv_polynomial.bind₂ (f.comp g)) φ
@[simp]
theorem
mv_polynomial.map_comp_C
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S) :
theorem
mv_polynomial.hom_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : mv_polynomial τ R →+* S)
(g : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑f (⇑(mv_polynomial.bind₁ g) φ) = ⇑(mv_polynomial.eval₂_hom (f.comp mv_polynomial.C) (λ (i : σ), ⇑f (g i))) φ
theorem
mv_polynomial.map_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(g : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.map f) (⇑(mv_polynomial.bind₁ g) φ) = ⇑(mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.map f) (g i))) (⇑(mv_polynomial.map f) φ)
@[simp]
theorem
mv_polynomial.eval₂_hom_comp_C
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(g : σ → S) :
(mv_polynomial.eval₂_hom f g).comp mv_polynomial.C = f
theorem
mv_polynomial.eval₂_hom_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(g : τ → S)
(h : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.eval₂_hom f g) (⇑(mv_polynomial.bind₁ h) φ) = ⇑(mv_polynomial.eval₂_hom f (λ (i : σ), ⇑(mv_polynomial.eval₂_hom f g) (h i))) φ
theorem
mv_polynomial.aeval_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
[algebra R S]
(f : τ → S)
(g : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) (⇑(mv_polynomial.bind₁ g) φ) = ⇑(mv_polynomial.aeval (λ (i : σ), ⇑(mv_polynomial.aeval f) (g i))) φ
theorem
mv_polynomial.aeval_comp_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
[algebra R S]
(f : τ → S)
(g : σ → mv_polynomial τ R) :
(mv_polynomial.aeval f).comp (mv_polynomial.bind₁ g) = mv_polynomial.aeval (λ (i : σ), ⇑(mv_polynomial.aeval f) (g i))
theorem
mv_polynomial.eval₂_hom_comp_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : S →+* T)
(g : σ → T)
(h : R →+* mv_polynomial σ S) :
(mv_polynomial.eval₂_hom f g).comp (mv_polynomial.bind₂ h) = mv_polynomial.eval₂_hom ((mv_polynomial.eval₂_hom f g).comp h) g
theorem
mv_polynomial.eval₂_hom_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
(f : S →+* T)
(g : σ → T)
(h : R →+* mv_polynomial σ S)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.eval₂_hom f g) (⇑(mv_polynomial.bind₂ h) φ) = ⇑(mv_polynomial.eval₂_hom ((mv_polynomial.eval₂_hom f g).comp h) g) φ
theorem
mv_polynomial.aeval_bind₂
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
{T : Type u_5}
[comm_semiring R]
[comm_semiring S]
[comm_semiring T]
[algebra S T]
(f : σ → T)
(g : R →+* mv_polynomial σ S)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) (⇑(mv_polynomial.bind₂ g) φ) = ⇑(mv_polynomial.eval₂_hom (↑(mv_polynomial.aeval f).comp g) f) φ
theorem
mv_polynomial.eval₂_hom_C_left
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R) :
theorem
mv_polynomial.bind₁_monomial
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(d : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.bind₁ f) (⇑(mv_polynomial.monomial d) r) = ⇑mv_polynomial.C r * d.support.prod (λ (i : σ), f i ^ ⇑d i)
theorem
mv_polynomial.bind₂_monomial
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S)
(d : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.bind₂ f) (⇑(mv_polynomial.monomial d) r) = ⇑f r * ⇑(mv_polynomial.monomial d) 1
@[simp]
theorem
mv_polynomial.bind₂_monomial_one
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* mv_polynomial σ S)
(d : σ →₀ ℕ) :
⇑(mv_polynomial.bind₂ f) (⇑(mv_polynomial.monomial d) 1) = ⇑(mv_polynomial.monomial d) 1
theorem
mv_polynomial.vars_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
[decidable_eq τ]
(f : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
theorem
mv_polynomial.mem_vars_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R)
{j : τ}
(h : j ∈ (⇑(mv_polynomial.bind₁ f) φ).vars) :
@[protected, instance]
noncomputable
def
mv_polynomial.monad
{R : Type u_3}
[comm_semiring R] :
monad (λ (σ : Type u_1), mv_polynomial σ R)
Equations
@[protected, instance]
def
mv_polynomial.is_lawful_functor
{R : Type u_3}
[comm_semiring R] :
is_lawful_functor (λ (σ : Type u_1), mv_polynomial σ R)
@[protected, instance]
def
mv_polynomial.is_lawful_monad
{R : Type u_3}
[comm_semiring R] :
is_lawful_monad (λ (σ : Type u_1), mv_polynomial σ R)