Conjugation of closed subgroup schemes

A rational point of an affine group conjugates its closed subgroup schemes. In Hopf coordinates, closed subgroups are represented contravariantly by Hopf ideals, so conjugating an ideal means taking its inverse image under the coordinate automorphism of point conjugation.

This file makes that operation a group action on Hopf ideals. It proves the order and membership characterizations and checks its geometric meaning on points: pulling a point back by the inner automorphism identifies the points cut out by an ideal with those cut out by its conjugate.

The action is the basic language needed for conjugacy theorems for Borel subgroups and maximal tori.

A rational point g normalizes the closed subgroup N cut out by I when conjugation by g maps I into itself; every rational point normalizes a normal closed subgroup. Conjugation by a normalizing point then restricts to an endomorphism of N, whose coordinate map is the bialgebra endomorphism of H ⧸ I induced by point conjugation. This is how normalizing points act on the characters of N.

Main declarations

• TauCeti.HopfIdeal.conjugate: the Hopf ideal of the conjugated closed subgroup.
• TauCeti.HopfIdeal.instMulAction: rational points act on Hopf ideals by conjugation.
• TauCeti.HopfIdeal.IsNormal.le_conjugate: rational points normalize a normal closed subgroup.
• TauCeti.HopfIdeal.quotientPointConjugation: conjugation by a normalizing point, restricted to the subgroup, as a bialgebra endomorphism of its coordinate algebra.
• TauCeti.CommHopfAlgCat.mapDomain_pointConjugation_mem_conjugate_iff: the pointwise interpretation of the conjugated ideal.

References

• J. S. Milne, Algebraic Groups (2017), Sections 3.5 and 17.a.
• T. A. Springer, Linear Algebraic Groups, Sections 6.2--6.3.

