The conormal sequence of a closed affine subgroup

Let I be a Hopf ideal of a commutative Hopf algebra H. The quotient map H ⟶ H/I induces a surjection on augmentation cotangent spaces. Its kernel is the image of I in the ambient cotangent space, the conormal space of the corresponding closed subgroup at the identity. Thus there is a short exact sequence over any commutative base ring

N* ⟶ Tₑ*G ⟶ Tₑ*V(I) ⟶ 0.

Dualizing recovers the injective differential constructed in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Tangent. In finite dimension, rank-nullity gives dim Lie(V(I)) + dim N* = dim Lie(G). This is the closed-subgroup conormal and dimension tool needed in Layer 2 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.HopfIdeal.conormalSubspace: the image of the defining Hopf ideal in the ambient augmentation cotangent space.
• TauCeti.HopfIdeal.quotientCotangentMap: the map on cotangent spaces induced by the quotient.
• TauCeti.HopfIdeal.quotientCotangentMap_toCotangent: the quotient map on an augmentation-ideal representative.
• TauCeti.HopfIdeal.cotangentLinearEquiv_comp_quotientCotangentMap: dualizing the cotangent map gives the differential of the closed-subgroup inclusion.
• TauCeti.HopfIdeal.quotientCotangentMap_surjective: right exactness of the conormal sequence.
• TauCeti.HopfIdeal.ker_quotientCotangentMap: its kernel is the conormal subspace.
• TauCeti.HopfIdeal.quotientLieHom_surjective_iff_conormalSubspace_eq_bot: the closed-subgroup differential is onto exactly when its conormal space vanishes.
• TauCeti.HopfIdeal.conormalSubspace_eq_bot_iff_toIdeal_le_sq_augmentationIdeal: conormal vanishing means that the defining ideal has no linear term at the identity.
• TauCeti.HopfIdeal.finrank_quotientLie_add_finrank_conormal: the resulting dimension formula.
• TauCeti.HopfIdeal.finrank_quotientLie_le: the resulting closed-subgroup dimension bound.
• TauCeti.HopfIdeal.exists_maximal_finrank_quotientLie: every nonempty family of closed subgroups contains one of maximal Lie dimension.
• TauCeti.HopfIdeal.finrank_quotientLie_antitone: inclusion of closed subgroups cannot increase Lie dimension.

References

J. S. Milne, Algebraic Groups (2017), §10.a; the conormal sequence is the cotangent-space form of the tangent inclusion of a closed subgroup. The implementation uses Mathlib's general Ideal.mapCotangent exactness API.

