The multiplicative opposite linear equivalence

This file defines the multiplicative opposite linear equivalence as linear maps op and unop. This is essentially mul_opposite.op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ but defined as linear maps rather than linear_equiv.

We also define ten_swap which is the linear automorphisms on A ⊗[R] Aᵐᵒᵖ given by swapping the tensor factors while keeping the ᵒᵖ in place, i.e., ten_swap (x ⊗ₜ op y) = y ⊗ₜ op x.

@[reducible, inline]

abbrev op (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] : A ≃ₗ[R] Aᵐᵒᵖ

Equations

• op R = MulOpposite.opLinearEquiv R

@[simp]

theorem op_apply {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] (x : A) : (op R) x = MulOpposite.op x

@[reducible, inline]

abbrev unop (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] : Aᵐᵒᵖ ≃ₗ[R] A

Equations

• unop R = (op R).symm

@[simp]

theorem unop_apply {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] (x : Aᵐᵒᵖ) : (unop R) x = MulOpposite.unop x

@[simp]

theorem unop_op {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] (x : A) : (unop R) ((op R) x) = x

@[simp]

theorem op_unop {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] (x : Aᵐᵒᵖ) : (op R) ((unop R) x) = x

theorem unop_comp_op {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] : ↑(unop R) ∘ₗ ↑(op R) = 1

theorem op_comp_unop {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] : ↑(op R) ∘ₗ ↑(unop R) = 1

theorem op_star_apply {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] [Star A] (a : A) : (op R) (star a) = star ((op R) a)

theorem unop_star_apply {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] [Star A] (a : Aᵐᵒᵖ) : (unop R) (star a) = star ((unop R) a)

@[reducible, inline]

noncomputable abbrev tenSwap (R : Type u_2) {A : Type u_3} {B : Type u_4} [AddCommMonoid A] [AddCommMonoid B] [CommSemiring R] [Module R A] [Module R B] : TensorProduct R A Bᵐᵒᵖ ≃ₗ[R] TensorProduct R B Aᵐᵒᵖ

Equations

• tenSwap R = (TensorProduct.comm R A Bᵐᵒᵖ).trans (LinearEquiv.TensorProduct.map (unop R) (op R))

@[simp]

theorem tenSwap_apply {R : Type u_3} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] {B : Type u_1} [AddCommMonoid B] [Module R B] (x : A) (y : Bᵐᵒᵖ) : (tenSwap R) (x ⊗ₜ[R] y) = MulOpposite.unop y ⊗ₜ[R] MulOpposite.op x

theorem tenSwap_apply' {R : Type u_3} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] {B : Type u_1} [AddCommMonoid B] [Module R B] (x : A) (y : B) : (tenSwap R) (x ⊗ₜ[R] MulOpposite.op y) = y ⊗ₜ[R] MulOpposite.op x

@[simp]

theorem tenSwap_symm {R : Type u_3} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] {B : Type u_1} [AddCommMonoid B] [Module R B] : (tenSwap R).symm = tenSwap R

theorem tenSwap_comp_tenSwap {R : Type u_3} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] {B : Type u_1} [AddCommMonoid B] [Module R B] : ↑(tenSwap R) ∘ₗ ↑(tenSwap R) = 1

@[simp]

theorem tenSwap_apply_tenSwap {R : Type u_2} {A : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] {B : Type u_1} [AddCommMonoid B] [Module R B] (x : TensorProduct R A Bᵐᵒᵖ) : (tenSwap R) ((tenSwap R) x) = x