English
The MV-polynomial construction carries a lawful monad structure, i.e., it satisfies the Monad laws with the given pure and bind operations.
Русский
Конструкция mv-полиномов обладает законной монада-структурой, то есть удовлетворяет монадамым законам с данными операциями pure и bind.
LaTeX
$$$$ \text{LawfulMonad} \; (\mathrm{MvPolynomial}\; \sigma\; R) $$$$
Lean4
instance lawfulMonad : LawfulMonad fun σ => MvPolynomial σ R
where
pure_bind := by intros; simp [pure, bind]
bind_assoc := by intros; simp [bind, ← bind₁_comp_bind₁]
seqLeft_eq := by intros; simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]; rfl
seqRight_eq := by intros; simp [SeqRight.seqRight, Seq.seq, (· <$> ·), bind₁_rename]; rfl
pure_seq := by intros; simp [(· <$> ·), pure, Seq.seq]
bind_pure_comp := by aesop
bind_map := by
aesop
/-
Possible TODO for the future:
Enable the following definitions, and write a lot of supporting lemmas.
def bind (f : R →+* mv_polynomial τ S) (g : σ → mv_polynomial τ S) :
mv_polynomial σ R →+* mv_polynomial τ S :=
eval₂_hom f g
def join (f : R →+* S) : mv_polynomial (mv_polynomial σ R) S →ₐ[S] mv_polynomial σ S :=
aeval (map f)
def ajoin [algebra R S] : mv_polynomial (mv_polynomial σ R) S →ₐ[S] mv_polynomial σ S :=
join (algebra_map R S)
-/
