mathlib documentation

data.mv_polynomial.monad

Monad operations on mv_polynomial

This file defines two monadic operations on mv_polynomial. Given p : 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} [comm_semiring R] :
(σ → 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
def mv_polynomial.bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [comm_semiring R] [comm_semiring 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
def mv_polynomial.join₁ {σ : Type u_1} {R : Type u_3} [comm_semiring 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
def mv_polynomial.join₂ {σ : Type u_1} {R : Type u_3} [comm_semiring 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]

@[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 : σ) :

@[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 : σ) :

@[simp]

theorem mv_polynomial.aeval_X_left_apply {σ : Type u_1} {R : Type u_3} [comm_semiring R] (φ : mv_polynomial σ R) :

@[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) :

@[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) :

@[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) :

@[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) :

@[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) :

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) :

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) :

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) :

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 : τ → υ) :

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) :

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) :

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 : σ → τ) :

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) :

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) :

@[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) :

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) :

@[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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

@[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 : σ →₀ ) :

@[instance]
def mv_polynomial.monad {R : Type u_3} [comm_semiring R] :
monad (λ (σ : Type u_1), mv_polynomial σ R)

Equations
@[instance]
def mv_polynomial.is_lawful_functor {R : Type u_3} [comm_semiring R] :
is_lawful_functor (λ (σ : Type u_1), mv_polynomial σ R)

@[instance]
def mv_polynomial.is_lawful_monad {R : Type u_3} [comm_semiring R] :
is_lawful_monad (λ (σ : Type u_1), mv_polynomial σ R)