Conjugation of maximal tori

Conjugation by a rational point is an automorphism of the ambient affine group, so it preserves maximal tori. This file records that invariance for the Hopf-ideal definition of a maximal torus.

This invariance is the half of a conjugacy statement for maximal tori that does not depend on the existence of a conjugating rational point. Generic consequences of a theorem conjugating diagonalizable subgroups into a distinguished maximal torus are also collected here, so concrete matrix groups only need to supply that group-specific input.

Main declarations

• TauCeti.HopfIdeal.IsMaximalTorus.conjugate: the conjugate of a maximal torus is maximal.
• TauCeti.HopfIdeal.isMaximalTorus_conjugate_iff: maximal-torus status is invariant under conjugation.
• TauCeti.HopfIdeal.exists_eq_conjugate_of_isMaximalTorus_of_split: a split maximal torus is conjugate to a distinguished maximal torus whenever diagonalizable subgroups can be conjugated into it.

References

• J. S. Milne, Algebraic Groups (2017), Section 17.a.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), Section 11.1.

theorem TauCeti.HopfIdeal.IsMaximalTorus.conjugate {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {I : HopfIdeal k H} (hI : IsMaximalTorus k (↧H) I) (g : WithConv (H →ₐ[k] k)) : IsMaximalTorus k (↧H) (I.conjugate g)

The conjugate of a maximal torus by a rational point is a maximal torus.

theorem TauCeti.HopfIdeal.isMaximalTorus_conjugate_iff {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (I : HopfIdeal k H) (g : WithConv (H →ₐ[k] k)) : IsMaximalTorus k (↧H) (I.conjugate g) ↔ IsMaximalTorus k (↧H) I

Maximal-torus status is invariant under conjugation by a rational point.

This is not a simp lemma: isMaximalTorus_iff unfolds IsMaximalTorus on the left-hand side, so the statement is never in simp-normal form.

theorem TauCeti.HopfIdeal.exists_eq_conjugate_of_isMaximalTorus_of_split {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (D : HopfIdeal k H) (hD : IsMaximalTorus k (↧H) D) {I : HopfIdeal k H} (hcontain : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) (hI : IsMaximalTorus k (↧H) I) (hsplit : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I)) : ∃ (g : WithConv (H →ₐ[k] k)), I = D.conjugate g

A split maximal torus is conjugate to a distinguished maximal torus, provided it can be conjugated into the distinguished torus.

theorem TauCeti.HopfIdeal.exists_conjugate_eq_of_isMaximalTorus_of_split {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (D : HopfIdeal k H) (hD : IsMaximalTorus k (↧H) D) {I J : HopfIdeal k H} (hcontainI : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) (hcontainJ : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } J) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ J) (hI : IsMaximalTorus k (↧H) I) (hJ : IsMaximalTorus k (↧H) J) (hsplitI : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I)) (hsplitJ : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } J)) : ∃ (g : WithConv (H →ₐ[k] k)), I.conjugate g = J

Any two split maximal tori are conjugate when diagonalizable subgroups can be conjugated into a distinguished maximal torus.

theorem TauCeti.HopfIdeal.isMaximalTorus_iff_exists_eq_conjugate {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsAlgClosed k] (D : HopfIdeal k H) (hD : IsMaximalTorus k (↧H) D) (I : HopfIdeal k H) (hcontain : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) : IsMaximalTorus k (↧H) I ↔ ∃ (g : WithConv (H →ₐ[k] k)), I = D.conjugate g

Over an algebraically closed field, the maximal tori are exactly the conjugates of a distinguished maximal torus when diagonalizable subgroups can be conjugated into it.

theorem TauCeti.HopfIdeal.exists_conjugate_eq_of_isMaximalTorus {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsAlgClosed k] (D : HopfIdeal k H) (hD : IsMaximalTorus k (↧H) D) {I J : HopfIdeal k H} (hcontainI : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } I) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) (hcontainJ : DiagonalizableGroup.groupLikeSpannedProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := ↧H, property := ⋯ } J) → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ J) (hI : IsMaximalTorus k (↧H) I) (hJ : IsMaximalTorus k (↧H) J) : ∃ (g : WithConv (H →ₐ[k] k)), I.conjugate g = J

Over an algebraically closed field, any two maximal tori are conjugate when diagonalizable subgroups can be conjugated into a distinguished maximal torus.