Coalgebra.coassoc
theorem Coalgebra.coassoc :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
[self : Coalgebra R A],
↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul =
LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul
This theorem states that the comultiplication operation in a coalgebra over a commutative semiring is coassociative. In the context of a coalgebra structure (with a commutative semiring R and an additive commutative monoid A that also forms a module over R), the theorem asserts that the composition of the associator function for tensor products with the sequence of comultiplication operations (first applied to the right tensor factor and then to the result) is equivalent to the sequence of comultiplication operations (first applied, then applied to the left tensor factor using a natural linear map induced by comultiplication). In mathematical terms, it asserts that the diagram involving these operations commutes, embodying the property of coassociativity.
More concisely: In a coalgebra over a commutative semiring, the order of applying the comultiplication operations is irrelevant, i.e., (comultiplication ∘ tensor²) is equal to (tensor² ∘ comultiplication).
|
Coalgebra.lTensor_counit_comp_comul
theorem Coalgebra.lTensor_counit_comp_comul :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
[self : Coalgebra R A],
LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R A R).flip 1
This theorem, `Coalgebra.lTensor_counit_comp_comul`, states that for any type `R` equipped with a `CommSemiring` structure, and any type `A` equipped with both an `AddCommMonoid` and a `Module` structure over `R`, the composition of the `lTensor` of the `counit` of a `Coalgebra` over `R` and `A`, followed by the `comul` of the `Coalgebra`, is equal to the flipped version of the `TensorProduct.mk` of `R`, `A`, and `R` when applied to the number 1. In terms of category theory, this is saying that the right counitality law holds in the category of coalgebras.
More concisely: For any `CommSemiring R`, `AddCommMonoid A`, and `Module A R`, the composition of the `lTensor` of `Coalgebra.counit` and `Coalgebra.comul` over `R` and `A` equals the flipped `TensorProduct.mk` of `R`, `A`, and `R` applied to 1. (or: The right counitality law holds in the category of coalgebras over `R` and `AddCommMonoid A`.)
|
Coalgebra.rTensor_counit_comp_comul
theorem Coalgebra.rTensor_counit_comp_comul :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
[self : Coalgebra R A], LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R R A) 1
The theorem `Coalgebra.rTensor_counit_comp_comul` states that for any type `R` with a commutative semiring structure, type `A` with an additive commutative monoid and a module structure over `R`, and a coalgebra over `R` and `A`, the composition of the right tensor product of `A` and the coalgebra counit with the coalgebra comultiplication equals the tensor product of `R`, `R` and `A` applied to `1`. This is a condition ensuring that the counit operation respects the structure of the coalgebra, often referred to as the left counitality law.
More concisely: For any commutative semiring R, additive commutative monoid and R-module A with a coalgebra structure, the composition of the right tensor product of A and the coalgebra counit with the coalgebra comultiplication equals the tensor product of R, R, and A applied to 1. (i.e., Coalgas Albanese R A -> R <.> R <.> A = ∫ x : Coalgas Albanese R A, tensor R R ℵ1 x)
|