The type-A carrier in the standard special linear model

The type-A families are constructed on the explicit full-weight carrier. Their pinned reference group is the group of algebraic-closure-valued points of the special linear group scheme over ℤ. This file records the comparison together with all of the pinned data used in the construction.

For both A_r(q) and ²A_r(q), carrierEquivSpecialLinear is the identity on underlying matrices. It sends each positive simple-root subgroup to its elementary transvection and intertwines the carrier Frobenius with entrywise Frobenius. On the twisted family it also intertwines the carrier graph automorphism with signed reverse inverse transpose. Thus the carrier Steinberg map agrees with the independently defined pinned scheme-point composite.

Main declarations

• TauCeti.TypeALieIndex.StandardGroup: the standard SL_{r+1} matrix group over the index's algebraic closure.
• TauCeti.TypeALieIndex.PinnedGroup and TauCeti.TypeALieIndex.pinnedEquivSpecialLinear: the algebraic-closure-valued points of the pinned SL_{r+1}/ℤ group scheme and their canonical matrix realization.
• TauCeti.TypeALieIndex.carrierEquivSpecialLinear: the equivalence from the explicit carrier.
• TauCeti.TypeALieIndex.specialLinearFrobenius, TauCeti.TypeALieIndex.specialLinearGraphAut, and TauCeti.TypeALieIndex.specialLinearSteinberg: the standard matrix maps.
• TauCeti.TypeALieIndex.specialLinearGraphAut_ofA and TauCeti.TypeALieIndex.specialLinearGraphAut_ofTwistedA: the graph-factor branch equations.
• TauCeti.TypeALieIndex.pinnedSimpleRootSubgroup, TauCeti.TypeALieIndex.pinnedFrobenius, TauCeti.TypeALieIndex.pinnedGraphAut, and TauCeti.TypeALieIndex.pinnedSteinberg: the pinning and Steinberg data on the pinned scheme points.
• TauCeti.TypeALieIndex.carrierEquivSpecialLinear_simpleRootSubgroup: agreement of the pinning.
• TauCeti.TypeALieIndex.carrierEquivSpecialLinear_steinberg: agreement of the Steinberg maps.
• TauCeti.TypeALieIndex.carrierEquivPinned, TauCeti.TypeALieIndex.carrierEquivPinned_simpleRootSubgroup, and TauCeti.TypeALieIndex.carrierEquivPinned_steinberg: the corresponding comparison with the pinned scheme points.

References

• R. W. Carter, Simple Groups of Lie Type, Chapters 2 and 14.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

@[reducible, inline]

noncomputable abbrev TauCeti.TypeALieIndex.StandardGroup (d : TypeALieIndex) : Type

The standard special linear matrix group corresponding to a validated type-A index.

Equations

• d.StandardGroup = Matrix.SpecialLinearGroup (Fin ((↑d).rank + 1)) (↑d).Closure

@[reducible, inline]

noncomputable abbrev TauCeti.TypeALieIndex.PinnedGroup (d : TypeALieIndex) : Type

The algebraic-closure-valued points of the pinned special linear group scheme over ℤ.

Equations

• d.PinnedGroup = ((AlgebraicGeometry.Spec ↧(↑d).Closure).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (TauCeti.SpecialLinear.groupScheme ℤ ((↑d).rank + 1)).X)

noncomputable def TauCeti.TypeALieIndex.pinnedEquivSpecialLinear (d : TypeALieIndex) : d.PinnedGroup ≃* d.StandardGroup

The canonical matrix realization of the pinned special linear scheme points.

Equations

• d.pinnedEquivSpecialLinear = TauCeti.SpecialLinear.schemePointsMulEquiv ((↑d).rank + 1) (↑d).Closure

noncomputable def TauCeti.TypeALieIndex.carrierEquivSpecialLinear (d : TypeALieIndex) : d.AmbientGroup ≃* d.StandardGroup

The explicit type-A carrier is equivalent to the standard special linear matrix group. The equivalence preserves the underlying matrix.

