The coalgebra structure on monoid algebras

Given a type X, a commutative semiring R and a semiring A which is also an R-coalgebra, this file collects results about the R-coalgebra instance on A[X] inherited from the corresponding structure on its coefficients, defined in Mathlib/RingTheory/Coalgebra/Basic.lean.

Main definitions

• (Add)MonoidAlgebra.instCoalgebra: the R-coalgebra structure on A[X] when A is an R-coalgebra.
• LaurentPolynomial.instCoalgebra: the R-coalgebra structure on the Laurent polynomials A[T;T⁻¹] when A is an R-coalgebra.

noncomputable instance MonoidAlgebra.instCoalgebra (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] (X : Type u_3) [Module R A] [Coalgebra R A] : Coalgebra R (MonoidAlgebra A X)

Equations

• MonoidAlgebra.instCoalgebra R A X = Finsupp.instCoalgebra R X A

@[simp]

theorem MonoidAlgebra.counit_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.counit (single x a) = CoalgebraStruct.counit a

@[simp]

theorem MonoidAlgebra.comul_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.comul (single x a) = (TensorProduct.map (lsingle x) (lsingle x)) (CoalgebraStruct.comul a)

noncomputable instance AddMonoidAlgebra.instCoalgebra (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] (X : Type u_3) [Module R A] [Coalgebra R A] : Coalgebra R (AddMonoidAlgebra A X)

Equations

• AddMonoidAlgebra.instCoalgebra R A X = Finsupp.instCoalgebra R X A

@[simp]

theorem AddMonoidAlgebra.counit_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.counit (single x a) = CoalgebraStruct.counit a

@[simp]

theorem AddMonoidAlgebra.comul_single {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.comul (single x a) = (TensorProduct.map (lsingle x) (lsingle x)) (CoalgebraStruct.comul a)

noncomputable instance LaurentPolynomial.instCoalgebra (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] : Coalgebra R (LaurentPolynomial A)

Equations

• LaurentPolynomial.instCoalgebra R A = inferInstanceAs (Coalgebra R (AddMonoidAlgebra A ℤ))

@[simp]

theorem LaurentPolynomial.comul_C {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) : CoalgebraStruct.comul (C a) = (TensorProduct.map (AddMonoidAlgebra.lsingle 0) (AddMonoidAlgebra.lsingle 0)) (CoalgebraStruct.comul a)

@[simp]

theorem LaurentPolynomial.comul_C_mul_T {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) (n : ℤ) : CoalgebraStruct.comul (C a * T n) = (TensorProduct.map (AddMonoidAlgebra.lsingle n) (AddMonoidAlgebra.lsingle n)) (CoalgebraStruct.comul a)

theorem LaurentPolynomial.comul_C_mul_T_self {R : Type u_1} [CommSemiring R] (a : R) (n : ℤ) : CoalgebraStruct.comul (C a * T n) = T n ⊗ₜ[R] (C a * T n)

@[simp]

theorem LaurentPolynomial.counit_C {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) : CoalgebraStruct.counit (C a) = CoalgebraStruct.counit a

@[simp]

theorem LaurentPolynomial.counit_C_mul_T {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) (n : ℤ) : CoalgebraStruct.counit (C a * T n) = CoalgebraStruct.counit a