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
@[implicit_reducible]
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แตแต’แต–
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
@[implicit_reducible]
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แตแต’แต–