Equations

• d.carrierEquivSpecialLinear = TauCeti.SlStd.specialLinearMulEquiv (↑d).rank

noncomputable def TauCeti.TypeALieIndex.carrierEquivPinned (d : TypeALieIndex) : d.AmbientGroup ≃* d.PinnedGroup

The explicit type-A carrier is equivalent to the points of the pinned SL_{r+1}/ℤ group scheme.

Equations

• d.carrierEquivPinned = d.carrierEquivSpecialLinear.trans d.pinnedEquivSpecialLinear.symm

noncomputable def TauCeti.TypeALieIndex.specialLinearFrobenius (d : TypeALieIndex) : d.StandardGroup →* d.StandardGroup

Entrywise q-power Frobenius on the standard special linear matrix group.

Equations

• d.specialLinearFrobenius = Matrix.SpecialLinearGroup.map (iterateFrobenius (↑d).Closure (↑d).characteristic (↑d).fieldExponent)

noncomputable def TauCeti.TypeALieIndex.specialLinearGraphAut (d : TypeALieIndex) : MulAut d.StandardGroup

The graph factor on the standard special linear matrix group: the identity for A_r(q) and signed reverse inverse transpose for ²A_r(q).

Equations

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

theorem TauCeti.TypeALieIndex.specialLinearGraphAut_ofA (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.A rank q).Valid) : (ofA rank q hvalid).specialLinearGraphAut = 1

On A_r(q), the standard special-linear graph factor is trivial.

theorem TauCeti.TypeALieIndex.specialLinearGraphAut_ofTwistedA (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.twistedA rank q).Valid) : (ofTwistedA rank q hvalid).specialLinearGraphAut = Matrix.SpecialLinearGroup.typeAGraphAutomorphism (↑(ofTwistedA rank q hvalid)).rank (↑(ofTwistedA rank q hvalid)).Closure

On ²A_r(q), the standard special-linear graph factor is signed reverse inverse transpose.

noncomputable def TauCeti.TypeALieIndex.specialLinearSteinberg (d : TypeALieIndex) : d.StandardGroup →* d.StandardGroup

The standard matrix Steinberg map: the graph factor composed with entrywise q-power Frobenius.

Equations

• d.specialLinearSteinberg = (MulEquiv.toMonoidHom d.specialLinearGraphAut).comp d.specialLinearFrobenius

noncomputable def TauCeti.TypeALieIndex.pinnedSimpleRootSubgroup (d : TypeALieIndex) (i : Fin (↑d).rank) : Multiplicative (↑d).Closure →* d.PinnedGroup

The positive simple-root subgroup of the pinned special linear group scheme.

Equations

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

noncomputable def TauCeti.TypeALieIndex.pinnedFrobenius (d : TypeALieIndex) : d.PinnedGroup →* d.PinnedGroup

Entrywise q-power Frobenius on the pinned special linear scheme points. This is defined from the canonical matrix realization, independently of the explicit carrier.

Equations

• d.pinnedFrobenius = d.pinnedEquivSpecialLinear.symm.toMonoidHom.comp (d.specialLinearFrobenius.comp d.pinnedEquivSpecialLinear.toMonoidHom)

noncomputable def TauCeti.TypeALieIndex.pinnedGraphAut (d : TypeALieIndex) : MulAut d.PinnedGroup

The graph factor on the pinned special linear scheme points, defined through their canonical matrix realization.

Equations

• d.pinnedGraphAut = (d.pinnedEquivSpecialLinear.trans d.specialLinearGraphAut).trans d.pinnedEquivSpecialLinear.symm

noncomputable def TauCeti.TypeALieIndex.pinnedSteinberg (d : TypeALieIndex) : d.PinnedGroup →* d.PinnedGroup

The independently defined Steinberg map on the pinned special linear scheme points. It is the pinned graph factor composed with entrywise Frobenius.

Equations

• d.pinnedSteinberg = (MulEquiv.toMonoidHom d.pinnedGraphAut).comp d.pinnedFrobenius

