Documentation

LeanPool.Monlib4.LinearAlgebra.Ips.OpUnop

The multiplicative opposite linear equivalence #

This file defines the multiplicative opposite linear equivalence as linear maps op and unop.

We also define ten_swap, the linear automorphism on A ⊗[R] Aᵐᵒᵖ that swaps the tensor factors while keeping the ᵒᵖ in place.

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

The linear equivalence sending a vector to its multiplicative opposite.

Equations
Instances For
    source
    @[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
    source
    @[reducible, inline]
    abbrev unop (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] :
    Aᵐᵒᵖ ≃ₗ[R] A

    The inverse linear equivalence from the multiplicative opposite.

    Equations
    Instances For
      source
      @[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
      source
      @[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
      source
      @[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
      source
      theorem unop_comp_op {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] :
      ↑(unop R) ∘ₗ ↑(op R) = 1
      source
      theorem op_comp_unop {R : Type u_2} {A : Type u_1} [CommSemiring R] [AddCommMonoid A] [Module R A] :
      ↑(op R) ∘ₗ ↑(unop R) = 1
      source
      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)
      source
      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)
      source
      @[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ᵐᵒᵖ

      Swap tensor factors while moving the multiplicative-opposite marker to the other factor.

      Equations
      Instances For
        source
        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
        source
        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
        source
        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
        source
        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
        source
        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