# Monad operations on mv_polynomial#

This file defines two monadic operations on mv_polynomial. Given p : mv_polynomial σ R,

• mv_polynomial.bind₁ and mv_polynomial.join₁ operate on the variable type σ.
• mv_polynomial.bind₂ and mv_polynomial.join₂ operate on the coefficient type R.
• mv_polynomial.bind₁ f φ with f : σ → mv_polynomial τ R and φ : mv_polynomial σ R, is the polynomial φ(f 1, ..., f i, ...) : mv_polynomial τ R.
• mv_polynomial.join₁ φ with φ : mv_polynomial (mv_polynomial σ R) R collapses φ to a mv_polynomial σ R, by evaluating φ under the map X f ↦ f for f : 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 φ with f : R →+* mv_polynomial σ S and φ : mv_polynomial σ R is the mv_polynomial σ S obtained from φ by mapping the coefficients of φ through f and considering the resulting polynomial as polynomial expression in mv_polynomial σ R.
• mv_polynomial.join₂ φ with φ : mv_polynomial σ (mv_polynomial σ R) collapses φ to a mv_polynomial σ R, by considering φ as polynomial expression in mv_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).

def mv_polynomial.bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) :

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
def mv_polynomial.bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) :

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
def mv_polynomial.join₁ {σ : Type u_1} {R : Type u_3}  :

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
def mv_polynomial.join₂ {σ : Type u_1} {R : Type u_3}  :
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} (f : σ → ) :
@[simp]
theorem mv_polynomial.eval₂_hom_C_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) :
@[simp]
theorem mv_polynomial.eval₂_hom_eq_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) :
@[simp]
theorem mv_polynomial.aeval_id_eq_join₁ (σ : Type u_1) (R : Type u_3)  :
theorem mv_polynomial.eval₂_hom_C_id_eq_join₁ (σ : Type u_1) (R : Type u_3) (φ : R) :
@[simp]
theorem mv_polynomial.eval₂_hom_id_X_eq_join₂ (σ : Type u_1) (R : Type u_3)  :
@[simp]
theorem mv_polynomial.bind₁_X_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) (i : σ) :
= f i
@[simp]
theorem mv_polynomial.bind₂_X_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) (i : σ) :
@[simp]
theorem mv_polynomial.bind₁_X_left {σ : Type u_1} {R : Type u_3}  :
theorem mv_polynomial.aeval_X_left {σ : Type u_1} {R : Type u_3}  :
theorem mv_polynomial.aeval_X_left_apply {σ : Type u_1} {R : Type u_3} (φ : R) :
@[simp]
theorem mv_polynomial.bind₁_C_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) (x : R) :
@[simp]
theorem mv_polynomial.bind₂_C_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) (r : R) :
= f r
@[simp]
theorem mv_polynomial.bind₂_C_left {σ : Type u_1} {R : Type u_3}  :
@[simp]
theorem mv_polynomial.bind₂_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) :
@[simp]
theorem mv_polynomial.join₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) (φ : R) :
= φ
@[simp]
theorem mv_polynomial.join₂_comp_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) :
theorem mv_polynomial.aeval_id_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) (p : R) :
p) = p
@[simp]
theorem mv_polynomial.join₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) (φ : R) :
@[simp]
theorem mv_polynomial.bind₁_id {σ : Type u_1} {R : Type u_3}  :
@[simp]
theorem mv_polynomial.bind₂_id {σ : Type u_1} {R : Type u_3}  :
theorem mv_polynomial.bind₁_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : σ → ) (g : τ → ) (φ : R) :
( φ) = (mv_polynomial.bind₁ (λ (i : σ), (f i))) φ
theorem mv_polynomial.bind₁_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : σ → ) (g : τ → ) :
= mv_polynomial.bind₁ (λ (i : σ), (f i))
theorem mv_polynomial.bind₂_comp_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : R →+* ) (g : S →+* ) :
theorem mv_polynomial.bind₂_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : R →+* ) (g : S →+* ) (φ : R) :
theorem mv_polynomial.rename_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : σ → ) (g : τ → υ) :
= mv_polynomial.bind₁ (λ (i : σ), (f i))
theorem mv_polynomial.rename_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : σ → ) (g : τ → υ) (φ : R) :
( φ) = (mv_polynomial.bind₁ (λ (i : σ), (f i))) φ
theorem mv_polynomial.map_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : R →+* ) (g : S →+* T) (φ : R) :
theorem mv_polynomial.bind₁_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : τ → ) (g : σ → τ) :
theorem mv_polynomial.bind₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {υ : Type u_4} (f : τ → ) (g : σ → τ) (φ : R) :
theorem mv_polynomial.bind₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : S →+* ) (g : R →+* S) (φ : R) :
@[simp]
theorem mv_polynomial.map_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* S) :
theorem mv_polynomial.hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} (f : →+* S) (g : σ → ) (φ : R) :
f ( φ) = (λ (i : σ), f (g i))) φ
theorem mv_polynomial.map_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} (f : R →+* S) (g : σ → ) (φ : R) :
( φ) = (mv_polynomial.bind₁ (λ (i : σ), (g i))) ( φ)
@[simp]
theorem mv_polynomial.eval₂_hom_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* S) (g : σ → S) :
theorem mv_polynomial.eval₂_hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} (f : R →+* S) (g : τ → S) (h : σ → ) (φ : R) :
( φ) = (λ (i : σ), (h i))) φ
theorem mv_polynomial.aeval_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [ S] (f : τ → S) (g : σ → ) (φ : R) :
( φ) = (mv_polynomial.aeval (λ (i : σ), (g i))) φ
theorem mv_polynomial.aeval_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [ S] (f : τ → S) (g : σ → ) :
= mv_polynomial.aeval (λ (i : σ), (g i))
theorem mv_polynomial.eval₂_hom_comp_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : S →+* T) (g : σ → T) (h : R →+* ) :
= g
theorem mv_polynomial.eval₂_hom_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} (f : S →+* T) (g : σ → T) (h : R →+* ) (φ : R) :
( φ) = g) φ
theorem mv_polynomial.aeval_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [ T] (f : σ → T) (g : R →+* ) (φ : R) :
( φ) = f) φ
theorem mv_polynomial.eval₂_hom_C_left {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) :
theorem mv_polynomial.bind₁_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ → ) (d : σ →₀ ) (r : R) :
= * ∏ (i : σ) in d.support, f i ^ d i
theorem mv_polynomial.bind₂_monomial {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) (d : σ →₀ ) (r : R) :
= (f r) *
@[simp]
theorem mv_polynomial.bind₂_monomial_one {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* ) (d : σ →₀ ) :
@[instance]
def mv_polynomial.monad {R : Type u_3}  :
monad (λ (σ : Type u_1), R)
Equations
@[instance]
def mv_polynomial.is_lawful_functor {R : Type u_3}  :
is_lawful_functor (λ (σ : Type u_1), R)
@[instance]
def mv_polynomial.is_lawful_monad {R : Type u_3}  :
is_lawful_monad (λ (σ : Type u_1), R)