Frobenius-fixed points of the full-weight type-D spin carrier

For 4 ≤ n, TauCeti.TypeDSpinCarrier.frobenius n hn p k A is the p ^ k-power Frobenius endomorphism of the full-weight type-Dₙ spin carrier over a commutative ring A of exponential characteristic p. This file identifies its fixed-point group with the carrier's points over the Frobenius-fixed subring:

G(A^F) ≃* G(A)^F.

The underlying map applies the inclusion A^F → A to every matrix entry. Its inverse reads the entries of a fixed point in A^F. Consequently the fixed-point group is finite whenever A^F is finite; in particular this holds over a field of characteristic p for every nonzero Frobenius exponent.

Main declarations

• TauCeti.TypeDSpinCarrier.pointsMulEquivFixedSubgroupFrobenius: the fixed-point group equivalence.
• TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map: the forward map is the functorial map on carrier points induced by A^F → A.
• TauCeti.TypeDSpinCarrier.map_pointsMulEquivFixedSubgroupFrobenius_symm_apply: the inverse map recovers a fixed point after applying that inclusion.
• TauCeti.TypeDSpinCarrier.finite_fixedSubgroup_frobenius_of_charP: the fixed-point group over a field of characteristic p is finite for every nonzero exponent.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

The statement and interface parallel the fixed-point descriptions for the full-weight type-A and type-C carriers.

The fixed points as points over the fixed subring

noncomputable def TauCeti.TypeDSpinCarrier.pointsMulEquivFixedSubgroupFrobenius (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : ↥(points n hn ↥(frobeniusFixedSubring A p k)) ≃* ↥(fixedSubgroup (frobenius n hn p k A))

The Frobenius-fixed points of the full-weight type-Dₙ spin carrier are its points over the Frobenius-fixed subring. For p prime, 0 < k, and A an algebraic closure of ZMod p, this is the group isomorphism G(𝔽_(p^k)) ≃* G(A)^F.

Equations

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

theorem TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n hn ↥(frobeniusFixedSubring A p k))) : ↑↑((pointsMulEquivFixedSubgroupFrobenius n hn p k A) g) = (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑g

The fixed-point equivalence includes the matrix entries of a point over the Frobenius-fixed subring into the value ring.

theorem TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius_apply (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n hn ↥(frobeniusFixedSubring A p k))) (r c : Fin (dimension n)) : ↑↑↑((pointsMulEquivFixedSubgroupFrobenius n hn p k A) g) r c = ↑(↑↑g r c)

Entrywise, the fixed-point equivalence applies the inclusion of the Frobenius-fixed subring.

@[simp]

theorem TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n hn ↥(frobeniusFixedSubring A p k))) : ↑((pointsMulEquivFixedSubgroupFrobenius n hn p k A) g) = ((pointsPresentation n hn ↥(frobeniusFixedSubring A p k)).map (pointsPresentation n hn A) (frobeniusFixedSubring A p k).subtype) g

The fixed-point equivalence is the functorial point map along the inclusion of the Frobenius-fixed subring.

@[simp]

theorem TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n hn p k A))) : (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑((pointsMulEquivFixedSubgroupFrobenius n hn p k A).symm x) = ↑↑x

Including the matrix underlying the inverse image of a Frobenius-fixed point returns the original matrix.

@[simp]

theorem TauCeti.TypeDSpinCarrier.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply_apply (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n hn p k A))) (r c : Fin (dimension n)) : ↑(↑↑((pointsMulEquivFixedSubgroupFrobenius n hn p k A).symm x) r c) = ↑↑↑x r c

Entrywise, the inverse equivalence reads a Frobenius-fixed matrix over the fixed subring without changing its entries.

@[simp]

theorem TauCeti.TypeDSpinCarrier.map_pointsMulEquivFixedSubgroupFrobenius_symm_apply (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n hn p k A))) : ((pointsPresentation n hn ↥(frobeniusFixedSubring A p k)).map (pointsPresentation n hn A) (frobeniusFixedSubring A p k).subtype) ((pointsMulEquivFixedSubgroupFrobenius n hn p k A).symm x) = ↑x

The inverse equivalence, followed by the functorial point map from the fixed subring, returns the Frobenius-fixed carrier point.

Finiteness

theorem TauCeti.TypeDSpinCarrier.finite_fixedSubgroup_frobenius (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] [Finite ↥(frobeniusFixedSubring A p k)] : Finite ↥(fixedSubgroup (frobenius n hn p k A))

The Frobenius-fixed points of the full-weight type-Dₙ spin carrier form a finite group whenever the Frobenius-fixed subring is finite.

theorem TauCeti.TypeDSpinCarrier.finite_fixedSubgroup_frobenius_of_charP (n : ℕ) (hn : 4 ≤ n) (p k : ℕ) (K : Type v) [Field K] [Fact (Nat.Prime p)] [CharP K p] (hk : k ≠ 0) : Finite ↥(fixedSubgroup (frobenius n hn p k K))

The Frobenius-fixed points of the full-weight type-Dₙ spin carrier over a field of characteristic p form a finite group for every nonzero Frobenius exponent.