# Monad operations on MvPolynomial#

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

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

These operations themselves have algebraic structure: MvPolynomial.bind₁ and MvPolynomial.join₁ are algebra homs and MvPolynomial.bind₂ and MvPolynomial.join₂ are ring homs.

They interact in convenient ways with MvPolynomial.rename, MvPolynomial.map, MvPolynomial.vars, and other polynomial operations. Indeed, MvPolynomial.rename is the "map" operation for the (bind₁, join₁) pair, whereas MvPolynomial.map is the "map" operation for the other pair.

## Implementation notes #

We add a LawfulMonad 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 CommRingCat (or rather CommSemiRingCat).

def MvPolynomial.bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) :

bind₁ is the "left hand side" bind operation on MvPolynomial, operating on the variable type. Given a polynomial p : MvPolynomial σ R and a map f : σ → MvPolynomial τ 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
Instances For
def MvPolynomial.bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) :

bind₂ is the "right hand side" bind operation on MvPolynomial, operating on the coefficient type. Given a polynomial p : MvPolynomial σ R and a map f : R → MvPolynomial σ 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
Instances For
def MvPolynomial.join₁ {σ : Type u_1} {R : Type u_3} [] :

join₁ is the monadic join operation corresponding to MvPolynomial.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
• MvPolynomial.join₁ =
Instances For
def MvPolynomial.join₂ {σ : Type u_1} {R : Type u_3} [] :

