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.

@[instance_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ᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

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

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

@[instance_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ᵐᵒᵖ

Equations

• MulOpposite.instCoalgebra = { toCoalgebraStruct := MulOpposite.instCoalgebraStruct, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }