Conjugacy by eigenvalues in SL₂

DefinitionElements of \(\mathrm{SL}_2(F)\) with eigenvalues \(s\) and \(s^{-1}\)#✓fully proved

Let \(F\) be a field and let \(s \in F\). A matrix \(M \in \mathrm{SL}_2(F)\) has eigenvalues \(s\) and \(s^{-1}\) if its characteristic polynomial is \((X - s)(X - s^{-1})\).

def HasEigenvalues (M : Matrix.SpecialLinearGroup (Fin 2) F) (s : F) : Prop :=
  (↑M : Matrix (Fin 2) (Fin 2) F).charpoly =
    (Polynomial.X - Polynomial.C s) * (Polynomial.X - Polynomial.C s⁻¹)
Used by 3
Used byDiagonalizing elements of \(\mathrm{SL}_2(F)\) with distinct eigenvalues · Distinct eigenvalues give conjugacy to \(\operatorname{diag}(s, s^{-1})\) in \(\mathrm{SL}_2(F)\) · Matrices with the same distinct eigenvalues lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)

TheoremConjugacy to \(\operatorname{diag}(s, s^{-1})\) in terms of a conjugator#✓fully proved

Let \(F\) be a field, let \(s \in F\) with \(s \ne 0\), and let \(M \in \mathrm{SL}_2(F)\). Then \(M\) is conjugate in \(\mathrm{SL}_2(F)\) to the diagonal matrix \(\operatorname{diag}(s, s^{-1})\) if and only if there is \(P \in \mathrm{SL}_2(F)\) such that the matrix \(P M P^{-1}\) equals \(\operatorname{diag}(s, s^{-1})\).

theorem isConj_diag2_iff (M : Matrix.SpecialLinearGroup (Fin 2) F)
    (s : F) (hs0 : s ≠ 0) :
    IsConj M (Matrix.SpecialLinearGroup.diag2 s hs0) ↔
      ∃ P : Matrix.SpecialLinearGroup (Fin 2) F,
        (P * M * P⁻¹ : Matrix.SpecialLinearGroup (Fin 2) F).1 =
          Matrix.diagonal ![s, s⁻¹]
Used by 2
Used byDiagonalizing elements of \(\mathrm{SL}_2(F)\) with distinct eigenvalues · Distinct eigenvalues give conjugacy to \(\operatorname{diag}(s, s^{-1})\) in \(\mathrm{SL}_2(F)\)

TheoremConjugates of \(\operatorname{diag}(s, s^{-1})\) lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)#✓fully proved

Conjugates of \(\operatorname{diag}(s, s^{-1})\) lie in the same normal subgroups of \(\mathrm{SL}_2(F)\). Let \(F\) be a field, let \(N\) be a normal subgroup of \(\mathrm{SL}_2(F)\), and let \(s \in F\). Suppose \(N\) contains a matrix \(B\) for which some \(P \in \mathrm{SL}_2(F)\) makes the matrix \(P B P^{-1}\) equal to the diagonal matrix \(\operatorname{diag}(s, s^{-1})\). Then \(N\) contains every \(Q \in \mathrm{SL}_2(F)\) for which some \(P \in \mathrm{SL}_2(F)\) makes \(P Q P^{-1}\) equal to \(\operatorname{diag}(s, s^{-1})\).

The two matrices are conjugate to each other, via the diagonal matrix, and a normal subgroup is closed under conjugation.

theorem normal_subgroup_contains_all_conj_to_diag
    (N : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F))
    (hN : N.Normal) (s : F)
    (B : Matrix.SpecialLinearGroup (Fin 2) F) (hB : B ∈ N)
    (hBdiag : ∃ P : Matrix.SpecialLinearGroup (Fin 2) F,
      (P * B * P⁻¹ : Matrix.SpecialLinearGroup (Fin 2) F).1 =
        Matrix.diagonal ![s, s⁻¹])
    (Q : Matrix.SpecialLinearGroup (Fin 2) F)
    (hQdiag : ∃ P : Matrix.SpecialLinearGroup (Fin 2) F,
      (P * Q * P⁻¹ : Matrix.SpecialLinearGroup (Fin 2) F).1 =
        Matrix.diagonal ![s, s⁻¹]) :
    Q ∈ N
Used by 1
Used byMatrices with the same distinct eigenvalues lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)

TheoremDistinct eigenvalues give conjugacy to \(\operatorname{diag}(s, s^{-1})\) in \(\mathrm{SL}_2(F)\)#✓fully proved

