Documentation

Mathlib.RingTheory.Coalgebra.MulOpposite

MulOpposite of coalgebras #

Suppose R is a commutative semiring, and A is an R-coalgebra, then Aแตแต’แต– is an R-coalgebra, where we define the comultiplication and counit maps naturally.

source
๐Ÿ”ธ coverage
noncomputable instance MulOpposite.instCoalgebraStruct {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
CoalgebraStruct R Aแตแต’แต–
Equations
    source
    ๐Ÿ“ coverage
    theorem MulOpposite.comul_def {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
    CoalgebraStruct.comul = TensorProduct.map โ†‘(opLinearEquiv R) โ†‘(opLinearEquiv R) โˆ˜โ‚— CoalgebraStruct.comul โˆ˜โ‚— โ†‘(opLinearEquiv R).symm
    source
    ๐Ÿ“ coverage
    theorem MulOpposite.counit_def {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
    CoalgebraStruct.counit = CoalgebraStruct.counit โˆ˜โ‚— โ†‘(opLinearEquiv R).symm
    source
    ๐Ÿ”ธ coverage
    noncomputable instance MulOpposite.instCoalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] :
    Coalgebra R Aแตแต’แต–
    Equations