@[simp]

theorem TauCeti.TypeALieIndex.pinnedEquivSpecialLinear_pinnedSimpleRootSubgroup (d : TypeALieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.pinnedEquivSpecialLinear ((d.pinnedSimpleRootSubgroup i) u) = Matrix.SpecialLinearGroup.transvection ⋯ (Multiplicative.toAdd u)

Under the canonical matrix realization, a pinned simple-root element is its elementary transvection.

@[simp]

theorem TauCeti.TypeALieIndex.pinnedEquivSpecialLinear_pinnedFrobenius (d : TypeALieIndex) (g : d.PinnedGroup) : d.pinnedEquivSpecialLinear (d.pinnedFrobenius g) = d.specialLinearFrobenius (d.pinnedEquivSpecialLinear g)

The canonical matrix realization intertwines pinned and matrix Frobenius.

@[simp]

theorem TauCeti.TypeALieIndex.pinnedEquivSpecialLinear_pinnedGraphAut (d : TypeALieIndex) (g : d.PinnedGroup) : d.pinnedEquivSpecialLinear (d.pinnedGraphAut g) = d.specialLinearGraphAut (d.pinnedEquivSpecialLinear g)

The canonical matrix realization intertwines the pinned and matrix graph factors.

@[simp]

theorem TauCeti.TypeALieIndex.pinnedEquivSpecialLinear_pinnedSteinberg (d : TypeALieIndex) (g : d.PinnedGroup) : d.pinnedEquivSpecialLinear (d.pinnedSteinberg g) = d.specialLinearSteinberg (d.pinnedEquivSpecialLinear g)

The canonical matrix realization intertwines the pinned and matrix Steinberg maps.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivSpecialLinear_simpleRootSubgroup (d : TypeALieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.carrierEquivSpecialLinear ((d.simpleRootSubgroup i) u) = Matrix.SpecialLinearGroup.transvection ⋯ (Multiplicative.toAdd u)

The carrier equivalence identifies each positive simple-root subgroup with its elementary transvection in the standard special linear group.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivPinned_simpleRootSubgroup (d : TypeALieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.carrierEquivPinned ((d.simpleRootSubgroup i) u) = (d.pinnedSimpleRootSubgroup i) u

The carrier-to-pinned equivalence matches the positive simple-root subgroups.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivSpecialLinear_frobenius (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivSpecialLinear (d.frobenius g) = d.specialLinearFrobenius (d.carrierEquivSpecialLinear g)

The carrier equivalence intertwines the two entrywise Frobenius maps.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivPinned_frobenius (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivPinned (d.frobenius g) = d.pinnedFrobenius (d.carrierEquivPinned g)

The carrier-to-pinned equivalence intertwines the Frobenius factors.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivSpecialLinear_graphAut (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivSpecialLinear (d.graphAut g) = d.specialLinearGraphAut (d.carrierEquivSpecialLinear g)

The carrier equivalence intertwines the two graph factors. This is trivial on A_r(q) and compares the two signed reverse-inverse-transpose maps on ²A_r(q).

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivPinned_graphAut (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivPinned (d.graphAut g) = d.pinnedGraphAut (d.carrierEquivPinned g)

The carrier-to-pinned equivalence intertwines the graph factors.

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivSpecialLinear_steinberg (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivSpecialLinear (d.steinberg g) = d.specialLinearSteinberg (d.carrierEquivSpecialLinear g)

The carrier Steinberg map agrees with the standard matrix Steinberg map. This covers entrywise Frobenius on A_r(q) and signed reverse inverse transpose after Frobenius on ²A_r(q).

@[simp]

theorem TauCeti.TypeALieIndex.carrierEquivPinned_steinberg (d : TypeALieIndex) (g : d.AmbientGroup) : d.carrierEquivPinned (d.steinberg g) = d.pinnedSteinberg (d.carrierEquivPinned g)

The explicit carrier Steinberg map agrees with the independently defined Steinberg map on the pinned special linear scheme points.