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 CommRing (or rather CommSemiRing).

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

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

• MvPolynomial.bind₁ f = MvPolynomial.aeval f

def MvPolynomial.bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) : MvPolynomial σ R →+* MvPolynomial σ S

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

• MvPolynomial.bind₂ f = MvPolynomial.eval₂Hom f MvPolynomial.X

def MvPolynomial.join₁ {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial (MvPolynomial σ R) R →ₐ[R] MvPolynomial σ R

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₁ = MvPolynomial.aeval id

def MvPolynomial.join₂ {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial σ (MvPolynomial σ R) →+* MvPolynomial σ R

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

• MvPolynomial.join₂ = MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X

@[simp]

theorem MvPolynomial.aeval_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) : MvPolynomial.aeval f = MvPolynomial.bind₁ f

@[simp]

theorem MvPolynomial.eval₂Hom_C_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) : MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)

@[simp]

theorem MvPolynomial.eval₂Hom_eq_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) : MvPolynomial.eval₂Hom f MvPolynomial.X = MvPolynomial.bind₂ f

@[simp]

theorem MvPolynomial.aeval_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [CommSemiring R] : MvPolynomial.aeval id = MvPolynomial.join₁

theorem MvPolynomial.eval₂Hom_C_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [CommSemiring R] (φ : MvPolynomial (MvPolynomial σ R) 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) [CommSemiring R] : MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X = MvPolynomial.join₂

@[simp]

theorem MvPolynomial.bind₁_X_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (i : σ) : (MvPolynomial.bind₁ f) (MvPolynomial.X i) = f i

@[simp]

theorem MvPolynomial.bind₂_X_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (i : σ) : (MvPolynomial.bind₂ f) (MvPolynomial.X i) = MvPolynomial.X i

@[simp]

theorem MvPolynomial.bind₁_X_left {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial.bind₁ MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)

@[simp]

theorem MvPolynomial.bind₁_C_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (x : R) : (MvPolynomial.bind₁ f) (MvPolynomial.C x) = MvPolynomial.C x

@[simp]

theorem MvPolynomial.bind₂_C_right {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (r : R) : (MvPolynomial.bind₂ f) (MvPolynomial.C r) = f r

@[simp]

theorem MvPolynomial.bind₂_C_left {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial.bind₂ MvPolynomial.C = RingHom.id (MvPolynomial σ R)

@[simp]

theorem MvPolynomial.bind₂_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) : RingHom.comp (MvPolynomial.bind₂ f) MvPolynomial.C = f

@[simp]

theorem MvPolynomial.join₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) : MvPolynomial.join₂ ((MvPolynomial.map f) φ) = (MvPolynomial.bind₂ f) φ

@[simp]

theorem MvPolynomial.join₂_comp_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) : RingHom.comp MvPolynomial.join₂ (MvPolynomial.map f) = MvPolynomial.bind₂ f

theorem MvPolynomial.aeval_id_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (p : MvPolynomial σ R) : (MvPolynomial.aeval id) ((MvPolynomial.rename f) p) = (MvPolynomial.aeval f) p

@[simp]

theorem MvPolynomial.join₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : MvPolynomial.join₁ ((MvPolynomial.rename f) φ) = (MvPolynomial.bind₁ f) φ

@[simp]

theorem MvPolynomial.bind₁_id {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial.bind₁ id = MvPolynomial.join₁

@[simp]

theorem MvPolynomial.bind₂_id {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial.bind₂ (RingHom.id (MvPolynomial σ R)) = MvPolynomial.join₂

theorem MvPolynomial.bind₁_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R) (φ : MvPolynomial σ R) : (MvPolynomial.bind₁ g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.bind₁ g) (f i)) φ

theorem MvPolynomial.bind₁_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R) : AlgHom.comp (MvPolynomial.bind₁ g) (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.bind₁ g) (f i)

theorem MvPolynomial.bind₂_comp_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) : RingHom.comp (MvPolynomial.bind₂ g) (MvPolynomial.bind₂ f) = MvPolynomial.bind₂ (RingHom.comp (MvPolynomial.bind₂ g) f)

theorem MvPolynomial.bind₂_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) (φ : MvPolynomial σ R) : (MvPolynomial.bind₂ g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ (RingHom.comp (MvPolynomial.bind₂ g) f)) φ

theorem MvPolynomial.rename_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R) (g : τ → υ) : AlgHom.comp (MvPolynomial.rename g) (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.rename g) (f i)

theorem MvPolynomial.rename_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R) (g : τ → υ) (φ : MvPolynomial σ R) : (MvPolynomial.rename g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.rename g) (f i)) φ

theorem MvPolynomial.map_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* T) (φ : MvPolynomial σ R) : (MvPolynomial.map g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ (RingHom.comp (MvPolynomial.map g) f)) φ

