Physlib.Relativity.SL2C.Basic

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.SL2C.SelfAdjoint
public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Physlib.Relativity.LorentzGroup.Restricted.Basic

The group SL(2, ℂ) and it's relation to the Lorentz group

The aim of this file is to give the relationship between SL(2, ℂ) and the Lorentz group.

@[expose] public section

Some basic properties about SL(2, ℂ)

Possibly to be moved to mathlib at some point.



lemma inverse_coe (M : SL(2, ℂ)) : M.1⁻¹ = (M⁻¹).1 := byM:SL(2, ℂ)⊢ (↑M)⁻¹ = ↑M⁻¹
  rw [SpecialLinearGroup.coe_inv,M:SL(2, ℂ)⊢ (↑M)⁻¹ = (↑M).adjugateM:SL(2, ℂ)⊢ Ring.inverse 1 • (↑M).adjugate = (↑M).adjugate Matrix.inv_def,M:SL(2, ℂ)⊢ Ring.inverse (↑M).det • (↑M).adjugate = (↑M).adjugateM:SL(2, ℂ)⊢ Ring.inverse 1 • (↑M).adjugate = (↑M).adjugate SpecialLinearGroup.det_coeM:SL(2, ℂ)⊢ Ring.inverse 1 • (↑M).adjugate = (↑M).adjugateM:SL(2, ℂ)⊢ Ring.inverse 1 • (↑M).adjugate = (↑M).adjugate]M:SL(2, ℂ)⊢ Ring.inverse 1 • (↑M).adjugate = (↑M).adjugate
  simpAll goals completed! 🐙

lemma transpose_coe (M : SL(2, ℂ)) : M.1ᵀ = (M.transpose).1 := rfl

Representation of SL(2, ℂ) on spacetime

Through the correspondence between spacetime and self-adjoint matrices, we can define a representation a representation of SL(2, ℂ) on spacetime.

Given an element M ∈ SL(2, ℂ) the linear map from selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) to itself defined by A ↦ M * A * Mᴴ.

