Base change of coalgebras #
This file records formulas for the coalgebra structure on a scalar extension A ⊗[R] H.
Cocommutativity can be checked after faithfully flat extension of scalars, without requiring
an algebra structure on the coalgebra.
Main declarations #
TauCeti.Coalgebra.baseChange_comul_tmul: the comultiplication of a scalar extension on pure tensors.TauCeti.Coalgebra.IsCocomm.of_baseChange: cocommutativity descends along a faithfully flat commutative algebra.
theorem
TauCeti.Coalgebra.baseChange_comul_tmul
{R : Type u}
(A : Type v)
{H : Type w}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[AddCommMonoid H]
[Module R H]
[CoalgebraStruct R H]
(a : A)
(h : H)
:
CoalgebraStruct.comul (a ⊗ₜ[R] h) = (TensorProduct.AlgebraTensorModule.distribBaseChange R A H H) (a ⊗ₜ[R] CoalgebraStruct.comul h)
The comultiplication of a base-changed coalgebra on a pure tensor.
theorem
TauCeti.Coalgebra.IsCocomm.of_baseChange
{k : Type u}
{K : Type v}
{H : Type w}
[CommRing k]
[CommRing K]
[Algebra k K]
[Module.FaithfullyFlat k K]
[AddCommGroup H]
[Module k H]
[Coalgebra k H]
[h : Coalgebra.IsCocomm K (TensorProduct k K H)]
:
Cocommutativity descends along a faithfully flat commutative algebra.