mathlib3 documentation

data.mv_polynomial.monad

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,

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

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

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

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

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.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.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]
@[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) :
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.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.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_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.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.vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [comm_semiring R] [decidable_eq τ] (f : σ mv_polynomial τ R) (φ : mv_polynomial σ R) :
((mv_polynomial.bind₁ f) φ).vars φ.vars.bUnion (λ (i : σ), (f i).vars)
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) :
(i : σ), i φ.vars j (f i).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]
@[protected, instance]