Distinct eigenvalues give conjugacy to \(\operatorname{diag}(s, s^{-1})\) in \(\mathrm{SL}_2(F)\). Let \(F\) be a field and let \(s \in F\) with \(s \ne s^{-1}\) and \(s \ne 0\). If \(M \in \mathrm{SL}_2(F)\) has eigenvalues \(s\) and \(s^{-1}\), that is, characteristic polynomial \((X - s)(X - s^{-1})\), then \(M\) is conjugate in \(\mathrm{SL}_2(F)\) to the diagonal matrix \(\operatorname{diag}(s, s^{-1})\).

The proof builds the conjugating matrix from eigenvectors for \(s\) and \(s^{-1}\): distinct eigenvalues give linearly independent eigenvectors, so the matrix of eigenvectors has nonzero determinant, and rescaling its first column makes the determinant \(1\).

theorem eigenvalues_implies_isConj_diag2 (s : F) (hs : s ≠ s⁻¹)
    (M : Matrix.SpecialLinearGroup (Fin 2) F) (hM : HasEigenvalues M s)
    (hs0 : s ≠ 0) : IsConj M (Matrix.SpecialLinearGroup.diag2 s hs0)
Uses 2 · Used by 1
Statement usesElements of \(\mathrm{SL}_2(F)\) with eigenvalues \(s\) and \(s^{-1}\)
Proof usesConjugacy to \(\operatorname{diag}(s, s^{-1})\) in terms of a conjugator
Used byDiagonalizing elements of \(\mathrm{SL}_2(F)\) with distinct eigenvalues

TheoremDiagonalizing elements of \(\mathrm{SL}_2(F)\) with distinct eigenvalues#✓fully proved

Let \(F\) be a field, let \(s \in F\) with \(s \ne s^{-1}\), and let \(M \in \mathrm{SL}_2(F)\) have eigenvalues \(s\) and \(s^{-1}\), that is, characteristic polynomial \((X - s)(X - s^{-1})\). Then there is \(P \in \mathrm{SL}_2(F)\) such that the matrix \(P M P^{-1}\) equals the diagonal matrix \(\operatorname{diag}(s, s^{-1})\).

theorem eigenvalues_implies_conj_to_diag (s : F) (hs : s ≠ s⁻¹)
    (M : Matrix.SpecialLinearGroup (Fin 2) F) (hM : HasEigenvalues M s) :
    ∃ P : Matrix.SpecialLinearGroup (Fin 2) F,
      (P * M * P⁻¹ : Matrix.SpecialLinearGroup (Fin 2) F).1 =
        Matrix.diagonal ![s, s⁻¹]
Uses 3 · Used by 1
Statement usesElements of \(\mathrm{SL}_2(F)\) with eigenvalues \(s\) and \(s^{-1}\)
Proof usesDistinct eigenvalues give conjugacy to \(\operatorname{diag}(s, s^{-1})\) in \(\mathrm{SL}_2(F)\) · Conjugacy to \(\operatorname{diag}(s, s^{-1})\) in terms of a conjugator
Used byMatrices with the same distinct eigenvalues lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)

TheoremMatrices with the same distinct eigenvalues lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)#✓fully proved

Matrices with the same distinct eigenvalues lie in the same normal subgroups of \(\mathrm{SL}_2(F)\). Let \(F\) be a field, let \(N\) be a normal subgroup of \(\mathrm{SL}_2(F)\), and let \(s \in F\) with \(s \ne s^{-1}\). If \(N\) contains a matrix with eigenvalues \(s\) and \(s^{-1}\), then \(N\) contains every matrix in \(\mathrm{SL}_2(F)\) with eigenvalues \(s\) and \(s^{-1}\).

theorem normal_contains_all_with_eigenvalues
    (N : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F))
    (hN : N.Normal) (s : F) (hs : s ≠ s⁻¹)
    (B : Matrix.SpecialLinearGroup (Fin 2) F) (hB : B ∈ N)
    (hBeig : HasEigenvalues B s)
    (Q : Matrix.SpecialLinearGroup (Fin 2) F)
    (hQeig : HasEigenvalues Q s) :
    Q ∈ N
Uses 3
Statement usesElements of \(\mathrm{SL}_2(F)\) with eigenvalues \(s\) and \(s^{-1}\)
Proof usesDiagonalizing elements of \(\mathrm{SL}_2(F)\) with distinct eigenvalues · Conjugates of \(\operatorname{diag}(s, s^{-1})\) lie in the same normal subgroups of \(\mathrm{SL}_2(F)\)
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.