join₂ is the monadic join operation corresponding to MvPolynomial.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
Instances For
@[simp]
theorem MvPolynomial.aeval_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) :
@[simp]
theorem MvPolynomial.eval₂Hom_C_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) :
MvPolynomial.eval₂Hom MvPolynomial.C f =
@[simp]
theorem MvPolynomial.eval₂Hom_eq_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) :
MvPolynomial.eval₂Hom f MvPolynomial.X =
@[simp]
theorem MvPolynomial.aeval_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [] :
= MvPolynomial.join₁
theorem MvPolynomial.eval₂Hom_C_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [] (φ : MvPolynomial () R) :
(MvPolynomial.eval₂Hom MvPolynomial.C id) φ = MvPolynomial.join₁ φ
@[simp]
theorem MvPolynomial.eval₂Hom_id_X_eq_join₂ (σ : Type u_1) (R : Type u_3) [] :
MvPolynomial.eval₂Hom (RingHom.id ()) MvPolynomial.X = MvPolynomial.join₂
@[simp]
theorem MvPolynomial.bind₁_X_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (i : σ) :
() = f i
@[simp]
theorem MvPolynomial.bind₂_X_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) (i : σ) :
@[simp]
theorem MvPolynomial.bind₁_X_left {σ : Type u_1} {R : Type u_3} [] :
MvPolynomial.bind₁ MvPolynomial.X = AlgHom.id R ()
theorem MvPolynomial.bind₁_C_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (x : R) :
(MvPolynomial.C x) = MvPolynomial.C x
@[simp]
theorem MvPolynomial.bind₂_C_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) (r : R) :
(MvPolynomial.C r) = f r
@[simp]
theorem MvPolynomial.bind₂_C_left {σ : Type u_1} {R : Type u_3} [] :
@[simp]
theorem MvPolynomial.bind₂_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) :
.comp MvPolynomial.C = f
@[simp]
theorem MvPolynomial.join₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) (φ : ) :
MvPolynomial.join₂ (() φ) = φ
@[simp]
theorem MvPolynomial.join₂_comp_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) :
MvPolynomial.join₂.comp () =
theorem MvPolynomial.aeval_id_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (p : ) :
() ( p) = p
@[simp]
theorem MvPolynomial.join₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (φ : ) :
MvPolynomial.join₁ ( φ) = φ
@[simp]
theorem MvPolynomial.bind₁_id {σ : Type u_1} {R : Type u_3} [] :
= MvPolynomial.join₁
@[simp]
theorem MvPolynomial.bind₂_id {σ : Type u_1} {R : Type u_3} [] :
= MvPolynomial.join₂
theorem MvPolynomial.bind₁_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : σ) (g : τ) (φ : ) :
( φ) = (MvPolynomial.bind₁ fun (i : σ) => (f i)) φ
theorem MvPolynomial.bind₁_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : σ) (g : τ) :
.comp = MvPolynomial.bind₁ fun (i : σ) => (f i)
theorem MvPolynomial.bind₂_comp_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* ) (g : S →+* ) :
.comp = MvPolynomial.bind₂ (.comp f)
theorem MvPolynomial.bind₂_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* ) (g : S →+* ) (φ : ) :
( φ) = (MvPolynomial.bind₂ (.comp f)) φ
theorem MvPolynomial.rename_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : σ) (g : τυ) :
.comp = MvPolynomial.bind₁ fun (i : σ) => (f i)
theorem MvPolynomial.rename_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : σ) (g : τυ) (φ : ) :
( φ) = (MvPolynomial.bind₁ fun (i : σ) => (f i)) φ
theorem MvPolynomial.map_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* ) (g : S →+* T) (φ : ) :
() ( φ) = (MvPolynomial.bind₂ (().comp f)) φ
theorem MvPolynomial.bind₁_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : τ) (g : στ) :
theorem MvPolynomial.bind₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] {υ : Type u_6} (f : τ) (g : στ) (φ : ) :
( φ) = (MvPolynomial.bind₁ (f g)) φ
theorem MvPolynomial.bind₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [] [] [] (f : S →+* ) (g : R →+* S) (φ : ) :
(() φ) = (MvPolynomial.bind₂ (f.comp g)) φ
@[simp]
theorem MvPolynomial.map_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) :
().comp MvPolynomial.C = MvPolynomial.C.comp f
theorem MvPolynomial.hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] (f : →+* S) (g : σ) (φ : ) :
f ( φ) = (MvPolynomial.eval₂Hom (f.comp MvPolynomial.C) fun (i : σ) => f (g i)) φ
theorem MvPolynomial.map_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (g : σ) (φ : ) :
() ( φ) = (MvPolynomial.bind₁ fun (i : σ) => () (g i)) (() φ)
@[simp]
theorem MvPolynomial.eval₂Hom_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (g : σS) :
().comp MvPolynomial.C = f
theorem MvPolynomial.eval₂Hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (g : τS) (h : σ) (φ : ) :
() ( φ) = (MvPolynomial.eval₂Hom f fun (i : σ) => () (h i)) φ
theorem MvPolynomial.aeval_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] [Algebra R S] (f : τS) (g : σ) (φ : ) :
( φ) = (MvPolynomial.aeval fun (i : σ) => (g i)) φ
theorem MvPolynomial.aeval_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [] [] [Algebra R S] (f : τS) (g : σ) :
.comp = MvPolynomial.aeval fun (i : σ) => (g i)
theorem MvPolynomial.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 →+* ) :
().comp = MvPolynomial.eval₂Hom (().comp h) g
theorem MvPolynomial.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 →+* ) (φ : ) :
() ( φ) = (MvPolynomial.eval₂Hom (().comp h) g) φ
theorem MvPolynomial.aeval_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [] [] [] [Algebra S T] (f : σT) (g : R →+* ) (φ : ) :
( φ) = (MvPolynomial.eval₂Hom (().comp g) f) φ
theorem MvPolynomial.eval₂Hom_C_left {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) :
MvPolynomial.eval₂Hom MvPolynomial.C f =
theorem MvPolynomial.bind₁_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (d : σ →₀ ) (r : R) :
() = MvPolynomial.C r * id.support, f i ^ d i
theorem MvPolynomial.bind₂_monomial {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) (d : σ →₀ ) (r : R) :
() = f r *
@[simp]
theorem MvPolynomial.bind₂_monomial_one {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* ) (d : σ →₀ ) :
() =
theorem MvPolynomial.vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] [] (f : σ) (φ : ) :
( φ).vars φ.vars.biUnion fun (i : σ) => (f i).vars
theorem MvPolynomial.mem_vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : σ) (φ : ) {j : τ} (h : j ( φ).vars) :
iφ.vars, j (f i).vars
instance MvPolynomial.monad {R : Type u_3} [] :
Monad fun (σ : Type u_6) =>
Equations