1. Physlib
  2. Relativity
  3. Fermions
  4. Weyl
  5. Two
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.Fermions.Weyl.LeftHanded public import Physlib.Relativity.Fermions.Weyl.RightHanded public import Physlib.Relativity.Fermions.Weyl.DualLeftHanded public import Physlib.Relativity.Fermions.Weyl.DualRightHanded

Tensor product of two Weyl fermion

@[expose] public section

Equivalences to matrices.

Equivalence of leftHanded ⊗ leftHanded to 2 x 2 complex matrices.

def leftLeftToMatrix : (LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct LeftHandedWeyl.basis LeftHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding leftLeftToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis) (i, j) = M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of dualLeftHanded ⊗ dualLeftHanded to 2 x 2 complex matrices.

def dualLeftdualLeftToMatrix : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding dualLeftdualLeftToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis) (i, j) = M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of leftHanded ⊗ dualLeftHanded to 2 x 2 complex matrices.

def leftDualLeftToMatrix : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct LeftHandedWeyl.basis DualLeftHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding leftDualLeftToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis) (i, j) = M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of dualLeftHanded ⊗ leftHanded to 2 x 2 complex matrices.

def dualLeftLeftToMatrix : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct DualLeftHandedWeyl.basis LeftHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding dualLeftLeftToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis) (i, j) = M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of rightHanded ⊗ rightHanded to 2 x 2 complex matrices.

def rightRightToMatrix : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct RightHandedWeyl.basis RightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding rightRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (i, j) = M i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of dualRightHanded ⊗ dualRightHanded to 2 x 2 complex matrices.

def dualRightDualRightToMatrix : (DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct DualRightHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding dualRightDualRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (i, j) = M i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of rightHanded ⊗ dualRightHanded to 2 x 2 complex matrices.

def rightDualRightToMatrix : (RightHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct RightHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding rightDualRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (i, j) = M i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of dualRightHanded ⊗ rightHanded to 2 x 2 complex matrices.

def dualRightRightToMatrix : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct DualRightHandedWeyl.basis RightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding dualRightRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (i, j) = M i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of dualLeftHanded ⊗ dualRightHanded to 2 x 2 complex matrices.

def dualLeftDualRightToMatrix : (DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct DualLeftHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding dualLeftDualRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis) (i, j) = M i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

Equivalence of leftHanded ⊗ rightHanded to 2 x 2 complex matrices.

def leftRightToMatrix : (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ := (Basis.tensorProduct LeftHandedWeyl.basis RightHandedWeyl.basis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

Expanding leftRightToMatrix in terms of the standard basis.

M:Matrix (Fin 2) (Fin 2) ℂ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (x, y) • (LeftHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (x, y) = ∑ i, ∑ j, M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j M:Matrix (Fin 2) (Fin 2) ℂi:Fin 2x✝¹:i ∈ Finset.univj:Fin 2x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M)) (i, j) • (LeftHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (i, j) = M i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j All goals completed! 🐙 M:Matrix (Fin 2) (Fin 2) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2)).symm ((LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)).symm M) ∈ Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙

The coercion of Finsupp.linearEquivFunOnFinite to a function is the underlying finitely-supported function, used to bridge it with Matrix.mulVec.

private lemma coe_linearEquivFunOnFinite (g : (Fin 2 × Fin 2) →₀ ℂ) : Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) g = ⇑g := rfl

Group actions

The group action of SL(2,ℂ) on leftHanded ⊗ leftHanded is equivalent to M.1 * leftLeftToMatrix v * (M.1)ᵀ.

set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙

The group action of SL(2,ℂ) on dualLeftHanded ⊗ dualLeftHanded is equivalent to (M.1⁻¹)ᵀ * leftLeftToMatrix v * (M.1⁻¹).