@[simps!]
noncomputable def toSelfAdjointMap (M : SL(2, ℂ)) :
    selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
  toFun A := ⟨M.1 * A.1 * Matrix.conjTranspose M,
    byM:SL(2, ℂ)A:↥(selfAdjoint ℂ²ˣ²)⊢ ↑M * ↑A * (↑M)ᴴ ∈ selfAdjoint ℂ²ˣ²
      noncomm_ring [selfAdjoint.mem_iff, star_eq_conjTranspose,
        conjTranspose_mul, conjTranspose_conjTranspose,
        (star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]All goals completed! 🐙⟩
  map_add' A B := byM:SL(2, ℂ)A:↥(selfAdjoint ℂ²ˣ²)B:↥(selfAdjoint ℂ²ˣ²)⊢ ⟨↑M * ↑(A + B) * (↑M)ᴴ, ⋯⟩ = ⟨↑M * ↑A * (↑M)ᴴ, ⋯⟩ + ⟨↑M * ↑B * (↑M)ᴴ, ⋯⟩
    simp only [AddSubgroup.coe_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]M:SL(2, ℂ)A:↥(selfAdjoint ℂ²ˣ²)B:↥(selfAdjoint ℂ²ˣ²)⊢ ↑M * (↑A + ↑B) * (↑M)ᴴ = ↑M * ↑A * (↑M)ᴴ + ↑M * ↑B * (↑M)ᴴ
    noncomm_ring [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, AddSubmonoid.mk_add_mk,
      Subtype.mk.injEq]All goals completed! 🐙
  map_smul' r A := byM:SL(2, ℂ)r:ℝA:↥(selfAdjoint ℂ²ˣ²)⊢ ⟨↑M * ↑(r • A) * (↑M)ᴴ, ⋯⟩ = (RingHom.id ℝ) r • ⟨↑M * ↑A * (↑M)ᴴ, ⋯⟩
    noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
      RingHom.id_apply]All goals completed! 🐙

              lemma toSelfAdjointMap_apply (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
    toSelfAdjointMap M A = ⟨M.1 * A.1 * Matrix.conjTranspose M, byM:SL(2, ℂ)A:↥(selfAdjoint ℂ²ˣ²)⊢ ↑M * ↑A * (↑M)ᴴ ∈ selfAdjoint ℂ²ˣ²
        noncomm_ring [selfAdjoint.mem_iff, star_eq_conjTranspose,
        conjTranspose_mul, conjTranspose_conjTranspose,
        (star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]All goals completed! 🐙⟩ := rfllemma toSelfAdjointMap_apply_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
    det ((toSelfAdjointMap M) A).1 = det A.1 := byM:SL(2, ℂ)A:↥(selfAdjoint ℂ²ˣ²)⊢ (↑((toSelfAdjointMap M) A)).det = (↑A).det
  simp [toSelfAdjointMap]All goals completed! 🐙

lemma toSelfAdjointMap_apply_pauliBasis'_inl (M : SL(2, ℂ)) :
    toSelfAdjointMap M (PauliMatrix.pauliBasis' (Sum.inl 0)) =
    ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) •
      PauliMatrix.pauliBasis' (Sum.inl 0) +
    (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
      (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) •
        PauliMatrix.pauliBasis' (Sum.inr 0)
    + ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) •
        PauliMatrix.pauliBasis' (Sum.inr 1)
    + ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) •
      PauliMatrix.pauliBasis' (Sum.inr 2) := byM:SL(2, ℂ)⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) =
  ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inl 0) +
        -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im +
              (↑M 0 0).re * (↑M 1 0).re) •
          PauliMatrix.pauliBasis' (Sum.inr 0) +
      (-(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re) •
        PauliMatrix.pauliBasis' (Sum.inr 1) +
    ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inr 2)
  simp only [toSelfAdjointMap, PauliMatrix.pauliBasis', Fin.isValue, Basis.coe_mk,
    PauliMatrix.pauliSelfAdjoint', PauliMatrix.pauliMatrix, one_fin_two, LinearMap.coe_mk,
    AddHom.coe_mk, neg_add_rev, neg_of, neg_cons, neg_zero, neg_empty, neg_mul, neg_neg]M:SL(2, ℂ)⊢ ⟨↑M * !![1, 0; 0, 1] * (↑M)ᴴ, ⋯⟩ =
  ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • ⟨!![1, 0; 0, 1], ⋯⟩ +
        (-((↑M 0 0).re * (↑M 1 0).re) +
            (-((↑M 0 0).im * (↑M 1 0).im) + (-((↑M 0 1).im * (↑M 1 1).im) + -((↑M 0 1).re * (↑M 1 1).re)))) •
          ⟨!![0, -1; -1, 0], ⋯⟩ +
      (-((↑M 0 0).re * (↑M 1 0).im) + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im +
          (↑M 0 1).im * (↑M 1 1).re) •
        ⟨!![0, I; -I, 0], ⋯⟩ +
    ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • ⟨!![-1, 0; 0, 1], ⋯⟩
  ext1M:SL(2, ℂ)⊢ ↑⟨↑M * !![1, 0; 0, 1] * (↑M)ᴴ, ⋯⟩ =
  ↑(((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • ⟨!![1, 0; 0, 1], ⋯⟩ +
          (-((↑M 0 0).re * (↑M 1 0).re) +
              (-((↑M 0 0).im * (↑M 1 0).im) + (-((↑M 0 1).im * (↑M 1 1).im) + -((↑M 0 1).re * (↑M 1 1).re)))) •
            ⟨!![0, -1; -1, 0], ⋯⟩ +
        (-((↑M 0 0).re * (↑M 1 0).im) + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im +
            (↑M 0 1).im * (↑M 1 1).re) •
          ⟨!![0, I; -I, 0], ⋯⟩ +
      ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • ⟨!![-1, 0; 0, 1], ⋯⟩)
  simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_of, smul_cons, real_smul,
    ofReal_div, ofReal_add, ofReal_pow, ofReal_ofNat, mul_one, smul_zero, smul_empty, smul_neg,
    ofReal_neg, ofReal_mul, neg_add_rev, neg_neg, of_add_of, add_cons, head_cons, add_zero,
    tail_cons, zero_add, empty_add_empty, ofReal_sub]M:SL(2, ℂ)⊢ ↑M * !![1, 0; 0, 1] * (↑M)ᴴ =
  !![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I;
    ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]
  conv =>M:SL(2, ℂ)| ↑M * !![1, 0; 0, 1] * (↑M)ᴴ =
  !![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I;
    ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2] lhsM:SL(2, ℂ)| ↑M * !![1, 0; 0, 1] * (↑M)ᴴ; erw [← eta_fin_two 1, mul_one]M:SL(2, ℂ)| ↑M * (↑M)ᴴ
  conv =>M:SL(2, ℂ)| ↑M * (↑M)ᴴ =
  !![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I;
    ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2] lhsM:SL(2, ℂ)| ↑M * (↑M)ᴴ; lhsM:SL(2, ℂ)| ↑M; rw [eta_fin_two M.1]M:SL(2, ℂ)| !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1]
  conv =>M:SL(2, ℂ)| !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1] * (↑M)ᴴ =
  !![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I;
    ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2] lhsM:SL(2, ℂ)| !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1] * (↑M)ᴴ; rhsM:SL(2, ℂ)| (↑M)ᴴ; rw [eta_fin_two M.1ᴴ]M:SL(2, ℂ)| !![(↑M)ᴴ 0 0, (↑M)ᴴ 0 1; (↑M)ᴴ 1 0, (↑M)ᴴ 1 1]
  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def, cons_mul, Nat.succ_eq_add_one,
    Nat.reduceAdd, vecMul_cons, head_cons, smul_cons, smul_eq_mul, smul_empty, tail_cons,
    empty_vecMul, add_zero, add_cons, empty_add_empty, empty_mul, Equiv.symm_apply_apply,
    EmbeddingLike.apply_eq_iff_eq]M:SL(2, ℂ)⊢ ![![↑M 0 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑M 1 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 1 1)]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
  rw [mul_conj',M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑M 0 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑M 1 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 1 1)]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]] mul_conj',M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑M 1 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 1 1)]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]] mul_conj',M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1),
      ↑‖↑M 1 0‖ ^ 2 + ↑M 1 1 * (starRingEnd ℂ) (↑M 1 1)]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]] mul_conj'M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]]M:SL(2, ℂ)⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
    ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]] =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
      ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
            ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
          I],
    ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
          ↑(↑M 0 0).re * ↑(↑M 1 0).re +
        -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I),
      (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
        (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
  ext x yM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
      ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]]
    x y =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
        ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I],
      ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
                ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
              I),
        (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
    x y
  match x, y with
  | 0, 0 | 1, 1 =>M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
      ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]]
    1 1 =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
        ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I],
      ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
                ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
              I),
        (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
    1 1M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
      ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]]
    0 0 =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
        ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I],
      ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
                ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
              I),
        (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
    0 0
    simp only [Fin.isValue, cons_val', cons_val_zero, cons_val_one, empty_val', cons_val_fin_one]M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2 =
  (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
    (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2
    ring_nfAll goals completed! 🐙
  | 0, 1 | 1, 0 =>M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
      ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]]
    1 0 =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
        ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I],
      ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
                ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
              I),
        (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
    1 0M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ![![↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2, ↑M 0 0 * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1)],
      ![↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1), ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2]]
    0 1 =
  ![![(↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          -((-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2),
        ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          (-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
              ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
            I],
      ![↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
            ↑(↑M 0 0).re * ↑(↑M 1 0).re +
          -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
                ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
              I),
        (↑‖↑M 0 0‖ ^ 2 + ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2 +
          (-↑‖↑M 0 0‖ ^ 2 - ↑‖↑M 0 1‖ ^ 2 + ↑‖↑M 1 0‖ ^ 2 + ↑‖↑M 1 1‖ ^ 2) / 2]]
    0 1
    simp only [Fin.isValue, cons_val', cons_val_zero, cons_val_one, empty_val', cons_val_fin_one]M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1) =
  ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).im * ↑(↑M 1 1).im + ↑(↑M 0 0).im * ↑(↑M 1 0).im +
      ↑(↑M 0 0).re * ↑(↑M 1 0).re +
    -((-(↑(↑M 0 0).re * ↑(↑M 1 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).im - ↑(↑M 0 1).re * ↑(↑M 1 1).im +
          ↑(↑M 0 1).im * ↑(↑M 1 1).re) *
        I)
    ring_nfM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ ↑M 1 0 * (starRingEnd ℂ) (↑M 0 0) + ↑M 1 1 * (starRingEnd ℂ) (↑M 0 1) =
  ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).re * ↑(↑M 1 1).im * I - ↑(↑M 1 1).re * ↑(↑M 0 1).im * I +
            ↑(↑M 0 1).im * ↑(↑M 1 1).im +
          ↑(↑M 0 0).im * ↑(↑M 1 0).im -
        ↑(↑M 0 0).im * ↑(↑M 1 0).re * I +
      ↑(↑M 1 0).im * ↑(↑M 0 0).re * I +
    ↑(↑M 0 0).re * ↑(↑M 1 0).re
    rw [← re_add_im (M.1 0 0),M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) * (starRingEnd ℂ) (↑M 1 0) + ↑M 0 1 * (starRingEnd ℂ) (↑M 1 1) =
  ↑(↑M 0 1).re * ↑(↑M 1 1).re - ↑(↑M 0 1).re * ↑(↑M 1 1).im * I + ↑(↑M 1 1).re * ↑(↑M 0 1).im * I +
            ↑(↑M 0 1).im * ↑(↑M 1 1).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑M 1 0).im +
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑M 1 0).re * I -
      ↑(↑M 1 0).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑M 1 0).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re ← re_add_im (M.1 0 1),M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) * (starRingEnd ℂ) (↑M 1 0) +
    (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) * (starRingEnd ℂ) (↑M 1 1) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑M 1 1).re - ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑M 1 1).im * I +
              ↑(↑M 1 1).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑M 1 1).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑M 1 0).im +
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑M 1 0).re * I -
      ↑(↑M 1 0).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑M 1 0).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re ← re_add_im (M.1 1 0),M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) * (starRingEnd ℂ) (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) +
    (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) * (starRingEnd ℂ) (↑M 1 1) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑M 1 1).re - ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑M 1 1).im * I +
              ↑(↑M 1 1).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑M 1 1).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im +
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I -
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re ← re_add_im (M.1 1 1)M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) * (starRingEnd ℂ) (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) +
    (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) * (starRingEnd ℂ) (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re -
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I +
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im +
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I -
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re]M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) * (starRingEnd ℂ) (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) +
    (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) * (starRingEnd ℂ) (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re -
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I +
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im +
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I -
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).reM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (starRingEnd ℂ) (↑(↑M 0 0).re + ↑(↑M 0 0).im * I) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (starRingEnd ℂ) (↑(↑M 0 1).re + ↑(↑M 0 1).im * I) =
  ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re +
                ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).re * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im * I -
              ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).re * ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * I +
            ↑(↑(↑M 0 1).re + ↑(↑M 0 1).im * I).im * ↑(↑(↑M 1 1).re + ↑(↑M 1 1).im * I).im +
          ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im -
        ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).im * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re * I +
      ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).im * ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * I +
    ↑(↑(↑M 0 0).re + ↑(↑M 0 0).im * I).re * ↑(↑(↑M 1 0).re + ↑(↑M 1 0).im * I).re
    simp only [Fin.isValue, map_add, conj_ofReal, _root_.map_mul, conj_I, mul_neg, add_re,
      ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, add_zero, add_im,
      mul_im, zero_add]M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ (↑(↑M 1 0).re + ↑(↑M 1 0).im * I) * (↑(↑M 0 0).re + -(↑(↑M 0 0).im * I)) +
    (↑(↑M 1 1).re + ↑(↑M 1 1).im * I) * (↑(↑M 0 1).re + -(↑(↑M 0 1).im * I)) =
  ↑(↑M 0 1).re * ↑(↑M 1 1).re + ↑(↑M 0 1).re * ↑(↑M 1 1).im * I - ↑(↑M 1 1).re * ↑(↑M 0 1).im * I +
            ↑(↑M 0 1).im * ↑(↑M 1 1).im +
          ↑(↑M 0 0).im * ↑(↑M 1 0).im -
        ↑(↑M 0 0).im * ↑(↑M 1 0).re * I +
      ↑(↑M 1 0).im * ↑(↑M 0 0).re * I +
    ↑(↑M 0 0).re * ↑(↑M 1 0).re
    ring_nfM:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ -(↑(↑M 1 0).re * I * ↑(↑M 0 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).re + ↑(↑M 1 0).im * I * ↑(↑M 0 0).re -
            ↑(↑M 1 0).im * I ^ 2 * ↑(↑M 0 0).im -
          I * ↑(↑M 1 1).re * ↑(↑M 0 1).im +
        I * ↑(↑M 1 1).im * ↑(↑M 0 1).re -
      I ^ 2 * ↑(↑M 1 1).im * ↑(↑M 0 1).im +
    ↑(↑M 1 1).re * ↑(↑M 0 1).re =
  -(↑(↑M 1 0).re * I * ↑(↑M 0 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).re + ↑(↑M 1 0).im * I * ↑(↑M 0 0).re +
            ↑(↑M 1 0).im * ↑(↑M 0 0).im -
          I * ↑(↑M 1 1).re * ↑(↑M 0 1).im +
        I * ↑(↑M 1 1).im * ↑(↑M 0 1).re +
      ↑(↑M 1 1).re * ↑(↑M 0 1).re +
    ↑(↑M 1 1).im * ↑(↑M 0 1).im
    simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, one_mul, sub_neg_eq_add]M:SL(2, ℂ)x:Fin (Nat.succ 1)y:Fin 2⊢ -(↑(↑M 1 0).re * I * ↑(↑M 0 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).re + ↑(↑M 1 0).im * I * ↑(↑M 0 0).re +
            ↑(↑M 1 0).im * ↑(↑M 0 0).im -
          I * ↑(↑M 1 1).re * ↑(↑M 0 1).im +
        I * ↑(↑M 1 1).im * ↑(↑M 0 1).re +
      ↑(↑M 1 1).im * ↑(↑M 0 1).im +
    ↑(↑M 1 1).re * ↑(↑M 0 1).re =
  -(↑(↑M 1 0).re * I * ↑(↑M 0 0).im) + ↑(↑M 1 0).re * ↑(↑M 0 0).re + ↑(↑M 1 0).im * I * ↑(↑M 0 0).re +
            ↑(↑M 1 0).im * ↑(↑M 0 0).im -
          I * ↑(↑M 1 1).re * ↑(↑M 0 1).im +
        I * ↑(↑M 1 1).im * ↑(↑M 0 1).re +
      ↑(↑M 1 1).re * ↑(↑M 0 1).re +
    ↑(↑M 1 1).im * ↑(↑M 0 1).im
    ringAll goals completed! 🐙

The monoid homomorphisms from SL(2, ℂ) to matrices indexed by Fin 1 ⊕ Fin 3 formed by the action M A Mᴴ.


def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where
  toFun M := LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis' (toSelfAdjointMap M)
  map_one' := by⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap 1) = 1
    simp only [toSelfAdjointMap, SpecialLinearGroup.coe_one, one_mul, conjTranspose_one,
      mul_one, Subtype.coe_eta]⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis')
    { toFun := fun A => A, map_add' := ⋯, map_smul' := ⋯ } =
  1
    erw [LinearMap.toMatrix_one⊢ 1 = 1]All goals completed! 🐙
  map_mul' M N := byM:SL(2, ℂ)N:SL(2, ℂ)⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap (M * N)) =
  (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M) *
    (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap N)
    rw [← LinearMap.toMatrix_mulM:SL(2, ℂ)N:SL(2, ℂ)⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap (M * N)) =
  (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M * toSelfAdjointMap N)M:SL(2, ℂ)N:SL(2, ℂ)⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap (M * N)) =
  (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M * toSelfAdjointMap N)]M:SL(2, ℂ)N:SL(2, ℂ)⊢ (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap (M * N)) =
  (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M * toSelfAdjointMap N)
    apply congrArgM:SL(2, ℂ)N:SL(2, ℂ)⊢ toSelfAdjointMap (M * N) = toSelfAdjointMap M * toSelfAdjointMap N
    ext1 xM:SL(2, ℂ)N:SL(2, ℂ)x:↥(selfAdjoint ℂ²ˣ²)⊢ (toSelfAdjointMap (M * N)) x = (toSelfAdjointMap M * toSelfAdjointMap N) x
    erw [Module.End.mul_applyM:SL(2, ℂ)N:SL(2, ℂ)x:↥(selfAdjoint ℂ²ˣ²)⊢ (toSelfAdjointMap (M * N)) x = (toSelfAdjointMap M) ((toSelfAdjointMap N) x)]M:SL(2, ℂ)N:SL(2, ℂ)x:↥(selfAdjoint ℂ²ˣ²)⊢ (toSelfAdjointMap (M * N)) x = (toSelfAdjointMap M) ((toSelfAdjointMap N) x)
    simp only [toSelfAdjointMap_apply, SpecialLinearGroup.coe_mul, conjTranspose_mul,
      Subtype.mk.injEq]M:SL(2, ℂ)N:SL(2, ℂ)x:↥(selfAdjoint ℂ²ˣ²)⊢ ↑M * ↑N * ↑x * ((↑N)ᴴ * (↑M)ᴴ) = ↑M * (↑N * ↑x * (↑N)ᴴ) * (↑M)ᴴ
    ext1M:SL(2, ℂ)N:SL(2, ℂ)x:↥(selfAdjoint ℂ²ˣ²)i✝:Fin 2j✝:Fin 2⊢ (↑M * ↑N * ↑x * ((↑N)ᴴ * (↑M)ᴴ)) i✝ j✝ = (↑M * (↑N * ↑x * (↑N)ᴴ) * (↑M)ᴴ) i✝ j✝
    noncomm_ringAll goals completed! 🐙



lemma toMatrix_mem_lorentzGroup (M : SL(2, ℂ)) : toMatrix M ∈ LorentzGroup 3 := byM:SL(2, ℂ)⊢ toMatrix M ∈ LorentzGroup 3
  rw [LorentzGroup.mem_iff_normM:SL(2, ℂ)⊢ ∀ (w : ContrMod 3),
  contrContrContractField ((toMatrix M *ᵥ w) ⊗ₜ[ℝ] (toMatrix M *ᵥ w)) = contrContrContractField (w ⊗ₜ[ℝ] w)M:SL(2, ℂ)⊢ ∀ (w : ContrMod 3),
  contrContrContractField ((toMatrix M *ᵥ w) ⊗ₜ[ℝ] (toMatrix M *ᵥ w)) = contrContrContractField (w ⊗ₜ[ℝ] w)]M:SL(2, ℂ)⊢ ∀ (w : ContrMod 3),
  contrContrContractField ((toMatrix M *ᵥ w) ⊗ₜ[ℝ] (toMatrix M *ᵥ w)) = contrContrContractField (w ⊗ₜ[ℝ] w)
  intro xM:SL(2, ℂ)x:ContrMod 3⊢ contrContrContractField ((toMatrix M *ᵥ x) ⊗ₜ[ℝ] (toMatrix M *ᵥ x)) = contrContrContractField (x ⊗ₜ[ℝ] x)
  apply ofReal_injectiveM:SL(2, ℂ)x:ContrMod 3⊢ ↑(contrContrContractField ((toMatrix M *ᵥ x) ⊗ₜ[ℝ] (toMatrix M *ᵥ x))) = ↑(contrContrContractField (x ⊗ₜ[ℝ] x))
  rw [Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint,M:SL(2, ℂ)x:ContrMod 3⊢ (↑(ContrMod.toSelfAdjoint (toMatrix M *ᵥ x))).det = ↑(contrContrContractField (x ⊗ₜ[ℝ] x))All goals completed! 🐙 toMatrix_apply_contrMod,M:SL(2, ℂ)x:ContrMod 3⊢ (↑(ContrMod.toSelfAdjoint (ContrMod.toSelfAdjoint.symm ((toSelfAdjointMap M) (ContrMod.toSelfAdjoint x))))).det =
  ↑(contrContrContractField (x ⊗ₜ[ℝ] x))All goals completed! 🐙
    LinearEquiv.apply_symm_apply,M:SL(2, ℂ)x:ContrMod 3⊢ (↑((toSelfAdjointMap M) (ContrMod.toSelfAdjoint x))).det = ↑(contrContrContractField (x ⊗ₜ[ℝ] x))All goals completed! 🐙 toSelfAdjointMap_apply_det,M:SL(2, ℂ)x:ContrMod 3⊢ (↑(ContrMod.toSelfAdjoint x)).det = ↑(contrContrContractField (x ⊗ₜ[ℝ] x))All goals completed! 🐙
    Lorentz.contrContrContractField.same_eq_det_toSelfAdjointM:SL(2, ℂ)x:ContrMod 3⊢ (↑(ContrMod.toSelfAdjoint x)).det = (↑(ContrMod.toSelfAdjoint x)).detAll goals completed! 🐙]All goals completed! 🐙

The group homomorphism from SL(2, ℂ) to the Lorentz group 𝓛.

@[simps!]
def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
  toFun M := ⟨toMatrix M, toMatrix_mem_lorentzGroup M⟩
  map_one' := by⊢ ⟨toMatrix 1, ⋯⟩ = 1
    simp only [_root_.map_one]⊢ ⟨1, ⋯⟩ = 1
    rflAll goals completed! 🐙
  map_mul' M N := byM:SL(2, ℂ)N:SL(2, ℂ)⊢ ⟨toMatrix (M * N), ⋯⟩ = ⟨toMatrix M, ⋯⟩ * ⟨toMatrix N, ⋯⟩
    ext1M:SL(2, ℂ)N:SL(2, ℂ)⊢ ↑⟨toMatrix (M * N), ⋯⟩ = ↑(⟨toMatrix M, ⋯⟩ * ⟨toMatrix N, ⋯⟩)
    simp only [_root_.map_mul, lorentzGroupIsGroup_mul_coe]All goals completed! 🐙

              lemma toLorentzGroup_eq_pauliBasis' (M : SL(2, ℂ)) :
    toLorentzGroup M = LinearMap.toMatrix
    PauliMatrix.pauliBasis' PauliMatrix.pauliBasis' (toSelfAdjointMap M) := byM:SL(2, ℂ)⊢ ↑(toLorentzGroup M) = (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M)
  rflAll goals completed! 🐙

