Identity components of closed subgroups

For a closed subgroup N of an affine group G, HopfIdeal.identityComponent cuts out N° as a closed subgroup of G. Its quotient coordinate algebra is canonically isomorphic to the coordinate algebra obtained by taking the identity component inside N.

The identity component has the same tangent Lie algebra as N, and hence the same dimension when N is smooth. When G and N are reduced, normality of N implies normality of N° in G: the identity component is characteristic in N, and normality can be tested on rational points. All statements are over an algebraically closed field; no connectedness of the ambient group is required.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 2.37 and Chapter 10.
• The construction uses CommHopfAlgCat.Hom.quotientIsoOfSurjective; normality uses HopfIdeal.IsNormal.comapOfSurjective_of_forall_iso.

noncomputable def TauCeti.HopfIdeal.identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : HopfIdeal k ↑H.obj

The defining Hopf ideal of the identity component of a closed subgroup, viewed as a closed subgroup of the original ambient group.

@[simp]

theorem TauCeti.HopfIdeal.mem_identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) (x : ↑H.obj) : x ∈ I.identityComponent ↔ (CommHopfAlgCat.Hom.hom (H.obj.mkQuotient I)) x ∈ HopfAlgebra.identityComponentHopfIdeal

A function vanishes on N° exactly when its restriction to N vanishes on the identity component of N.

theorem TauCeti.HopfIdeal.le_identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : I ≤ I.identityComponent

The identity component of a closed subgroup is contained in that subgroup. The inequality is reversed on defining ideals.

theorem TauCeti.HopfIdeal.identityComponent_le_of_le {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hIJ : I ≤ J) (hJ : geometricallyConnectedCommHopfAlgProperty k (H.quotient J).obj) : I.identityComponent ≤ J

A connected closed subgroup of a closed subgroup N is contained in the identity component of N. The inequalities are reversed because they compare defining ideals.

noncomputable def TauCeti.HopfIdeal.identityComponentQuotientIso {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : (H.quotient I.identityComponent).obj ≅ (H.quotient I).identityComponent.obj

Computing the coordinate algebra of N° inside G or inside N gives isomorphic commutative Hopf algebras.

@[simp]

theorem TauCeti.HopfIdeal.mkQuotient_comp_identityComponentQuotientIso_hom {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : CategoryTheory.CategoryStruct.comp (H.obj.mkQuotient I.identityComponent) I.identityComponentQuotientIso.hom = CategoryTheory.CategoryStruct.comp (H.obj.mkQuotient I) ((H.obj.quotient I).mkQuotient HopfAlgebra.identityComponentHopfIdeal)

The comparison of the two coordinate algebras of N° respects restriction of functions from the ambient group.

@[simp]

theorem TauCeti.HopfIdeal.mkQuotient_comp_identityComponentQuotientIso_hom_assoc {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) {Z : CommHopfAlgCat k} (h : (H.obj.quotient I).quotient HopfAlgebra.identityComponentHopfIdeal ⟶ Z) : CategoryTheory.CategoryStruct.comp (H.obj.mkQuotient I.identityComponent) (CategoryTheory.CategoryStruct.comp I.identityComponentQuotientIso.hom h) = CategoryTheory.CategoryStruct.comp (H.obj.mkQuotient I) (CategoryTheory.CategoryStruct.comp ((H.obj.quotient I).mkQuotient HopfAlgebra.identityComponentHopfIdeal) h)

The comparison of the two coordinate algebras of N° respects restriction of functions from the ambient group.

theorem TauCeti.HopfIdeal.geometricallyConnected_identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : geometricallyConnectedCommHopfAlgProperty k (H.quotient I.identityComponent).obj

The identity component of a closed subgroup is geometrically connected.

theorem TauCeti.HopfIdeal.smooth_identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) [Algebra.Smooth k ↑(H.quotient I).obj] : Algebra.Smooth k ↑(H.quotient I.identityComponent).obj

The identity component of a smooth closed subgroup is smooth.

theorem TauCeti.HopfIdeal.IsNormal.identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : I.IsNormal) [IsReduced ↑H.obj] [IsReduced ↑(H.quotient I).obj] : I.identityComponent.IsNormal

The identity component of a reduced normal closed subgroup is normal in a reduced ambient affine group.

@[simp]

theorem TauCeti.HopfIdeal.lieSubalgebra_identityComponent {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) : I.identityComponent.lieSubalgebra = I.lieSubalgebra

A closed subgroup and its identity component have the same tangent Lie algebra in the ambient group.

@[simp]

theorem TauCeti.HopfIdeal.ringKrullDim_quotient_identityComponent_of_smooth {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} (I : HopfIdeal k ↑H.obj) [Algebra.Smooth k (↑H.obj ⧸ I.toIdeal)] : ringKrullDim (↑H.obj ⧸ I.identityComponent.toIdeal) = ringKrullDim (↑H.obj ⧸ I.toIdeal)

A smooth closed subgroup and its identity component have the same Krull dimension.