noncomputable def TauCeti.HopfIdeal.conormalSubspace {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : Submodule k (Bialgebra.CotangentSpace k H)

The image of a closed subgroup's defining Hopf ideal in the ambient augmentation cotangent space. This is the conormal space at the identity, equivalently I / (I ∩ (ker ε)²) embedded in (ker ε) / (ker ε)².

Equations

• I.conormalSubspace = Submodule.map (TauCeti.Bialgebra.cotangentMap k H) (Submodule.restrictScalars k I.toIdeal)

@[simp]

theorem TauCeti.HopfIdeal.mem_conormalSubspace_iff {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) (x : Bialgebra.CotangentSpace k H) : x ∈ I.conormalSubspace ↔ ∃ y ∈ I.toIdeal, (Bialgebra.cotangentMap k H) y = x

Membership in the conormal subspace means being represented by an element of the defining Hopf ideal.

theorem TauCeti.HopfIdeal.conormalSubspace_mono {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] {I J : HopfIdeal k H} (hIJ : I ≤ J) : I.conormalSubspace ≤ J.conormalSubspace

Enlarging the defining Hopf ideal enlarges the conormal space of the corresponding closed subgroup at the identity.

noncomputable def TauCeti.HopfIdeal.quotientCotangentMap {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : Bialgebra.CotangentSpace k H →ₗ[k] Bialgebra.CotangentSpace k (H ⧸ I.toIdeal)

The map on augmentation cotangent spaces induced by the quotient H ⟶ H/I.

Equations

• I.quotientCotangentMap = ↑k ((TauCeti.Bialgebra.AugmentationIdeal k H).mapCotangent (TauCeti.Bialgebra.AugmentationIdeal k (H ⧸ I.toIdeal)) (Algebra.ofId H (H ⧸ I.toIdeal)) ⋯)

@[simp]

theorem TauCeti.HopfIdeal.quotientCotangentMap_toCotangent {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) (x : ↥(Bialgebra.AugmentationIdeal k H)) : I.quotientCotangentMap ((Bialgebra.AugmentationIdeal k H).toCotangent x) = (Bialgebra.AugmentationIdeal k (H ⧸ I.toIdeal)).toCotangent ⟨(algebraMap H (H ⧸ I.toIdeal)) ↑x, ⋯⟩

The quotient cotangent map sends the class of an augmentation-ideal element to the class of its image in the quotient.

theorem TauCeti.HopfIdeal.quotientCotangentMap_cotangentMap {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) (x : H) : I.quotientCotangentMap ((Bialgebra.cotangentMap k H) x) = (Bialgebra.cotangentMap k (H ⧸ I.toIdeal)) ((Ideal.Quotient.mkₐ k I.toIdeal) x)

The quotient cotangent map sends the first-order displacement of x to the first-order displacement of its quotient class.

@[simp]

theorem TauCeti.HopfIdeal.cotangentLinearEquiv_comp_quotientCotangentMap {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] {B : Type w} [CommRing B] [Algebra k B] (I : HopfIdeal k H) (f : Bialgebra.CotangentSpace k (H ⧸ I.toIdeal) →ₗ[k] B) : I.quotientLieHom (Derivation.cotangentLinearEquiv f) = Derivation.cotangentLinearEquiv (f ∘ₗ I.quotientCotangentMap)

Under cotangent duality, precomposition by the quotient cotangent map is the differential of the closed-subgroup inclusion.

theorem TauCeti.HopfIdeal.quotientCotangentMap_surjective {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : Function.Surjective ⇑I.quotientCotangentMap

The map from the ambient cotangent space to the closed subgroup's cotangent space is surjective.

theorem TauCeti.HopfIdeal.ker_quotientCotangentMap {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : I.quotientCotangentMap.ker = I.conormalSubspace

The kernel of the quotient cotangent map is exactly the conormal subspace, giving the exact conormal sequence of a closed affine subgroup at the identity.

@[simp]

theorem TauCeti.HopfIdeal.conormalSubspace_eq_bot_iff_toIdeal_le_sq_augmentationIdeal {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : I.conormalSubspace = ⊥ ↔ I.toIdeal ≤ Bialgebra.AugmentationIdeal k H ^ 2

A closed subgroup has zero conormal space at the identity exactly when every element of its defining ideal vanishes to second order there.

theorem TauCeti.HopfIdeal.quotientLieHom_surjective_iff_conormalSubspace_eq_bot {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) : Function.Surjective ⇑I.quotientLieHom ↔ I.conormalSubspace = ⊥

The differential of a closed-subgroup inclusion is surjective exactly when the subgroup has zero conormal space at the identity. Equivalently, the inclusion is an infinitesimal equality at the identity.

theorem TauCeti.HopfIdeal.conormalSubspace_ker_eq_bot_of_surjective_of_derivationCompLieHom_surjective {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] {K : Type w} [CommRing K] [HopfAlgebra k K] (f : H →ₐc[k] K) (hf : Function.Surjective ⇑f) (hdf : Function.Surjective ⇑(derivationCompLieHom f)) : (ker f).conormalSubspace = ⊥

The kernel of a surjective Hopf-algebra morphism has zero conormal space when the differential of the morphism is surjective.

theorem TauCeti.HopfIdeal.finrank_quotientCotangent_add_finrank_conormal {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) [FiniteDimensional k (Bialgebra.CotangentSpace k H)] : Module.finrank k (Bialgebra.CotangentSpace k (H ⧸ I.toIdeal)) + Module.finrank k ↥I.conormalSubspace = Module.finrank k (Bialgebra.CotangentSpace k H)

In finite dimension, the dimension of the closed subgroup's cotangent space plus its conormal dimension is the dimension of the ambient cotangent space.

theorem TauCeti.HopfIdeal.finrank_quotientLie_add_finrank_conormal {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) [FiniteDimensional k (Bialgebra.CotangentSpace k H)] : Module.finrank k (Derivation k (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (H ⧸ I.toIdeal) k)) + Module.finrank k ↥I.conormalSubspace = Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k))

For a finite-dimensional ambient cotangent space, the Lie algebra dimension of a closed subgroup plus its conormal dimension is the Lie algebra dimension of the ambient group.

theorem TauCeti.HopfIdeal.finrank_quotientLie_le {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) [FiniteDimensional k (Bialgebra.CotangentSpace k H)] : Module.finrank k (Derivation k (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (H ⧸ I.toIdeal) k)) ≤ Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k))

The Lie dimension of a closed subgroup is at most the Lie dimension of the ambient affine group when the ambient cotangent space is finite-dimensional.

theorem TauCeti.HopfIdeal.exists_maximal_finrank_quotientLie {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [FiniteDimensional k (Bialgebra.CotangentSpace k H)] (P : HopfIdeal k H → Prop) (hP : ∃ (I : HopfIdeal k H), P I) : ∃ (I : HopfIdeal k H), P I ∧ ∀ (J : HopfIdeal k H), P J → Module.finrank k (Derivation k (H ⧸ J.toIdeal) (Bialgebra.CounitAlgebra k (H ⧸ J.toIdeal) k)) ≤ Module.finrank k (Derivation k (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (H ⧸ I.toIdeal) k))

Every nonempty family of closed affine subgroups contains one of maximal Lie dimension.

The family is specified by a predicate on its defining Hopf ideals. Its attained dimensions lie in the finite interval from zero to the Lie dimension of the ambient group, so a maximum exists without any finiteness assumption on the family itself.

theorem TauCeti.HopfIdeal.finrank_quotientLie_antitone {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [FiniteDimensional k (Bialgebra.CotangentSpace k H)] : Antitone fun (I : HopfIdeal k H) => Module.finrank k (Derivation k (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (H ⧸ I.toIdeal) k))

Lie dimension is antitone in the defining Hopf ideal: if I ≤ J, then the closed subgroup cut out by J is contained in the one cut out by I, so its Lie dimension is no larger.