noncomputable def TauCeti.HopfIdeal.conjugate {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : HopfIdeal R H

The Hopf ideal cutting out the conjugate of a closed subgroup by a rational point.

If I cuts out K and g is an R-valued point, this ideal cuts out gKg⁻¹. Since coordinate maps are contravariant, it is the inverse image of I under the coordinate automorphism of x ↦ gxg⁻¹.

Equations

• I.conjugate g = I.comapOfSurjective (TauCeti.HopfAlgebra.pointConjugationBialgEquiv g).toBialgHom ⋯

theorem TauCeti.HopfIdeal.conjugate_eq_comapOfSurjective {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : I.conjugate g = I.comapOfSurjective (HopfAlgebra.pointConjugationBialgEquiv g).toBialgHom ⋯

Conjugation is the inverse image under the bialgebra automorphism of point conjugation.

This is the public interface lemma for conjugate: the definition's body is not exposed outside this module, so downstream files cannot unfold it and rewrite with this instead.

@[simp]

theorem TauCeti.HopfIdeal.mem_conjugate {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {g : WithConv (H →ₐ[R] R)} {x : H} : x ∈ I.conjugate g ↔ (HopfAlgebra.pointConjugationAlgHom g) x ∈ I

Membership in a conjugated Hopf ideal is tested after applying the coordinate automorphism of point conjugation.

@[simp]

theorem TauCeti.HopfIdeal.conjugate_one {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.conjugate 1 = I

Conjugation by the identity point fixes every Hopf ideal.

theorem TauCeti.HopfIdeal.conjugate_mul {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g h : WithConv (H →ₐ[R] R)) : I.conjugate (g * h) = (I.conjugate h).conjugate g

Successive conjugations are conjugation by the product of the points.

@[simp]

theorem TauCeti.HopfIdeal.conjugate_inv_conjugate {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : (I.conjugate g).conjugate g⁻¹ = I

Conjugating by a point and then by its inverse recovers the original Hopf ideal.

@[simp]

theorem TauCeti.HopfIdeal.conjugate_conjugate_inv {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : (I.conjugate g⁻¹).conjugate g = I

Conjugating by the inverse point and then by the point recovers the original Hopf ideal.

theorem TauCeti.HopfIdeal.conjugate_mono {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) {I J : HopfIdeal R H} (h : I ≤ J) : I.conjugate g ≤ J.conjugate g

Conjugation is monotone on Hopf ideals.

theorem TauCeti.HopfIdeal.conjugate_inv_le_of_mem_quotientPointsSubgroup {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {A : Type w} [CommRing A] [Algebra R A] (I J : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (π : H →ₐ[R] A) (hker : ∀ (x : H), π x = 0 → x ∈ I) (hmem : WithConv.toConv (π.comp (HopfAlgebra.pointConjugationAlgHom g)) ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) J ↧A) : J.conjugate g⁻¹ ≤ I

If a conjugated point annihilates J and the kernel of the original point is contained in I, then conjugating J by the inverse point gives an ideal contained in I.

theorem TauCeti.HopfIdeal.conjugate_inv_le_of_mem_quotientPointsSubgroup_mkQuotient {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I J : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (hmem : WithConv.toConv ((↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (↧H) I))).comp (HopfAlgebra.pointConjugationAlgHom g)) ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) J ↧↑(CommHopfAlgCat.quotient (↧H) I)) : J.conjugate g⁻¹ ≤ I

If the conjugated generic point of the quotient by I belongs to the subgroup defined by J, then J.conjugate g⁻¹ ≤ I.

@[simp]

theorem TauCeti.HopfIdeal.conjugate_le_conjugate_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I J : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : I.conjugate g ≤ J.conjugate g ↔ I ≤ J

Conjugation preserves and reflects containment of Hopf ideals.

@[simp]

theorem TauCeti.HopfIdeal.conjugate_eq_conjugate_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I J : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) : I.conjugate g = J.conjugate g ↔ I = J

Conjugation preserves and reflects equality of Hopf ideals.

@[instance_reducible]

noncomputable instance TauCeti.HopfIdeal.instMulAction {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] : MulAction (WithConv (H →ₐ[R] R)) (HopfIdeal R H)

Rational points act on Hopf ideals by conjugating the represented closed subgroup.

Equations

• TauCeti.HopfIdeal.instMulAction = { smul := fun (g : WithConv (H →ₐ[R] R)) (I : TauCeti.HopfIdeal R H) => I.conjugate g, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.HopfIdeal.smul_eq_conjugate {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) (I : HopfIdeal R H) : g • I = I.conjugate g

The rational-point action on Hopf ideals is conjugation.

theorem TauCeti.HopfIdeal.IsNormal.le_conjugate {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} (hI : I.IsNormal) (g : WithConv (H →ₐ[R] R)) : I ≤ I.conjugate g

Every rational point normalizes a normal closed subgroup: conjugation by it maps the defining ideal into itself.

noncomputable def TauCeti.HopfIdeal.quotientPointConjugation {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (hg : I ≤ I.conjugate g) : H ⧸ I.toIdeal →ₐc[R] H ⧸ I.toIdeal

Conjugation by a rational point g normalizing the closed subgroup N cut out by I, restricted to N. This is the bialgebra endomorphism of H ⧸ I induced by the coordinate map of x ↦ g x g⁻¹.

Equations

• I.quotientPointConjugation g hg = Bialgebra.Quotient.liftBialgHom I.toIdeal ((Bialgebra.Quotient.mkBialgHom I.toIdeal).comp (TauCeti.HopfAlgebra.pointConjugationBialgEquiv g).toBialgHom) ⋯

@[simp]

theorem TauCeti.HopfIdeal.quotientPointConjugation_mk {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (hg : I ≤ I.conjugate g) (x : H) : (I.quotientPointConjugation g hg) ((Ideal.Quotient.mk I.toIdeal) x) = (Ideal.Quotient.mk I.toIdeal) ((HopfAlgebra.pointConjugationAlgHom g) x)

Restricted conjugation sends the class of x to the class of its conjugate.

@[simp]

theorem TauCeti.HopfIdeal.quotientPointConjugation_one {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (h : I ≤ I.conjugate 1) : I.quotientPointConjugation 1 h = BialgHom.id R (H ⧸ I.toIdeal)

Restricted conjugation by the identity point is the identity.

theorem TauCeti.HopfIdeal.quotientPointConjugation_mul {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g h : WithConv (H →ₐ[R] R)) (hg : I ≤ I.conjugate g) (hh : I ≤ I.conjugate h) (hgh : I ≤ I.conjugate (g * h)) : I.quotientPointConjugation (g * h) hgh = (I.quotientPointConjugation h hh).comp (I.quotientPointConjugation g hg)

Restricted conjugations compose in the order forced by contravariance.

theorem TauCeti.CommHopfAlgCat.mapDomain_pointConjugation_mem_conjugate_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (A : CommAlgCat R) (x : ↑(HopfAlgebra.points A)) : (AlgHom.mapDomain (HopfAlgebra.pointConjugationBialgEquiv g).toBialgHom) x ∈ quotientPointsSubgroup (↧H) (I.conjugate g) A ↔ x ∈ quotientPointsSubgroup (↧H) I A

Point conjugation identifies the subgroup cut out by a Hopf ideal with the subgroup cut out by its conjugate.

theorem TauCeti.CommHopfAlgCat.pointConjugation_mem_conjugate_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (g : WithConv (H →ₐ[R] R)) (A : CommAlgCat R) (x : ↑(HopfAlgebra.points A)) : (AlgHom.mapValue (Algebra.ofId R ↑A)) g * x * ((AlgHom.mapValue (Algebra.ofId R ↑A)) g)⁻¹ ∈ quotientPointsSubgroup (↧H) (I.conjugate g) A ↔ x ∈ quotientPointsSubgroup (↧H) I A

In explicit pointwise terms, conjugating a point by g carries the points of I exactly onto the points of the conjugated ideal.