Conjugation of Borel subgroups

Conjugation by a rational point is an automorphism of the ambient affine group, so it preserves Borel subgroups. This file records that invariance for the Hopf-ideal definition of a Borel subgroup, both over a general field and in the algebraically closed formulation.

This invariance is the half of a conjugacy statement for Borel subgroups that does not depend on the existence of a conjugating rational point. Over an algebraically closed field, the generic consequences of a theorem conjugating every Borel subgroup into a distinguished candidate are also collected here: the distinguished candidate is then a Borel subgroup, the Borel subgroups are exactly its conjugates, and any two of them are conjugate. Concrete matrix groups only need to supply that group-specific input, which Lie--Kolchin provides for the general linear group.

Main declarations

• TauCeti.HopfIdeal.IsBorel.conjugate: the conjugate of a Borel subgroup is Borel.
• TauCeti.HopfIdeal.isBorel_conjugate_iff: Borel status is invariant under conjugation.
• TauCeti.HopfIdeal.IsBorelOverAlgClosed.conjugate and TauCeti.HopfIdeal.isBorelOverAlgClosed_conjugate_iff: the same invariance for the algebraically closed Borel predicate.
• TauCeti.HopfIdeal.isBorelOverAlgClosed_of_forall_exists_conjugate_le: a Borel candidate into which every Borel subgroup can be conjugated is a Borel subgroup.
• TauCeti.HopfIdeal.isBorelOverAlgClosed_iff_exists_eq_conjugate: the Borel subgroups are then exactly its conjugates.
• TauCeti.HopfIdeal.exists_conjugate_eq_of_isBorelOverAlgClosed: any two Borel subgroups are then conjugate.

References

• J. S. Milne, Algebraic Groups (2017), Section 17.a.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), Section 11.1.
• TauCeti/Algebra/AlgebraicGroup/Torus/Conjugation.lean, for the analogous maximal-torus conjugation lemmas.

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

Conjugating a smooth connected solvable closed subgroup preserves these properties.

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

The conjugate of a Borel subgroup by a rational point is a Borel subgroup.

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

Borel status is invariant under conjugation by a rational point.

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

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

Over an algebraically closed field, the conjugate of a Borel subgroup by a rational point is a Borel subgroup.

theorem TauCeti.HopfIdeal.isBorelOverAlgClosed_conjugate_iff {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (I : HopfIdeal k H) (g : WithConv (H →ₐ[k] k)) : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) (I.conjugate g) ↔ IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I

The algebraically closed Borel property is invariant under conjugation by a rational point.

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

theorem TauCeti.HopfIdeal.isBorelOverAlgClosed_of_forall_exists_conjugate_le {k : Type u} [Field k] [IsAlgClosed k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (D : HopfIdeal k H) (hD : IsBorelCandidate k (FiniteTypeCommHopfAlgCat.of k H) D) (hcontain : ∀ (I : HopfIdeal k H), IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) D

A Borel candidate into which every Borel subgroup can be conjugated is a Borel subgroup. Over an algebraically closed field, if D cuts out a smooth, connected, solvable closed subgroup and every Borel subgroup lies in a conjugate of it, then D is maximal among smooth, connected, solvable closed subgroups.

theorem TauCeti.HopfIdeal.isBorelOverAlgClosed_iff_exists_eq_conjugate {k : Type u} [Field k] [IsAlgClosed k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (D : HopfIdeal k H) (hD : IsBorelCandidate k (FiniteTypeCommHopfAlgCat.of k H) D) (hcontain : ∀ (I : HopfIdeal k H), IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) (I : HopfIdeal k H) : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I ↔ ∃ (g : WithConv (H →ₐ[k] k)), I = D.conjugate g

Over an algebraically closed field, the Borel subgroups are exactly the conjugates of a distinguished Borel candidate into which every Borel subgroup can be conjugated.

theorem TauCeti.HopfIdeal.exists_conjugate_eq_of_isBorelOverAlgClosed {k : Type u} [Field k] [IsAlgClosed k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (D : HopfIdeal k H) (hD : IsBorelCandidate k (FiniteTypeCommHopfAlgCat.of k H) D) (hcontain : ∀ (I : HopfIdeal k H), IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I → ∃ (g : WithConv (H →ₐ[k] k)), D.conjugate g ≤ I) {I J : HopfIdeal k H} (hI : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) I) (hJ : IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.of k H) J) : ∃ (g : WithConv (H →ₐ[k] k)), I.conjugate g = J

Over an algebraically closed field, any two Borel subgroups are conjugate by a rational point, provided every Borel subgroup can be conjugated into a distinguished Borel candidate.