Chosen split maximal tori over a ring

SplitMaximalTorus R H r is a closed immersion of the standard rank-r split torus into the affine group with coordinate algebra H, maximal on every geometric fiber. It carries the coordinate morphism itself, rather than an existence assertion. The corresponding Hopf ideal and its quotient presentation are recovered from that morphism.

Maximality on geometric fibers is essential: maximality merely among tori over the base does not imply this condition. A chosen split maximal torus does not include a pinning or trivializations of the root spaces over the base.

Chosen split maximal tori are transported along isomorphisms of coordinate Hopf algebras (SplitMaximalTorus.comapOfIso) and base-changed along ring maps R → S (SplitMaximalTorus.baseChange). The base-changed torus is cut out by the base change of the original defining ideal, and its geometric fibers are geometric fibers of the original torus, so a torus chosen over ℤ specializes to every commutative ring.

Main declarations

• TauCeti.SplitMaximalTorus: a chosen split maximal torus of an affine group over a ring.
• TauCeti.SplitMaximalTorus.comapOfIso: transport along an isomorphism of coordinate Hopf algebras.
• TauCeti.SplitMaximalTorus.baseChange: base change along R → S.
• TauCeti.SplitMaximalTorus.definingIdeal_baseChange: the base-changed torus is cut out by the base change of the defining ideal.

References

• B. Conrad, Reductive Group Schemes (2014), Definition 3.2.1 and Example 3.2.3.

structure TauCeti.SplitMaximalTorus (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Algebra.FiniteType R ↑H] (r : ℕ) : Type u

A parametrized split maximal torus of an affine group over R. The coordinate map is surjective, expressing a closed immersion, and its defining ideal is maximal as a torus on every geometric fiber.

• coordinateMap : H ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))).obj

  Restriction of functions to the chosen rank-r split torus.

• surjective : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom self.coordinateMap)

  The chosen torus is a closed subgroup.

• maximal (k : Type u) [Field k] [Algebra R k] [IsAlgClosed k] : HopfIdeal.IsMaximalTorus k (CommHopfAlgCat.baseChange H) (CommHopfAlgCat.baseChangeHopfIdeal (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom self.coordinateMap) ⋯))

  The chosen torus is maximal in every geometric fiber.

theorem TauCeti.SplitMaximalTorus.ext {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} {T U : SplitMaximalTorus R H r} (h : T.coordinateMap = U.coordinateMap) : T = U

A chosen split maximal torus is determined by its coordinate map.

theorem TauCeti.SplitMaximalTorus.ext_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} {T U : SplitMaximalTorus R H r} : T = U ↔ T.coordinateMap = U.coordinateMap

noncomputable def TauCeti.SplitMaximalTorus.definingIdeal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) : HopfIdeal R ↑H

The Hopf ideal cutting out the chosen split maximal torus.

Equations

• T.definingIdeal = TauCeti.HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom T.coordinateMap) ⋯

@[simp]

theorem TauCeti.SplitMaximalTorus.mem_definingIdeal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) (x : ↑H) : x ∈ T.definingIdeal ↔ (CommHopfAlgCat.Hom.hom T.coordinateMap) x = 0

A function belongs to the defining ideal exactly when its restriction to the torus is zero.

noncomputable def TauCeti.SplitMaximalTorus.coordinateIso {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) : (FiniteTypeCommHopfAlgCat.of R ↑H).quotient T.definingIdeal ≅ DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))

The quotient coordinate algebra of the chosen torus is the standard split-torus algebra.

Equations

• T.coordinateIso = (TauCeti.finiteTypeCommHopfAlgProperty R).isoMk (TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso T.coordinateMap ⋯)

@[simp]

theorem TauCeti.SplitMaximalTorus.mkQuotient_comp_coordinateIso_hom {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) : CategoryTheory.CategoryStruct.comp ((FiniteTypeCommHopfAlgCat.of R ↑H).mkQuotient T.definingIdeal) T.coordinateIso.hom = CategoryTheory.ObjectProperty.homMk T.coordinateMap

The quotient presentation recovers restriction to the torus.

theorem TauCeti.SplitMaximalTorus.splitTorus_quotient {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) : splitTorusCommHopfAlgProperty R ((FiniteTypeCommHopfAlgCat.of R ↑H).quotient T.definingIdeal)

The closed subgroup defined by the chosen torus is a split torus over the base ring.

theorem TauCeti.SplitMaximalTorus.isMaximalTorus_geometricFiber {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (T : SplitMaximalTorus R H r) (k : Type u) [Field k] [Algebra R k] [IsAlgClosed k] : HopfIdeal.IsMaximalTorus k (CommHopfAlgCat.baseChange H) (CommHopfAlgCat.baseChangeHopfIdeal T.definingIdeal)

The chosen torus is maximal after extension to any algebraically closed field over R.

noncomputable def TauCeti.SplitMaximalTorus.comapOfIso {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} {L : CommHopfAlgCat R} [Algebra.FiniteType R ↑L] (T : SplitMaximalTorus R L r) (e : H ≅ L) : SplitMaximalTorus R H r

Transport of a chosen split maximal torus across an isomorphism e : H ≅ L of coordinate Hopf algebras: the torus of L becomes a torus of H by restricting functions along e.

Equations

• T.comapOfIso e = { coordinateMap := CategoryTheory.CategoryStruct.comp e.hom T.coordinateMap, surjective := ⋯, maximal := ⋯ }

@[simp]

theorem TauCeti.SplitMaximalTorus.comapOfIso_coordinateMap {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} {L : CommHopfAlgCat R} [Algebra.FiniteType R ↑L] (T : SplitMaximalTorus R L r) (e : H ≅ L) : (T.comapOfIso e).coordinateMap = CategoryTheory.CategoryStruct.comp e.hom T.coordinateMap

The transported torus has coordinate map e.hom ≫ T.coordinateMap.

@[simp]

theorem TauCeti.SplitMaximalTorus.definingIdeal_comapOfIso {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} {L : CommHopfAlgCat R} [Algebra.FiniteType R ↑L] (T : SplitMaximalTorus R L r) (e : H ≅ L) : (T.comapOfIso e).definingIdeal = T.definingIdeal.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯

The defining ideal of the transported torus is the pullback of the original defining ideal along e.

noncomputable def TauCeti.SplitMaximalTorus.baseChange {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (S : Type u) [CommRing S] [Algebra R S] (T : SplitMaximalTorus R H r) : SplitMaximalTorus S (CommHopfAlgCat.baseChange H) r

Base change of a chosen split maximal torus along R → S. Its coordinate map is the base change of the original one, read in the standard split-torus coordinates over S; its geometric fibers are geometric fibers of the original torus.

Equations

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

@[simp]

theorem TauCeti.SplitMaximalTorus.baseChange_coordinateMap {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (S : Type u) [CommRing S] [Algebra R S] (T : SplitMaximalTorus R H r) : (baseChange S T).coordinateMap = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap T.coordinateMap) (DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso R S (SplitTorus.characterGroup (ULift.{u, 0} (Fin r)))).hom

The base-changed torus has the base-changed coordinate map.

@[simp]

theorem TauCeti.SplitMaximalTorus.definingIdeal_baseChange {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {r : ℕ} (S : Type u) [CommRing S] [Algebra R S] (T : SplitMaximalTorus R H r) : (baseChange S T).definingIdeal = CommHopfAlgCat.baseChangeHopfIdeal T.definingIdeal

The defining ideal of the base-changed torus is the base change of the defining ideal.