Special root-datum isogenies on split tori

The special isogenies of the pinned B₂, G₂, and F₄ root data induce endomorphisms of their split maximal tori. Their action on scheme-valued points is given by the Laurent monomials specified by the special-isogeny matrices, and their squares are the coordinatewise power maps of degrees two, three, and two. These are the maximal-torus restrictions of the corresponding special isogenies of pinned reductive groups.

Main definitions

• TauCeti.DynkinType.b2SpecialTorusEnd, TauCeti.DynkinType.g2SpecialTorusEnd, and TauCeti.DynkinType.f4SpecialTorusEnd: the split-torus morphisms prescribed by the three special root-datum isogenies.

Main results

• TauCeti.DynkinType.schemePointsMulEquiv_b2SpecialTorusEnd and its G₂ and F₄ counterparts: the coordinate action of the special torus maps on scheme-valued points.
• TauCeti.DynkinType.b2SpecialTorusEnd_comp_self, TauCeti.DynkinType.g2SpecialTorusEnd_comp_self, and TauCeti.DynkinType.f4SpecialTorusEnd_comp_self: the special torus maps square to the characteristic power maps.
• TauCeti.DynkinType.mapValue_frobenius_two_eq_comp_b2SpecialTorusEnd_comp_self and its G₂ and F₄ counterparts: on points in the defining characteristic, these squares are Frobenius.

References

• SGA 3, Exposés XXI–XXII.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

The special isogenies on split maximal tori

noncomputable def TauCeti.DynkinType.b2SpecialTorusEnd (R : Type) [CommRing R] : SplitTorus.groupScheme R (Fin 2) ⟶ SplitTorus.groupScheme R (Fin 2)

The split-torus morphism prescribed by the pinned B₂ special root-datum isogeny.

Equations

• TauCeti.DynkinType.b2SpecialTorusEnd R = TauCeti.SplitTorus.ofLinearMap R TauCeti.DynkinType.b2SpecialIsogeny.weightMap

noncomputable def TauCeti.DynkinType.g2SpecialTorusEnd (R : Type) [CommRing R] : SplitTorus.groupScheme R (Fin 2) ⟶ SplitTorus.groupScheme R (Fin 2)

The split-torus morphism prescribed by the pinned G₂ special root-datum isogeny.

Equations

• TauCeti.DynkinType.g2SpecialTorusEnd R = TauCeti.SplitTorus.ofLinearMap R TauCeti.DynkinType.g2SpecialIsogeny.weightMap

noncomputable def TauCeti.DynkinType.f4SpecialTorusEnd (R : Type) [CommRing R] : SplitTorus.groupScheme R (Fin 4) ⟶ SplitTorus.groupScheme R (Fin 4)

The split-torus morphism prescribed by the pinned F₄ special root-datum isogeny.

Equations

• TauCeti.DynkinType.f4SpecialTorusEnd R = TauCeti.SplitTorus.ofLinearMap R TauCeti.DynkinType.f4SpecialIsogeny.weightMap

@[simp]

theorem TauCeti.DynkinType.schemePointsMulEquiv_b2SpecialTorusEnd (R : Type) [CommRing R] {A : Type} [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R (Fin 2)).X) (i : Fin 2) : SplitTorus.schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (b2SpecialTorusEnd R).hom.hom) i = ![SplitTorus.schemePointsMulEquiv p 1 ^ 2, SplitTorus.schemePointsMulEquiv p 0] i

On scheme-valued points, the B₂ special torus endomorphism sends (x₀, x₁) to (x₁², x₀).

@[simp]

theorem TauCeti.DynkinType.schemePointsMulEquiv_g2SpecialTorusEnd (R : Type) [CommRing R] {A : Type} [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R (Fin 2)).X) (i : Fin 2) : SplitTorus.schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (g2SpecialTorusEnd R).hom.hom) i = ![SplitTorus.schemePointsMulEquiv p 1, SplitTorus.schemePointsMulEquiv p 0 ^ 3] i

On scheme-valued points, the G₂ special torus endomorphism sends (x₀, x₁) to (x₁, x₀³).

@[simp]

theorem TauCeti.DynkinType.schemePointsMulEquiv_f4SpecialTorusEnd (R : Type) [CommRing R] {A : Type} [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R (Fin 4)).X) (i : Fin 4) : SplitTorus.schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (f4SpecialTorusEnd R).hom.hom) i = ![SplitTorus.schemePointsMulEquiv p 3 ^ 2, SplitTorus.schemePointsMulEquiv p 2 ^ 2, SplitTorus.schemePointsMulEquiv p 1, SplitTorus.schemePointsMulEquiv p 0] i

On scheme-valued points, the F₄ special torus endomorphism sends (x₀, x₁, x₂, x₃) to (x₃², x₂², x₁, x₀).

@[simp]

theorem TauCeti.DynkinType.b2SpecialTorusEnd_comp_self (R : Type) [CommRing R] : CategoryTheory.CategoryStruct.comp (b2SpecialTorusEnd R) (b2SpecialTorusEnd R) = SplitTorus.powEnd R (Fin 2) 2

The square of the B₂ special torus endomorphism is the coordinatewise square map.

@[simp]

theorem TauCeti.DynkinType.g2SpecialTorusEnd_comp_self (R : Type) [CommRing R] : CategoryTheory.CategoryStruct.comp (g2SpecialTorusEnd R) (g2SpecialTorusEnd R) = SplitTorus.powEnd R (Fin 2) 3

The square of the G₂ special torus endomorphism is the coordinatewise cube map.

@[simp]

theorem TauCeti.DynkinType.f4SpecialTorusEnd_comp_self (R : Type) [CommRing R] : CategoryTheory.CategoryStruct.comp (f4SpecialTorusEnd R) (f4SpecialTorusEnd R) = SplitTorus.powEnd R (Fin 4) 2

The square of the F₄ special torus endomorphism is the coordinatewise square map.

Frobenius square relations on points

theorem TauCeti.DynkinType.mapValue_frobenius_two_eq_comp_b2SpecialTorusEnd_comp_self {A : Type} [CommRing A] [ExpChar A 2] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 2)).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (frobenius A 2).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (b2SpecialTorusEnd ℤ) (b2SpecialTorusEnd ℤ)).hom.hom

On points in characteristic two, the square of the B₂ special torus endomorphism is Frobenius.

theorem TauCeti.DynkinType.mapValue_frobenius_three_eq_comp_g2SpecialTorusEnd_comp_self {A : Type} [CommRing A] [ExpChar A 3] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 2)).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (frobenius A 3).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (g2SpecialTorusEnd ℤ) (g2SpecialTorusEnd ℤ)).hom.hom

On points in characteristic three, the square of the G₂ special torus endomorphism is Frobenius.

theorem TauCeti.DynkinType.mapValue_frobenius_two_eq_comp_f4SpecialTorusEnd_comp_self {A : Type} [CommRing A] [ExpChar A 2] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 4)).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (frobenius A 2).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (f4SpecialTorusEnd ℤ) (f4SpecialTorusEnd ℤ)).hom.hom

On points in characteristic two, the square of the F₄ special torus endomorphism is Frobenius.