LeanPool.Monlib4.LinearAlgebra.Coalgebra.MulOpposite

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.Coalgebra.MulOpposite.

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] : (TensorProduct R A B)ᵐᵒᵖ ≃ₗ[R] TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ

The tensor product of multiplicative opposites as the opposite of a tensor product.

Equations

• TensorProduct.opLinearEquiv = (MulOpposite.opLinearEquiv R).symm.trans (LinearEquiv.TensorProduct.map (MulOpposite.opLinearEquiv R) (MulOpposite.opLinearEquiv R))

@[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) : opLinearEquiv (MulOpposite.op (x ⊗ₜ[R] y)) = MulOpposite.op x ⊗ₜ[R] MulOpposite.op y

@[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ᵐᵒᵖ) : opLinearEquiv.symm (x ⊗ₜ[R] y) = MulOpposite.op (MulOpposite.unop x ⊗ₜ[R] MulOpposite.unop y)

@[implicit_reducible]

noncomputable instance MulOpposite.coalgebraStruct {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct 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] : CoalgebraStruct.comul = ↑TensorProduct.opLinearEquiv ∘ₗ CoalgebraStruct.comul.op

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

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) : f.op = ↑(MulOpposite.opLinearEquiv R) ∘ₗ f ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm

@[reducible]

noncomputable instance MulOpposite.coalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Coalgebra R Aᵐᵒᵖ

Equations

• MulOpposite.coalgebra = { toCoalgebraStruct := MulOpposite.coalgebraStruct, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }