The special unitary group SU(2)

DefinitionDiagonal rotation#✓fully proved

For a real number \(\theta\), the diagonal rotation through \(\theta\) is the \(2 \times 2\) complex diagonal matrix \(\operatorname{diag}(e^{i\theta}, e^{-i\theta})\).

noncomputable def diagRotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ :=
  !![Complex.exp (↑θ * Complex.I), 0; 0, Complex.exp (-(↑θ * Complex.I))]

Used by 15

Used byDiagonal rotations are \(2\pi\)-periodic · When two diagonal rotations are equal · Diagonal rotations as diagonal matrices · Diagonal rotation through a multiple of \(2\pi\) · Diagonal rotations lie in \(\mathrm{SU}(2)\) · Diagonal rotation as a longitude element · Equal rotation matrices give equal longitude elements · The angle homomorphism into the longitude subgroup · Longitude elements multiply by adding angles · Longitude map · The longitude map on the class of an angle · The longitude map is injective · The longitude map is surjective · Longitude subgroup · Conjugate transpose of a diagonal rotation

TheoremDiagonal rotations as diagonal matrices#✓fully proved

For every real number \(\theta\), the diagonal rotation through \(\theta\) is the diagonal matrix whose diagonal entries are \(e^{i\theta}\) and \(e^{-i\theta}\), in that order.

theorem diagRotation_eq_diagonal (θ : ℝ) : diagRotation θ =
    Matrix.diagonal ![Complex.exp (↑θ * Complex.I),
      Complex.exp (-(↑θ * Complex.I))]

Uses 1 · Used by 6

Statement usesDiagonal rotation

Used byDiagonal rotations are \(2\pi\)-periodic · Diagonal rotation through a multiple of \(2\pi\) · Diagonal rotations lie in \(\mathrm{SU}(2)\) · Longitude elements multiply by adding angles · Longitude subgroup · Conjugate transpose of a diagonal rotation

TheoremConjugate transpose of a diagonal rotation#✓fully proved

For every real number \(\theta\), the conjugate transpose of the diagonal rotation through \(\theta\) is the diagonal rotation through \(-\theta\).

theorem star_diagRotation (θ : ℝ) : star (diagRotation θ) = diagRotation (-θ)

Uses 2 · Used by 2

Statement usesDiagonal rotation

Proof usesDiagonal rotations as diagonal matrices

Used byDiagonal rotations lie in \(\mathrm{SU}(2)\) · Longitude subgroup

TheoremDiagonal rotations lie in \(\mathrm{SU}(2)\)#✓fully proved

For every real number \(\theta\), the diagonal rotation through \(\theta\) is a \(2 \times 2\) complex matrix that is unitary and has determinant \(1\), that is, it lies in \(\mathrm{SU}(2)\).

theorem diagRotation_mem_specialUnitaryGroup (θ : ℝ) :
    diagRotation θ ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

Uses 3 · Used by 1

Statement usesDiagonal rotation

Proof usesDiagonal rotations as diagonal matrices · Conjugate transpose of a diagonal rotation

Used byDiagonal rotation as a longitude element

TheoremDiagonal rotation through a multiple of \(2\pi\)#✓fully proved

For every integer \(n\), the diagonal rotation through \(2\pi n\) is the \(2 \times 2\) identity matrix.

theorem diagRotation_int_mul_two_pi (n : ℤ) : diagRotation (n * (2 * Real.pi)) = 1

Uses 2 · Used by 3

Statement usesDiagonal rotation

Proof usesDiagonal rotations as diagonal matrices

Used byDiagonal rotations are \(2\pi\)-periodic · Longitude map · The longitude map on the class of an angle

TheoremDiagonal rotations are \(2\pi\)-periodic#✓fully proved

For every real number \(\theta\) and every integer \(n\), the diagonal rotation through \(\theta + 2\pi n\) equals the diagonal rotation through \(\theta\).

theorem diagRotation_add_int_mul_two_pi (θ : ℝ) (n : ℤ) :
    diagRotation (θ + n * (2 * Real.pi)) = diagRotation θ

Uses 3 · Used by 1

Statement usesDiagonal rotation

Proof usesDiagonal rotations as diagonal matrices · Diagonal rotation through a multiple of \(2\pi\)

Used byWhen two diagonal rotations are equal

DefinitionLongitude subgroup#✓fully proved

The longitude subgroup of \(\mathrm{SU}(2)\) is the subgroup of those elements of \(\mathrm{SU}(2)\) that are the diagonal rotation through \(\theta\) for some real number \(\theta\).

It is the longitude \(\mathrm{Long}_i\) at the equator point \(i\).

def longitudeSubgroup : Subgroup (Matrix.specialUnitaryGroup (Fin 2) ℂ) where
  carrier := {M | ∃ θ : ℝ, (M : Matrix (Fin 2) (Fin 2) ℂ) = diagRotation θ}
  mul_mem' := by
    intro a b ⟨θ₁, hθ₁⟩ ⟨θ₂, hθ₂⟩
    exact ⟨θ₁ + θ₂, by
      simp only [Submonoid.coe_mul, hθ₁, hθ₂, diagRotation_add]⟩
  one_mem' := ⟨0, diagRotation_zero.symm⟩
  inv_mem' := by
    intro a ⟨θ, hθ⟩
    refine ⟨-θ, ?_⟩
    have ha : ((a⁻¹ : Matrix.specialUnitaryGroup (Fin 2) ℂ) :
        Matrix (Fin 2) (Fin 2) ℂ) = star (a : Matrix (Fin 2) (Fin 2) ℂ) := by
      rw [← Matrix.star_eq_inv, Matrix.specialUnitaryGroup.coe_star]
    rw [ha, hθ, star_diagRotation]

Uses 3 · Used by 10

Statement usesDiagonal rotation · Diagonal rotations as diagonal matrices · Conjugate transpose of a diagonal rotation

Used byDiagonal rotation as a longitude element · Equal rotation matrices give equal longitude elements · The angle homomorphism into the longitude subgroup · Longitude elements multiply by adding angles · Longitude map · The longitude map on the class of an angle · The longitude map is bijective · The longitude map is injective · The longitude map is surjective · Isomorphism of the circle group with the longitude subgroup

DefinitionDiagonal rotation as a longitude element#✓fully proved

For a real number \(\theta\), the diagonal rotation through \(\theta\), regarded as an element of the longitude subgroup of \(\mathrm{SU}(2)\).

noncomputable def diagRotationToLongitude (θ : ℝ) : longitudeSubgroup :=
  ⟨⟨diagRotation θ, diagRotation_mem_specialUnitaryGroup θ⟩, ⟨θ, rfl⟩⟩

Uses 3 · Used by 7

Statement usesDiagonal rotation · Diagonal rotations lie in \(\mathrm{SU}(2)\) · Longitude subgroup

Used byEqual rotation matrices give equal longitude elements · The angle homomorphism into the longitude subgroup · Longitude elements multiply by adding angles · Longitude map · The longitude map on the class of an angle · The longitude map is injective · The longitude map is surjective

TheoremLongitude elements multiply by adding angles#✓fully proved

For real numbers \(a\) and \(b\), in the longitude subgroup the product of the diagonal rotations through \(a\) and through \(b\) is the diagonal rotation through \(a + b\).

theorem diagRotationToLongitude_mul (a b : ℝ) :
    diagRotationToLongitude a * diagRotationToLongitude b =
      diagRotationToLongitude (a + b)

Uses 4 · Used by 1

Statement usesDiagonal rotation as a longitude element · Longitude subgroup

Proof usesDiagonal rotation · Diagonal rotations as diagonal matrices

Used byThe angle homomorphism into the longitude subgroup

TheoremEqual rotation matrices give equal longitude elements#✓fully proved

For real numbers \(a\) and \(b\), if the diagonal rotations through \(a\) and through \(b\) are equal as matrices, then the elements of the longitude subgroup given by the diagonal rotations through \(a\) and through \(b\) are equal.

theorem diagRotationToLongitude_eq_of_diagRotation_eq {a b : ℝ}
    (h : diagRotation a = diagRotation b) :
    diagRotationToLongitude a = diagRotationToLongitude b

Uses 3

Statement usesDiagonal rotation · Diagonal rotation as a longitude element · Longitude subgroup

DefinitionThe angle homomorphism into the longitude subgroup#✓fully proved

The homomorphism from the additive group \(\mathbb{R}\) to the longitude subgroup, written additively, that sends a real number \(\theta\) to the diagonal rotation through \(\theta\), regarded as an element of the longitude subgroup.

noncomputable def diagRotationToLongitudeHom : ℝ →+ Additive longitudeSubgroup where
  toFun θ := Additive.ofMul (diagRotationToLongitude θ)
  map_zero' := by
    rw [show (0 : Additive longitudeSubgroup) = Additive.ofMul 1 from rfl]
    congr 1
    exact Subtype.ext (Subtype.ext diagRotation_zero)
  map_add' θ₁ θ₂ := by
    show Additive.ofMul (diagRotationToLongitude (θ₁ + θ₂)) =
      Additive.ofMul (diagRotationToLongitude θ₁ * diagRotationToLongitude θ₂)
    exact congrArg Additive.ofMul (diagRotationToLongitude_mul θ₁ θ₂).symm

Uses 4 · Used by 2

Statement usesDiagonal rotation · Diagonal rotation as a longitude element · Longitude elements multiply by adding angles · Longitude subgroup

Used byLongitude map · The longitude map on the class of an angle

DefinitionLongitude map#✓fully proved

The longitude map is the group homomorphism from the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, to the longitude subgroup of \(\mathrm{SU}(2)\) that sends the class of a real number \(\theta\) to the diagonal rotation through \(\theta\), that is, to \(\cos\theta \cdot I + \sin\theta \cdot \operatorname{diag}(i, -i) = \operatorname{diag}(e^{i\theta}, e^{-i\theta})\), where \(I\) is the \(2 \times 2\) identity matrix. It is well defined because diagonal rotations are \(2\pi\)-periodic.

MathlibExt.GroupTheory.SU2Longitude.longitudeMap · 15 lines

noncomputable def longitudeMap :
    Multiplicative (AddCircle (2 * Real.pi)) →* longitudeSubgroup :=
  AddMonoidHom.toMultiplicative
    (QuotientAddGroup.lift (AddSubgroup.zmultiples (2 * Real.pi))
      diagRotationToLongitudeHom (by
        intro a ha
        obtain ⟨n, hn⟩ := AddSubgroup.mem_zmultiples_iff.mp ha
        show Additive.ofMul (diagRotationToLongitude a) = 0
        rw [← hn]
        have hdiag : diagRotation (n • (2 * Real.pi)) = 1 := by
          rw [zsmul_eq_mul]
          exact diagRotation_int_mul_two_pi n
        rw [show (0 : Additive longitudeSubgroup) = Additive.ofMul 1 from rfl]
        congr 1
        exact Subtype.ext (Subtype.ext hdiag)))

Uses 5 · Used by 5

Statement usesDiagonal rotation · Diagonal rotation as a longitude element · The angle homomorphism into the longitude subgroup · Diagonal rotation through a multiple of \(2\pi\) · Longitude subgroup

Used byThe longitude map on the class of an angle · The longitude map is bijective · The longitude map is injective · The longitude map is surjective · Isomorphism of the circle group with the longitude subgroup

TheoremThe longitude map on the class of an angle#✓fully proved

For every real number \(\theta\), the longitude map sends the class of \(\theta\) in \(\mathbb{R}/2\pi\mathbb{Z}\) to the diagonal rotation through \(\theta\), regarded as an element of the longitude subgroup.

theorem longitudeMap_apply_ofAdd_mk (θ : ℝ) :
    longitudeMap (Multiplicative.ofAdd (↑θ : AddCircle (2 * Real.pi))) =
      diagRotationToLongitude θ

Uses 6 · Used by 2

Statement usesDiagonal rotation as a longitude element · Longitude map · Longitude subgroup

Proof usesDiagonal rotation · The angle homomorphism into the longitude subgroup · Diagonal rotation through a multiple of \(2\pi\)

Used byThe longitude map is injective · The longitude map is surjective

TheoremWhen two diagonal rotations are equal#✓fully proved

For real numbers \(a\) and \(b\), the diagonal rotations through \(a\) and through \(b\) are equal if and only if \(a = b + 2\pi n\) for some integer \(n\).

theorem diagRotation_eq_diagRotation_iff (a b : ℝ) :
    diagRotation a = diagRotation b ↔ ∃ n : ℤ, a = b + n * (2 * Real.pi)

Uses 2 · Used by 1

Statement usesDiagonal rotation

Proof usesDiagonal rotations are \(2\pi\)-periodic

Used byThe longitude map is injective

TheoremEvery point of \(\mathbb{R}/2\pi\mathbb{Z}\) comes from a real angle#✓fully proved

Every element \(x\) of the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, is the class of some real number \(a\).

theorem exists_ofAdd_mk_eq (x : Multiplicative (AddCircle (2 * Real.pi))) :
    ∃ a : ℝ, x = Multiplicative.ofAdd (↑a : AddCircle (2 * Real.pi))

Used by 1

Used byThe longitude map is injective

TheoremThe longitude map is injective#✓fully proved

The longitude map from the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, to the longitude subgroup of \(\mathrm{SU}(2)\) is injective.

The angle class is recovered from the diagonal rotation via the complex exponential.

theorem longitudeMap_injective : Function.Injective longitudeMap

Uses 7 · Used by 1

Statement usesLongitude map · Longitude subgroup

Proof usesDiagonal rotation · Diagonal rotation as a longitude element · When two diagonal rotations are equal · Every point of \(\mathbb{R}/2\pi\mathbb{Z}\) comes from a real angle · The longitude map on the class of an angle

Used byThe longitude map is bijective

TheoremThe longitude map is surjective#✓fully proved

The longitude map from the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, to the longitude subgroup of \(\mathrm{SU}(2)\) is surjective: every element of the longitude subgroup is the image of some class.

theorem longitudeMap_surjective : Function.Surjective longitudeMap

Uses 5 · Used by 1

Statement usesLongitude map · Longitude subgroup

Proof usesDiagonal rotation · Diagonal rotation as a longitude element · The longitude map on the class of an angle

Used byThe longitude map is bijective

TheoremThe longitude map is bijective#✓fully proved

The longitude map from the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, to the longitude subgroup of \(\mathrm{SU}(2)\) is bijective.

theorem longitudeMap_bijective : Function.Bijective longitudeMap

Uses 4 · Used by 1

Statement usesLongitude map · Longitude subgroup

Proof usesThe longitude map is injective · The longitude map is surjective

Used byIsomorphism of the circle group with the longitude subgroup

DefinitionIsomorphism of the circle group with the longitude subgroup#✓fully proved

The group isomorphism from the circle group \(\mathbb{R}/2\pi\mathbb{Z}\), written multiplicatively, onto the longitude subgroup of \(\mathrm{SU}(2)\) given by the longitude map, which sends the class of a real number \(\theta\) to the diagonal rotation through \(\theta\).

noncomputable def longitudeMulEquiv :
    Multiplicative (AddCircle (2 * Real.pi)) ≃* longitudeSubgroup :=
  MulEquiv.ofBijective longitudeMap longitudeMap_bijective

Uses 3

Statement usesLongitude map · The longitude map is bijective · Longitude subgroup

TheoremMatrix form of \(\mathrm{SU}(2)\)#✓fully proved

Let \(M\) be a complex \(2 \times 2\) matrix in the special unitary group \(\mathrm{SU}(2)\), that is, \(M\) is unitary with determinant \(1\). Then there are complex numbers \(a, b\) with \(|a|^2 + |b|^2 = 1\) such that the first row of \(M\) is \((a, b)\) and the second row of \(M\) is \((-\bar b, \bar a)\).

theorem exists_eq_of_mem_specialUnitaryGroup_fin_two
    (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : M ∈ specialUnitaryGroup (Fin 2) ℂ) :
    ∃ a b : ℂ, M = !![a, b; -starRingEnd ℂ b, starRingEnd ℂ a] ∧
      Complex.normSq a + Complex.normSq b = 1

Used by 5

Used byThe center of \(\mathrm{SU}(2)\) · Characterization of \(\mathrm{SU}(2)\) · The trace of an \(\mathrm{SU}(2)\) matrix has absolute value at most two · Diagonalization in \(\mathrm{SU}(2)\) up to conjugacy · The trace of an \(\mathrm{SU}(2)\) matrix is real

TheoremThe trace of an \(\mathrm{SU}(2)\) matrix is real#✓fully proved

For every complex \(2 \times 2\) matrix \(M\) in the special unitary group \(\mathrm{SU}(2)\), the imaginary part of the trace of \(M\) is \(0\).