theorem MvPolynomial.bind₁_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : τ → MvPolynomial υ R) (g : σ → τ) : AlgHom.comp (MvPolynomial.bind₁ f) (MvPolynomial.rename g) = MvPolynomial.bind₁ (f ∘ g)

theorem MvPolynomial.bind₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : τ → MvPolynomial υ R) (g : σ → τ) (φ : MvPolynomial σ R) : (MvPolynomial.bind₁ f) ((MvPolynomial.rename g) φ) = (MvPolynomial.bind₁ (f ∘ g)) φ

theorem MvPolynomial.bind₂_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : S →+* MvPolynomial σ T) (g : R →+* S) (φ : MvPolynomial σ R) : (MvPolynomial.bind₂ f) ((MvPolynomial.map g) φ) = (MvPolynomial.bind₂ (RingHom.comp f g)) φ

@[simp]

theorem MvPolynomial.map_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) : RingHom.comp (MvPolynomial.map f) MvPolynomial.C = RingHom.comp MvPolynomial.C f

theorem MvPolynomial.hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : MvPolynomial τ R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : f ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.eval₂Hom (RingHom.comp f 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} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : (MvPolynomial.map f) ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.map f) (g i)) ((MvPolynomial.map f) φ)

@[simp]

theorem MvPolynomial.eval₂Hom_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ → S) : RingHom.comp (MvPolynomial.eval₂Hom f g) MvPolynomial.C = f

theorem MvPolynomial.eval₂Hom_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : τ → S) (h : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₁ h) φ) = (MvPolynomial.eval₂Hom f fun (i : σ) => (MvPolynomial.eval₂Hom f g) (h i)) φ

theorem MvPolynomial.aeval_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : (MvPolynomial.aeval f) ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.aeval fun (i : σ) => (MvPolynomial.aeval f) (g i)) φ

theorem MvPolynomial.aeval_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) : AlgHom.comp (MvPolynomial.aeval f) (MvPolynomial.bind₁ g) = MvPolynomial.aeval fun (i : σ) => (MvPolynomial.aeval f) (g i)

theorem MvPolynomial.eval₂Hom_comp_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) : RingHom.comp (MvPolynomial.eval₂Hom f g) (MvPolynomial.bind₂ h) = MvPolynomial.eval₂Hom (RingHom.comp (MvPolynomial.eval₂Hom f g) h) g

theorem MvPolynomial.eval₂Hom_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₂ h) φ) = (MvPolynomial.eval₂Hom (RingHom.comp (MvPolynomial.eval₂Hom f g) h) g) φ

theorem MvPolynomial.aeval_bind₂ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra S T] (f : σ → T) (g : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) : (MvPolynomial.aeval f) ((MvPolynomial.bind₂ g) φ) = (MvPolynomial.eval₂Hom (RingHom.comp (↑(MvPolynomial.aeval f)) g) f) φ

theorem MvPolynomial.eval₂Hom_C_left {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) : MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)

theorem MvPolynomial.bind₁_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.bind₁ f) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * Finset.prod d.support fun (i : σ) => f i ^ d i

theorem MvPolynomial.bind₂_monomial {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) r) = f r * (MvPolynomial.monomial d) 1

@[simp]

theorem MvPolynomial.bind₂_monomial_one {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) : (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) 1) = (MvPolynomial.monomial d) 1

theorem MvPolynomial.vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : MvPolynomial.vars ((MvPolynomial.bind₁ f) φ) ⊆ Finset.biUnion (MvPolynomial.vars φ) fun (i : σ) => MvPolynomial.vars (f i)

theorem MvPolynomial.mem_vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ MvPolynomial.vars ((MvPolynomial.bind₁ f) φ)) : ∃ i ∈ MvPolynomial.vars φ, j ∈ MvPolynomial.vars (f i)

instance MvPolynomial.monad {R : Type u_3} [CommSemiring R] : Monad fun (σ : Type u_6) => MvPolynomial σ R

Equations

• MvPolynomial.monad = Monad.mk

instance MvPolynomial.lawfulFunctor {R : Type u_3} [CommSemiring R] : LawfulFunctor fun (σ : Type u_6) => MvPolynomial σ R

Equations

• (_ : LawfulFunctor fun (σ : Type u_6) => MvPolynomial σ R) = (_ : LawfulFunctor fun (σ : Type u_6) => MvPolynomial σ R)

instance MvPolynomial.lawfulMonad {R : Type u_3} [CommSemiring R] : LawfulMonad fun (σ : Type u_6) => MvPolynomial σ R

Equations

• (_ : LawfulMonad fun (σ : Type u_6) => MvPolynomial σ R) = (_ : LawfulMonad fun (σ : Type u_6) => MvPolynomial σ R)