Comparing the type-A standard carrier with special linear matrices

Over a field, the matrix points of the full-weight type-A_r carrier are precisely the determinant-one matrices. This file packages that equality as a multiplicative equivalence with SL_{r+1} and proves that it respects the structures used by the finite groups of Lie type: the numbered root subgroups, entrywise Frobenius, and signed reverse inverse transpose.

The equivalence is deliberately the identity on underlying matrices. Consequently the comparison does not merely identify two abstract groups: it identifies their standard representations and their chosen type-A pinning.

Main declarations

• TauCeti.SlStd.specialLinearMulEquiv: the carrier-point equivalence with SL_{r+1}.
• TauCeti.SlStd.specialLinearMulEquiv_rootSubgroupPoints: compatibility with the numbered root subgroups.
• TauCeti.SlStd.specialLinearMulEquiv_frobenius: compatibility with entrywise Frobenius.
• TauCeti.SlStd.specialLinearMulEquiv_graphAutomorphismPoints: compatibility with the pinned type-A graph automorphism.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• R. Steinberg, Lectures on Chevalley Groups, §§3--4.

noncomputable def TauCeti.SlStd.specialLinearMulEquiv (r : ℕ) {K : Type u} [Field K] : ↥(points r K) ≃* Matrix.SpecialLinearGroup (Fin (r + 1)) K

The full-weight type-A_r carrier points over a field are multiplicatively equivalent to SL_{r+1}. Both directions preserve the underlying matrix.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.SlStd.toGL_specialLinearMulEquiv (r : ℕ) {K : Type u} [Field K] (g : ↥(points r K)) : Matrix.SpecialLinearGroup.toGL ((specialLinearMulEquiv r) g) = ↑g

Applying the carrier equivalence and then including into GL leaves a carrier point unchanged.

@[simp]

theorem TauCeti.SlStd.specialLinearMulEquiv_symm_coe (r : ℕ) {K : Type u} [Field K] (g : Matrix.SpecialLinearGroup (Fin (r + 1)) K) : ↑((specialLinearMulEquiv r).symm g) = Matrix.SpecialLinearGroup.toGL g

The inverse carrier equivalence preserves the underlying general-linear matrix.

@[simp]

theorem TauCeti.SlStd.specialLinearMulEquiv_rootSubgroupPoints (r : ℕ) {K : Type u} [Field K] (i : Fin r ⊕ Fin r) (a : Multiplicative K) : (specialLinearMulEquiv r) ((rootSubgroupPoints r i K) a) = Matrix.SpecialLinearGroup.transvection ⋯ (Multiplicative.toAdd a)

The carrier equivalence identifies a numbered root subgroup with the corresponding determinant-one transvection.

@[simp]

theorem TauCeti.SlStd.specialLinearMulEquiv_frobenius (r : ℕ) {K : Type u} [Field K] (p k : ℕ) [ExpChar K p] (g : ↥(points r K)) : (specialLinearMulEquiv r) ((frobenius r p k K) g) = (Matrix.SpecialLinearGroup.map (iterateFrobenius K p k)) ((specialLinearMulEquiv r) g)

The carrier equivalence intertwines the carrier Frobenius with entrywise Frobenius on special linear matrices.

@[simp]

theorem TauCeti.SlStd.specialLinearMulEquiv_graphAutomorphismPoints (r : ℕ) {F : Type} [Field F] (g : ↥(points r F)) : (specialLinearMulEquiv r) ((graphAutomorphismPoints r F) g) = (Matrix.SpecialLinearGroup.typeAGraphAutomorphism r F) ((specialLinearMulEquiv r) g)

The carrier equivalence intertwines the carrier graph automorphism with signed reverse inverse transpose on special linear matrices.