set_option backward.isDefEq.respectTransparency false inv:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j⊢ ∑ y, ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j y * dualLeftdualLeftToMatrix v x y = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j⊢ (fun y => ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j y * dualLeftdualLeftToMatrix v x y) = fun x => ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * dualLeftdualLeftToMatrix v x_1 x = ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * dualLeftdualLeftToMatrix v x_1 x) = fun x1 => (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * dualLeftdualLeftToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2x1:Fin 2⊢ (↑M)⁻¹ x1 i * (↑M)⁻¹ x j * dualLeftdualLeftToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftdualLeftToMatrix v x1 x * (↑M)⁻¹ x j All goals completed! 🐙

The group action of SL(2,ℂ) on leftHanded ⊗ dualLeftHanded is equivalent to M.1 * leftDualLeftToMatrix v * (M.1⁻¹).

set_option backward.isDefEq.respectTransparency false inv:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j⊢ ∑ y, ∑ x, (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j y * leftDualLeftToMatrix v x y = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j⊢ (fun y => ∑ x, (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j y * leftDualLeftToMatrix v x y) = fun x => ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * leftDualLeftToMatrix v x_1 x = ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * leftDualLeftToMatrix v x_1 x) = fun x1 => ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) i x1 * (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) j x * leftDualLeftToMatrix v x1 x = ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j v:LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x) * (↑M)⁻¹ x j = ∑ x, ∑ x1, ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x jx:Fin 2x1:Fin 2⊢ ↑M i x1 * (↑M)⁻¹ x j * leftDualLeftToMatrix v x1 x = ↑M i x1 * leftDualLeftToMatrix v x1 x * (↑M)⁻¹ x j All goals completed! 🐙

The group action of SL(2,ℂ) on dualLeftHanded ⊗ leftHanded is equivalent to (M.1⁻¹)ᵀ * leftDualLeftToMatrix v * (M.1)ᵀ.

set_option backward.isDefEq.respectTransparency false inv:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) j y * dualLeftLeftToMatrix v x y = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x v:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x⊢ (fun y => ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) j y * dualLeftLeftToMatrix v x y) = fun x => ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x v:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) j x * dualLeftLeftToMatrix v x_1 x = ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x v:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) j x * dualLeftLeftToMatrix v x_1 x) = fun x1 => (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x v:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x1 * (LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M) j x * dualLeftLeftToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x v:DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x) * ↑M j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j xx:Fin 2x1:Fin 2⊢ (↑M)⁻¹ x1 i * ↑M j x * dualLeftLeftToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftLeftToMatrix v x1 x * ↑M j x All goals completed! 🐙

The group action of SL(2,ℂ) on rightHanded ⊗ rightHanded is equivalent to (M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ.

set_option backward.isDefEq.respectTransparency false inv:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j y * rightRightToMatrix v x y = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x v:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x⊢ (fun y => ∑ x, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j y * rightRightToMatrix v x y) = fun x => ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x v:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * rightRightToMatrix v x_1 x = ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x v:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * rightRightToMatrix v x_1 x) = fun x1 => (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x v:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * rightRightToMatrix v x1 x = (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x v:RightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2x1:Fin 2⊢ (↑M).map star i x1 * (↑M).map star j x * rightRightToMatrix v x1 x = (↑M).map star i x1 * rightRightToMatrix v x1 x * (↑M).map star j x All goals completed! 🐙

The group action of SL(2,ℂ) on dualRightHanded ⊗ dualRightHanded is equivalent to ((M.1⁻¹).conjTranspose * rightRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ.

set_option backward.isDefEq.respectTransparency false inv:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * dualRightDualRightToMatrix v x y = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ (fun y => ∑ x, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * dualRightDualRightToMatrix v x y) = fun x => ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualRightDualRightToMatrix v x_1 x = ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualRightDualRightToMatrix v x_1 x) = fun x1 => (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualRightDualRightToMatrix v x1 x = (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (↑M)⁻¹ᴴ i x1 * (↑M)⁻¹ᴴ j x * dualRightDualRightToMatrix v x1 x = (↑M)⁻¹ᴴ i x1 * dualRightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x All goals completed! 🐙

The group action of SL(2,ℂ) on rightHanded ⊗ dualRightHanded is equivalent to (M.1.map star) * rightDualRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ.

set_option backward.isDefEq.respectTransparency false inv:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * rightDualRightToMatrix v x y = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ (fun y => ∑ x, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * rightDualRightToMatrix v x y) = fun x => ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * rightDualRightToMatrix v x_1 x = ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * rightDualRightToMatrix v x_1 x) = fun x1 => (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) i x1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * rightDualRightToMatrix v x1 x = (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:RightHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (↑M).map star i x1 * (↑M)⁻¹ᴴ j x * rightDualRightToMatrix v x1 x = (↑M).map star i x1 * rightDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x All goals completed! 🐙

The group action of SL(2,ℂ) on dualRightHanded ⊗ rightHanded is equivalent to ((M.1⁻¹).conjTranspose * rightDualRightToMatrix v * ((M.1.map star)).ᵀ.

set_option backward.isDefEq.respectTransparency false inv:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j y * dualRightRightToMatrix v x y = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x v:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x⊢ (fun y => ∑ x, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j y * dualRightRightToMatrix v x y) = fun x => ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x v:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * dualRightRightToMatrix v x_1 x = ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x v:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * dualRightRightToMatrix v x_1 x) = fun x1 => (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x v:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) i x1 * (LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M) j x * dualRightRightToMatrix v x1 x = (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x v:DualRightHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (↑M).map star j x = ∑ x, ∑ x1, (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j xx:Fin 2x1:Fin 2⊢ (↑M)⁻¹ᴴ i x1 * (↑M).map star j x * dualRightRightToMatrix v x1 x = (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x * (↑M).map star j x All goals completed! 🐙
v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ ∑ y, ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * dualLeftDualRightToMatrix v x y = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x⊢ (fun y => ∑ x, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j y * dualLeftDualRightToMatrix v x y) = fun x => ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ ∑ x_1, (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualLeftDualRightToMatrix v x_1 x = ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2⊢ (fun x_1 => (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x_1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualLeftDualRightToMatrix v x_1 x) = fun x1 => (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis) (DualLeftHandedWeyl.rep M) i x1 * (LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis) (DualRightHandedWeyl.rep M) j x * dualLeftDualRightToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x v:DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x = ∑ x, ∑ x1, (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j xx:Fin 2x1:Fin 2⊢ (↑M)⁻¹ x1 i * (↑M)⁻¹ᴴ j x * dualLeftDualRightToMatrix v x1 x = (↑M)⁻¹ x1 i * dualLeftDualRightToMatrix v x1 x * (↑M)⁻¹ᴴ j x All goals completed! 🐙v:LeftHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftRightToMatrix v x1 x) * (↑M)ᴴ x j = ∑ x, ∑ x1, ↑M i x1 * leftRightToMatrix v x1 x * (↑M)ᴴ x jx:Fin 2x1:Fin 2⊢ ↑M i x1 * (↑M).map star j x * leftRightToMatrix v x1 x = ↑M i x1 * leftRightToMatrix v x1 x * (↑M)ᵀ.map star x j v:LeftHandedWeyl ⊗[ℂ] RightHandedWeylM:SL(2, ℂ)i:Fin 2j:Fin 2h1:∑ x, (∑ x1, ↑M i x1 * leftRightToMatrix v x1 x) * (↑M)ᴴ x j = ∑ x, ∑ x1, ↑M i x1 * leftRightToMatrix v x1 x * (↑M)ᴴ x jx:Fin 2x1:Fin 2⊢ ↑M i x1 * (starRingEnd ℂ) (↑M j x) * leftRightToMatrix v x1 x = ↑M i x1 * leftRightToMatrix v x1 x * (starRingEnd ℂ) (↑M j x) All goals completed! 🐙

The symm version of the group actions.

All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙v:ℂ²ˣ²hv:IsSelfAdjoint vM:SL(2, ℂ)⊢ (↑M).adjugateᴴᵀ = (↑M).adjugateᵀᴴ All goals completed! 🐙v:ℂ²ˣ²hv:IsSelfAdjoint vM:SL(2, ℂ)⊢ leftRightToMatrix.symm (↑M * v * (↑M)ᴴ) = leftRightToMatrix.symm ↑((SL2C.toSelfAdjointMap M) ⟨v, hv⟩) All goals completed! 🐙