lemma toSelfAdjointMap_basis (i : Fin 1 ⊕ Fin 3) :
    toSelfAdjointMap M (PauliMatrix.pauliBasis' i) =
    ∑ j, (toLorentzGroup M).1 j i • PauliMatrix.pauliBasis' j := byM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) = ∑ j, ↑(toLorentzGroup M) j i • PauliMatrix.pauliBasis' j
  rw [toLorentzGroup_eq_pauliBasis'M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) =
  ∑ j,
    (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M) j i •
      PauliMatrix.pauliBasis' jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) =
  ∑ j,
    (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M) j i •
      PauliMatrix.pauliBasis' j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) =
  ∑ j,
    (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M) j i •
      PauliMatrix.pauliBasis' j
  simp only [LinearMap.toMatrix_apply]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) =
  ∑ x, (PauliMatrix.pauliBasis'.repr ((toSelfAdjointMap M) (PauliMatrix.pauliBasis' i))) x • PauliMatrix.pauliBasis' x
  nth_rewrite 1 [← (Basis.sum_repr PauliMatrix.pauliBasis'
    ((toSelfAdjointMap M) (PauliMatrix.pauliBasis' i)))]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ ∑ i_1,
    (PauliMatrix.pauliBasis'.repr ((toSelfAdjointMap M) (PauliMatrix.pauliBasis' i))) i_1 •
      PauliMatrix.pauliBasis' i_1 =
  ∑ x, (PauliMatrix.pauliBasis'.repr ((toSelfAdjointMap M) (PauliMatrix.pauliBasis' i))) x • PauliMatrix.pauliBasis' x
  rflAll goals completed! 🐙

lemma toSelfAdjointMap_pauliBasis (i : Fin 1 ⊕ Fin 3) :
    toSelfAdjointMap M (PauliMatrix.pauliBasis i) =
    ∑ j, (toLorentzGroup M⁻¹).1 i j • PauliMatrix.pauliBasis j := byM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis i) = ∑ j, ↑(toLorentzGroup M⁻¹) i j • PauliMatrix.pauliBasis j
  have h1 : (toLorentzGroup M⁻¹).1 = minkowskiMatrix.dual (toLorentzGroup M).1 := by
    simp [LorentzGroup.inv_eq_dual]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis i) = ∑ j, ↑(toLorentzGroup M⁻¹) i j • PauliMatrix.pauliBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis i) = ∑ j, ↑(toLorentzGroup M⁻¹) i j • PauliMatrix.pauliBasis j
  simp only [h1]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis i) =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x
  rw [PauliMatrix.pauliBasis_minkowskiMetric_pauliBasis',M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ (toSelfAdjointMap M) (minkowskiMatrix i i • PauliMatrix.pauliBasis' i) =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis xM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x _root_.map_smul,M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ minkowskiMatrix i i • (toSelfAdjointMap M) (PauliMatrix.pauliBasis' i) =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis xM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x toSelfAdjointMap_basis,M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ minkowskiMatrix i i • ∑ j, ↑(toLorentzGroup M) j i • PauliMatrix.pauliBasis' j =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis xM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x
    Finset.smul_sumM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis xM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ ∑ x, minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x =
  ∑ x, minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x
  apply congrArgM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)⊢ (fun x => minkowskiMatrix i i • ↑(toLorentzGroup M) x i • PauliMatrix.pauliBasis' x) = fun x =>
  minkowskiMatrix.dual (↑(toLorentzGroup M)) i x • PauliMatrix.pauliBasis x
  funext jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ minkowskiMatrix i i • ↑(toLorentzGroup M) j i • PauliMatrix.pauliBasis' j =
  minkowskiMatrix.dual (↑(toLorentzGroup M)) i j • PauliMatrix.pauliBasis j
  rw [smul_smul,M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  minkowskiMatrix.dual (↑(toLorentzGroup M)) i j • PauliMatrix.pauliBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j) • PauliMatrix.pauliBasis' j PauliMatrix.pauliBasis_minkowskiMetric_pauliBasis',M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  minkowskiMatrix.dual (↑(toLorentzGroup M)) i j • minkowskiMatrix j j • PauliMatrix.pauliBasis' jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j) • PauliMatrix.pauliBasis' j smul_smulM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j) • PauliMatrix.pauliBasis' jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j) • PauliMatrix.pauliBasis' j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) • PauliMatrix.pauliBasis' j =
  (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j) • PauliMatrix.pauliBasis' j
  apply congrFunM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ HSMul.hSMul (minkowskiMatrix i i * ↑(toLorentzGroup M) j i) =
  HSMul.hSMul (minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j)
  apply congrArgM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3h1:↑(toLorentzGroup M⁻¹) = minkowskiMatrix.dual ↑(toLorentzGroup M)j:Fin 1 ⊕ Fin 3⊢ minkowskiMatrix i i * ↑(toLorentzGroup M) j i = minkowskiMatrix.dual (↑(toLorentzGroup M)) i j * minkowskiMatrix j j
  exact Eq.symm (minkowskiMatrix.dual_apply_minkowskiMatrix ((toLorentzGroup M).1) i j)All goals completed! 🐙

The first column of the Lorentz matrix formed from an element of SL(2, ℂ).


