noncomputable def
TensorProduct.opLinearEquiv
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R A]
[Module R B]
:
Equations
Instances For
@[simp]
theorem
TensorProduct.opLinearEquiv_tmul
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R A]
[Module R B]
(x : A)
(y : B)
:
@[simp]
theorem
TensorProduct.opLinearEquiv_symm_tmul
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R A]
[Module R B]
(x : Aᵐᵒᵖ)
(y : Bᵐᵒᵖ)
:
noncomputable instance
MulOpposite.coalgebraStruct
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[CoalgebraStruct R A]
:
Equations
- MulOpposite.coalgebraStruct = { comul := ↑TensorProduct.opLinearEquiv ∘ₗ CoalgebraStruct.comul.op, counit := CoalgebraStruct.counit ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm }
theorem
MulOpposite.comul_def
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[CoalgebraStruct R A]
:
theorem
MulOpposite.comul_def'
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[CoalgebraStruct R A]
:
theorem
MulOpposite.counit_def
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[CoalgebraStruct R A]
:
theorem
LinearMap.op_eq
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[Module R A]
[Module R B]
(f : A →ₗ[R] B)
:
noncomputable instance
MulOpposite.coalgebra
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[AddCommMonoid A]
[Module R A]
[Coalgebra R A]
:
Equations
- MulOpposite.coalgebra = { toCoalgebraStruct := MulOpposite.coalgebraStruct, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }