# 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`).

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
@[simp]
theorem MvPolynomial.aeval_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) :
aeval f = bind₁ f
source
@[simp]
theorem MvPolynomial.eval₂Hom_C_eq_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) :
eval₂Hom C f = ↑(bind₁ f)
source
@[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) :
eval₂Hom f X = bind₂ f
source
@[simp]
theorem MvPolynomial.aeval_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [CommSemiring R] :
aeval id = join₁
source
theorem MvPolynomial.eval₂Hom_C_id_eq_join₁ (σ : Type u_1) (R : Type u_3) [CommSemiring R] (φ : MvPolynomial (MvPolynomial σ R) R) :
(eval₂Hom C id) φ = join₁ φ
source
@[simp]
theorem MvPolynomial.eval₂Hom_id_X_eq_join₂ (σ : Type u_1) (R : Type u_3) [CommSemiring R] :
eval₂Hom (RingHom.id (MvPolynomial σ R)) X = join₂
source
@[simp]
theorem MvPolynomial.bind₁_X_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (i : σ) :
(bind₁ f) (X i) = f i
source
@[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 : σ) :
(bind₂ f) (X i) = X i
source
@[simp]
theorem MvPolynomial.bind₁_X_left {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
bind₁ X = AlgHom.id R (MvPolynomial σ R)
source
theorem MvPolynomial.bind₁_C_right {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (x : R) :
(bind₁ f) (C x) = C x
source
@[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) :
(bind₂ f) (C r) = f r
source
@[simp]
theorem MvPolynomial.bind₂_C_left {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
bind₂ C = RingHom.id (MvPolynomial σ R)
source
@[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) :
(bind₂ f).comp C = f
source
@[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) :
join₂ ((map f) φ) = (bind₂ f) φ
source
@[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) :
join₂.comp (map f) = bind₂ f
source
theorem MvPolynomial.aeval_id_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (p : MvPolynomial σ R) :
(aeval id) ((rename f) p) = (aeval f) p
source
@[simp]
theorem MvPolynomial.join₁_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
join₁ ((rename f) φ) = (bind₁ f) φ
source
@[simp]
theorem MvPolynomial.bind₁_id {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
bind₁ id = join₁
source
@[simp]
theorem MvPolynomial.bind₂_id {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
bind₂ (RingHom.id (MvPolynomial σ R)) = join₂
source
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) :
(bind₁ g) ((bind₁ f) φ) = (bind₁ fun (i : σ) => (bind₁ g) (f i)) φ
source
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) :
(bind₁ g).comp (bind₁ f) = bind₁ fun (i : σ) => (bind₁ g) (f i)
source
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) :
(bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)
source
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) :
(bind₂ g) ((bind₂ f) φ) = (bind₂ ((bind₂ g).comp f)) φ
source
theorem MvPolynomial.rename_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R) (g : τ → υ) :
(rename g).comp (bind₁ f) = bind₁ fun (i : σ) => (rename g) (f i)
source
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) :
(rename g) ((bind₁ f) φ) = (bind₁ fun (i : σ) => (rename g) (f i)) φ
source
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) :
(map g) ((bind₂ f) φ) = (bind₂ ((map g).comp f)) φ
source
theorem MvPolynomial.bind₁_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {υ : Type u_6} (f : τ → MvPolynomial υ R) (g : σ → τ) :
(bind₁ f).comp (rename g) = bind₁ (f ∘ g)
source
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) :
(bind₁ f) ((rename g) φ) = (bind₁ (f ∘ g)) φ
source
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) :
(bind₂ f) ((map g) φ) = (bind₂ (f.comp g)) φ
source
@[simp]
theorem MvPolynomial.map_comp_C {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) :
(map f).comp C = C.comp f
source
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 ((bind₁ g) φ) = (eval₂Hom (f.comp C) fun (i : σ) => f (g i)) φ
source
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) :
(map f) ((bind₁ g) φ) = (bind₁ fun (i : σ) => (map f) (g i)) ((map f) φ)
source
@[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) :
(eval₂Hom f g).comp C = f
source
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) :
(eval₂Hom f g) ((bind₁ h) φ) = (eval₂Hom f fun (i : σ) => (eval₂Hom f g) (h i)) φ
source
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) :
(aeval f) ((bind₁ g) φ) = (aeval fun (i : σ) => (aeval f) (g i)) φ
source
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) :
(aeval f).comp (bind₁ g) = aeval fun (i : σ) => (aeval f) (g i)
source
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) :
(eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g
source
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) :
(eval₂Hom f g) ((bind₂ h) φ) = (eval₂Hom ((eval₂Hom f g).comp h) g) φ
source
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) :
(aeval f) ((bind₂ g) φ) = (eval₂Hom ((↑(aeval f)).comp g) f) φ
source
theorem MvPolynomial.eval₂Hom_C_left {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) :
eval₂Hom C f = ↑(bind₁ f)

Alias of `MvPolynomial.eval₂Hom_C_eq_bind₁`.

source
theorem MvPolynomial.bind₁_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R) :
(bind₁ f) ((monomial d) r) = C r * ∏ i ∈ d.support, f i ^ d i
source
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) :
(bind₂ f) ((monomial d) r) = f r * (monomial d) 1
source
@[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 : σ →₀ ℕ) :
(bind₂ f) ((monomial d) 1) = (monomial d) 1
source
theorem MvPolynomial.vars_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
((bind₁ f) φ).vars ⊆ φ.vars.biUnion fun (i : σ) => (f i).vars
source
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 ∈ ((bind₁ f) φ).vars) :
∃ i ∈ φ.vars, j ∈ (f i).vars
source
instance MvPolynomial.monad {R : Type u_3} [CommSemiring R] :
Monad fun (σ : Type u_6) => MvPolynomial σ R
Equations

- One or more equations did not get rendered due to their size.

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