lemma toLorentzGroup_fst_col (M : SL(2, ℂ)) :
    (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = fun μ =>
      match μ with
      | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)
      | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
        (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))
      | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
        - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))
      | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := byM:SL(2, ℂ)⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = fun μ =>
  match μ with
  | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  | Sum.inr 0 =>
    -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
  | Sum.inr 1 =>
    -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
  | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ =>
    match μ with
    | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)
    | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
      (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))
    | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))
    | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = fun μ =>
  match μ with
  | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  | Sum.inr 0 =>
    -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
  | Sum.inr 1 =>
    -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
  | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  change (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = kM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
  have h1 : toSelfAdjointMap M (PauliMatrix.pauliBasis' (Sum.inl 0)) =
      ∑ μ, k μ • PauliMatrix.pauliBasis' μ := byM:SL(2, ℂ)⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = fun μ =>
  match μ with
  | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  | Sum.inr 0 =>
    -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
  | Sum.inr 1 =>
    -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
  | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
    simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
      Finset.sum_singleton, Fin.sum_univ_three]M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ (toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) =
  k (Sum.inl 0) • PauliMatrix.pauliBasis' (Sum.inl 0) +
    (k (Sum.inr 0) • PauliMatrix.pauliBasis' (Sum.inr 0) + k (Sum.inr 1) • PauliMatrix.pauliBasis' (Sum.inr 1) +
      k (Sum.inr 2) • PauliMatrix.pauliBasis' (Sum.inr 2))M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
    rw [toSelfAdjointMap_apply_pauliBasis'_inlM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inl 0) +
        -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im +
              (↑M 0 0).re * (↑M 1 0).re) •
          PauliMatrix.pauliBasis' (Sum.inr 0) +
      (-(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re) •
        PauliMatrix.pauliBasis' (Sum.inr 1) +
    ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inr 2) =
  k (Sum.inl 0) • PauliMatrix.pauliBasis' (Sum.inl 0) +
    (k (Sum.inr 0) • PauliMatrix.pauliBasis' (Sum.inr 0) + k (Sum.inr 1) • PauliMatrix.pauliBasis' (Sum.inr 1) +
      k (Sum.inr 2) • PauliMatrix.pauliBasis' (Sum.inr 2))M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inl 0) +
        -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im +
              (↑M 0 0).re * (↑M 1 0).re) •
          PauliMatrix.pauliBasis' (Sum.inr 0) +
      (-(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re) •
        PauliMatrix.pauliBasis' (Sum.inr 1) +
    ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inr 2) =
  k (Sum.inl 0) • PauliMatrix.pauliBasis' (Sum.inl 0) +
    (k (Sum.inr 0) • PauliMatrix.pauliBasis' (Sum.inr 0) + k (Sum.inr 1) • PauliMatrix.pauliBasis' (Sum.inr 1) +
      k (Sum.inr 2) • PauliMatrix.pauliBasis' (Sum.inr 2))M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k]M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2⊢ ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inl 0) +
        -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im +
              (↑M 0 0).re * (↑M 1 0).re) •
          PauliMatrix.pauliBasis' (Sum.inr 0) +
      (-(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re) •
        PauliMatrix.pauliBasis' (Sum.inr 1) +
    ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (Sum.inr 2) =
  k (Sum.inl 0) • PauliMatrix.pauliBasis' (Sum.inl 0) +
    (k (Sum.inr 0) • PauliMatrix.pauliBasis' (Sum.inr 0) + k (Sum.inr 1) • PauliMatrix.pauliBasis' (Sum.inr 1) +
      k (Sum.inr 2) • PauliMatrix.pauliBasis' (Sum.inr 2))M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
    abelM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = kM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:(toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
  rw [toSelfAdjointMap_basisM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = kM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k] at h1M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μ⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
  have h1x := sub_eq_zero_of_eq h1M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j - ∑ μ, k μ • PauliMatrix.pauliBasis' μ = 0⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
  rw [← Finset.sum_sub_distribM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = kM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k] at h1xM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0⊢ (fun μ => ↑(toLorentzGroup M) μ (Sum.inl 0)) = k
  funext μM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0μ:Fin 1 ⊕ Fin 3⊢ ↑(toLorentzGroup M) μ (Sum.inl 0) = k μ
  refine sub_eq_zero.mp ?_M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0μ:Fin 1 ⊕ Fin 3⊢ ↑(toLorentzGroup M) μ (Sum.inl 0) - k μ = 0
  refine Fintype.linearIndependent_iff.mp PauliMatrix.pauliBasis'.linearIndependent
    (fun x => ((toLorentzGroup M).1 x (Sum.inl 0) - k x)) ?_ μM:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0μ:Fin 1 ⊕ Fin 3⊢ ∑ i, (↑(toLorentzGroup M) i (Sum.inl 0) - k i) • PauliMatrix.pauliBasis' i = 0
  simp only [sub_smul]M:SL(2, ℂ)k:Fin 1 ⊕ Fin 3 → ℝ := 
  fun μ =>
    match μ with
    | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
    | Sum.inr 0 =>
      -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re)
    | Sum.inr 1 =>
      -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re
    | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2h1:∑ j, ↑(toLorentzGroup M) j (Sum.inl 0) • PauliMatrix.pauliBasis' j = ∑ μ, k μ • PauliMatrix.pauliBasis' μh1x:∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0μ:Fin 1 ⊕ Fin 3⊢ ∑ x, (↑(toLorentzGroup M) x (Sum.inl 0) • PauliMatrix.pauliBasis' x - k x • PauliMatrix.pauliBasis' x) = 0
  exact h1xAll goals completed! 🐙

The first element of the image of SL(2, ℂ) in the Lorentz group.

lemma toLorentzGroup_inl_inl (M : SL(2, ℂ)) :
    (toLorentzGroup M).1 (Sum.inl 0) (Sum.inl 0) =
    ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := byM:SL(2, ℂ)⊢ ↑(toLorentzGroup M) (Sum.inl 0) (Sum.inl 0) = (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  exact congrFun (toLorentzGroup_fst_col M) (Sum.inl 0)All goals completed! 🐙

The image of SL(2, ℂ) in the Lorentz group is orthochronous.


lemma toLorentzGroup_isOrthochronous (M : SL(2, ℂ)) :
    LorentzGroup.IsOrthochronous (toLorentzGroup M) := byM:SL(2, ℂ)⊢ LorentzGroup.IsOrthochronous (toLorentzGroup M)
  rw [LorentzGroup.IsOrthochronous,M:SL(2, ℂ)⊢ 0 ≤ ↑(toLorentzGroup M) (Sum.inl 0) (Sum.inl 0)M:SL(2, ℂ)⊢ 0 ≤ (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2 toLorentzGroup_inl_inlM:SL(2, ℂ)⊢ 0 ≤ (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2M:SL(2, ℂ)⊢ 0 ≤ (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2]M:SL(2, ℂ)⊢ 0 ≤ (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2
  positivityAll goals completed! 🐙

Homomorphism to the restricted Lorentz group

The homomorphism toLorentzGroup restricts to a homomorphism to the restricted Lorentz group. In this section we will define this homomorphism.

The determinant of the image of SL(2, ℂ) in the Lorentz group is one.


lemma toLorentzGroup_det_one (M : SL(2, ℂ)) : det (toLorentzGroup M).val = 1 :=
  let U := M.val.schurTriangulationUnitary
  let N := M.val.schurTriangulation.val
  have h : M.val = U * N * star U := M.val.schur_triangulation
  haveI : Invertible U.val := ⟨star U.val, U.property.left, U.property.right⟩
  calc det (toLorentzGroup M).val
    _ = LinearMap.det (toSelfAdjointMap' M) := LinearMap.det_toMatrix ..
    _ = LinearMap.det (toSelfAdjointMap' (U * N * U.val⁻¹)) :=
      suffices star U = U.val⁻¹ byM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this✝:Invertible ↑Uthis:↑(star U) = (↑U)⁻¹⊢ LinearMap.det (toSelfAdjointMap' ↑M) = LinearMap.det (toSelfAdjointMap' (↑U * N * (↑U)⁻¹)) rw [h,M:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this✝:Invertible ↑Uthis:↑(star U) = (↑U)⁻¹⊢ LinearMap.det (toSelfAdjointMap' (↑U * N * ↑(star U))) = LinearMap.det (toSelfAdjointMap' (↑U * N * (↑U)⁻¹))All goals completed! 🐙 thisM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this✝:Invertible ↑Uthis:↑(star U) = (↑U)⁻¹⊢ LinearMap.det (toSelfAdjointMap' (↑U * N * (↑U)⁻¹)) = LinearMap.det (toSelfAdjointMap' (↑U * N * (↑U)⁻¹))All goals completed! 🐙]All goals completed! 🐙
      calc star U.val
        _ = star U.val * (U.val * U.val⁻¹) := byM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this:Invertible ↑U⊢ star ↑U = star ↑U * (↑U * (↑U)⁻¹) simpAll goals completed! 🐙
        _ = star U.val * U.val * U.val⁻¹ := byM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this:Invertible ↑U⊢ star ↑U * (↑U * (↑U)⁻¹) = star ↑U * ↑U * (↑U)⁻¹ noncomm_ringAll goals completed! 🐙
        _ = U.val⁻¹ := byM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this:Invertible ↑U⊢ star ↑U * ↑U * (↑U)⁻¹ = (↑U)⁻¹ simpAll goals completed! 🐙
    _ = LinearMap.det (toSelfAdjointMap' N) := toSelfAdjointMap_similar_det U N
    _ = 1 :=
      suffices N.det = 1 from toSelfAdjointMap_det_one' M.val.schurTriangulation.property this
      calc N.det
        _ = det ((U * star U).val * N) := byM:SL(2, ℂ)U:↥(unitaryGroup (Fin 2) ℂ) := (↑M).schurTriangulationUnitaryN:ℂ²ˣ² := ↑(↑M).schurTriangulationh:↑M = ↑U * N * ↑(star U)this:Invertible ↑U⊢ N.det = (↑(U * star U) * N).det simpAll goals completed! 🐙
        _ = det (U.val * N * star U.val) := det_mul_right_comm ..
        _ = M.val.det := congrArg det h.symm
        _ = 1 := M.property

The homomorphism from SL(2, ℂ) to the restricted Lorentz group.

@[simps!]
def toRestrictedLorentzGroup : SL(2, ℂ) →* LorentzGroup.restricted 3 :=
  toLorentzGroup.codRestrict (LorentzGroup.restricted 3)
    (fun M => And.intro (toLorentzGroup_det_one M) (toLorentzGroup_isOrthochronous M))