mathlib3 documentation

monlib / linear_algebra.my_ips.op_unop

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.

def op {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

A →ₗ[R] Aᵐᵒᵖ

Equations

op = ↑(mul_opposite.op_linear_equiv R)

theorem op_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : A) :

⇑op x = mul_opposite.op x

def unop {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

Aᵐᵒᵖ →ₗ[R] A

Equations

unop = ↑((mul_opposite.op_linear_equiv R).symm)

theorem unop_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : Aᵐᵒᵖ) :

⇑unop x = mul_opposite.unop x

theorem unop_op {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : A) :

⇑unop (⇑op x) = x

theorem op_unop {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : Aᵐᵒᵖ) :

⇑op (⇑unop x) = x

theorem unop_comp_op {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

unop.comp op = 1

theorem op_comp_unop {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

op.comp unop = 1

theorem op_star_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] [has_star A] (a : A) :

⇑op (has_star.star a) = has_star.star (⇑op a)

theorem unop_star_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] [has_star A] (a : Aᵐᵒᵖ) :

⇑unop (has_star.star a) = has_star.star (⇑unop a)

def ten_swap {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

tensor_product R A Aᵐᵒᵖ →ₗ[R] tensor_product R A Aᵐᵒᵖ

Equations

ten_swap = (tensor_product.map unop op).comp (tensor_product.comm R A Aᵐᵒᵖ).to_linear_map

theorem ten_swap_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : A) (y : Aᵐᵒᵖ) :

⇑ten_swap (x ⊗ₜ[R] y) = mul_opposite.unop y ⊗ₜ[R] mul_opposite.op x

theorem ten_swap_apply' {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x y : A) :

⇑ten_swap (x ⊗ₜ[R] mul_opposite.op y) = y ⊗ₜ[R] mul_opposite.op x

theorem ten_swap_ten_swap {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

ten_swap.comp ten_swap = 1

theorem ten_swap_apply_ten_swap {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] (x : tensor_product R A Aᵐᵒᵖ) :

⇑ten_swap (⇑ten_swap x) = x

def ten_swap_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [add_comm_monoid A] [module R A] :

function.injective ⇑ten_swap