theorem trace_im_eq_zero_of_mem_specialUnitaryGroup_fin_two
    (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : M ∈ specialUnitaryGroup (Fin 2) ℂ) :
    (Matrix.trace M).im = 0

Uses 1

Proof usesMatrix form of \(\mathrm{SU}(2)\)

TheoremThe trace of an \(\mathrm{SU}(2)\) matrix has absolute value at most two#✓fully proved

For every complex \(2 \times 2\) matrix \(M\) in the special unitary group \(\mathrm{SU}(2)\), the trace of \(M\) satisfies \(|\operatorname{tr} M| \le 2\).

theorem norm_trace_le_two_of_mem_specialUnitaryGroup_fin_two
    (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : M ∈ specialUnitaryGroup (Fin 2) ℂ) :
    ‖Matrix.trace M‖ ≤ 2

Uses 1

Proof usesMatrix form of \(\mathrm{SU}(2)\)

TheoremThe center of \(\mathrm{SU}(2)\)#✓fully proved

An element \(M\) of the special unitary group \(\mathrm{SU}(2)\) of complex \(2 \times 2\) matrices lies in the center of \(\mathrm{SU}(2)\) if and only if \(M\) is the identity matrix \(I\) or \(M = -I\).

theorem mem_center_specialUnitaryGroup_fin_two_iff
    (M : specialUnitaryGroup (Fin 2) ℂ) :
    M ∈ Subgroup.center (specialUnitaryGroup (Fin 2) ℂ) ↔
      (M : Matrix (Fin 2) (Fin 2) ℂ) = 1 ∨ (M : Matrix (Fin 2) (Fin 2) ℂ) = -1

Uses 1 · Used by 1

Proof usesMatrix form of \(\mathrm{SU}(2)\)

Used byThe center of \(\mathrm{SU}(2)\) is proper

TheoremCharacterization of \(\mathrm{SU}(2)\)#✓fully proved

A complex \(2 \times 2\) matrix \(M\) lies in the special unitary group \(\mathrm{SU}(2)\), that is, \(M\) is unitary with determinant \(1\), if and only if there are complex numbers \(\alpha, \beta\) with \(|\alpha|^2 + |\beta|^2 = 1\) such that the first row of \(M\) is \((\alpha, \beta)\) and the second row is \((-\bar\beta, \bar\alpha)\).

theorem mem_specialUnitaryGroup_fin_two_iff {M : Matrix (Fin 2) (Fin 2) ℂ} :
    M ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ ↔
      ∃ α β : ℂ, M = !![α, β; -starRingEnd ℂ β, starRingEnd ℂ α] ∧
        Complex.normSq α + Complex.normSq β = 1

Uses 1

Proof usesMatrix form of \(\mathrm{SU}(2)\)

TheoremThe matrix \(\operatorname{diag}(i, -i)\) is special unitary#✓fully proved

The complex diagonal matrix \(\operatorname{diag}(i, -i)\), where \(i\) is the imaginary unit, lies in the special unitary group \(\mathrm{SU}(2)\) of complex \(2 \times 2\) matrices.

theorem diag_I_mem :
    !![Complex.I, (0 : ℂ); 0, -Complex.I] ∈
      Matrix.specialUnitaryGroup (Fin 2) ℂ

Used by 1

Used byThe center of \(\mathrm{SU}(2)\) is proper

TheoremThe matrix with rows \((0, 1)\) and \((-1, 0)\) is special unitary#✓fully proved

The complex \(2 \times 2\) matrix with rows \((0, 1)\) and \((-1, 0)\) lies in the special unitary group \(\mathrm{SU}(2)\) of complex \(2 \times 2\) matrices.

theorem antidiag_mem :
    !![(0 : ℂ), 1; -1, 0] ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

Used by 1

Used byDiagonal elements of \(\mathrm{SU}(2)\) with equal trace are conjugate

TheoremThe center of \(\mathrm{SU}(2)\) is proper#✓fully proved

The center of the special unitary group \(\mathrm{SU}(2)\) of complex \(2 \times 2\) matrices is not all of \(\mathrm{SU}(2)\).

The matrix \(\operatorname{diag}(i, -i)\), where \(i\) is the imaginary unit, lies in \(\mathrm{SU}(2)\) but is not central.

theorem su2_center_ne_top :
    Subgroup.center ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ) ≠ ⊤

Uses 2

Proof usesThe center of \(\mathrm{SU}(2)\) · The matrix \(\operatorname{diag}(i, -i)\) is special unitary

TheoremDiagonalization in \(\mathrm{SU}(2)\) up to conjugacy#✓fully proved

Every element of \(\mathrm{SU}(2)\) is conjugate in \(\mathrm{SU}(2)\) to an element of \(\mathrm{SU}(2)\) that is the diagonal matrix \(\operatorname{diag}(z, \bar z)\) for some complex number \(z\) with \(z \bar z = 1\).

theorem su2_conj_to_diag (A : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) :
    ∃ (D : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)),
      (∃ z : ℂ, z * starRingEnd ℂ z = 1 ∧
        (D : Matrix (Fin 2) (Fin 2) ℂ) =
          !![z, (0 : ℂ); 0, starRingEnd ℂ z]) ∧ IsConj A D

Uses 1 · Used by 1

Proof usesMatrix form of \(\mathrm{SU}(2)\)

Used byConjugacy in SU₂ is determined by the trace

TheoremTrace is invariant under conjugation in \(\mathrm{SU}(2)\)#✓fully proved

For all \(P\) and \(A\) in \(\mathrm{SU}(2)\), the trace of \(P A P^{-1}\) equals the trace of \(A\).

theorem su2_trace_conj_inv (P A : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) :
    Matrix.trace ((P * A * P⁻¹ : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) :
      Matrix (Fin 2) (Fin 2) ℂ) = Matrix.trace (A : Matrix (Fin 2) (Fin 2) ℂ)

Used by 1

Used byConjugacy in SU₂ is determined by the trace

TheoremDiagonal elements of \(\mathrm{SU}(2)\) with equal trace are conjugate#✓fully proved

Let \(z_1, z_2\) be complex numbers with \(z_1 \bar z_1 = 1\) and \(z_2 \bar z_2 = 1\), and let \(D_1, D_2\) be elements of \(\mathrm{SU}(2)\) equal to the diagonal matrices \(\operatorname{diag}(z_1, \bar z_1)\) and \(\operatorname{diag}(z_2, \bar z_2)\). If \(D_1\) and \(D_2\) have the same trace, then they are conjugate in \(\mathrm{SU}(2)\).

In the proof, either \(z_1 = z_2\), or \(z_1 = \bar z_2\) and conjugation by the anti-diagonal matrix with rows \((0, 1)\) and \((-1, 0)\) swaps the diagonal entries.

theorem su2_diag_conj_of_trace (D₁ D₂ : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ))
    (z₁ z₂ : ℂ) (hz₁ : z₁ * starRingEnd ℂ z₁ = 1)
    (hz₂ : z₂ * starRingEnd ℂ z₂ = 1)
    (hD₁ : (D₁ : Matrix (Fin 2) (Fin 2) ℂ) =
      !![z₁, (0 : ℂ); 0, starRingEnd ℂ z₁])
    (hD₂ : (D₂ : Matrix (Fin 2) (Fin 2) ℂ) =
      !![z₂, (0 : ℂ); 0, starRingEnd ℂ z₂])
    (htrace : Matrix.trace (D₁ : Matrix (Fin 2) (Fin 2) ℂ) =
      Matrix.trace (D₂ : Matrix (Fin 2) (Fin 2) ℂ)) :
    IsConj D₁ D₂

Uses 1 · Used by 1

Proof usesThe matrix with rows \((0, 1)\) and \((-1, 0)\) is special unitary

Used byConjugacy in SU₂ is determined by the trace

TheoremConjugacy in SU₂ is determined by the trace#✓fully proved

Two elements of SU₂ with the same trace are conjugate in SU₂.

theorem su2_conj_of_trace_eq (A B : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ))
    (h : Matrix.trace (A : Matrix (Fin 2) (Fin 2) ℂ) =
      Matrix.trace (B : Matrix (Fin 2) (Fin 2) ℂ)) :
    IsConj A B

Uses 3

Proof usesDiagonalization in \(\mathrm{SU}(2)\) up to conjugacy · Diagonal elements of \(\mathrm{SU}(2)\) with equal trace are conjugate · Trace is invariant under conjugation in \(\mathrm{SU}(2)\)

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.