Embedded Lie subgroups and the closed-subgroup theorem

A subgroup K of a Lie group G is an embedded Lie subgroup when it carries a smooth structure, for its subspace topology, making it a Lie group whose inclusion into G is smooth and an immersion. TauCeti.Lie.EmbeddedLieSubgroupData is that structure together with a choice of model vector space, and TauCeti.Lie.IsEmbeddedLieSubgroup is its existential form. Because the underlying topological space of K is the subspace topology of G, the inclusion is automatically a topological embedding, which is what distinguishes an embedded from a merely immersed subgroup; the remaining content is the smooth structure and the splitting of the differential.

The theorem of this file is Cartan's closed-subgroup theorem: a closed subgroup of a finite-dimensional real Lie group is an embedded Lie subgroup, with model vector space its Lie algebra TauCeti.Lie.lieSubalgebraOfSubgroup. It is what makes a group cut out of a Lie group by closed conditions -- a matrix group, a maximal torus, the kernel or centralizer of a continuous homomorphism -- a Lie group in its own right.

The model space being the Lie algebra pins the dimension of K. The finer statement that the Lie algebra of K as a Lie group maps isomorphically onto lieSubalgebraOfSubgroup K along the differential of the inclusion is not proved here.

Main definitions and results

• TauCeti.Lie.EmbeddedLieSubgroupData: a smooth structure exhibiting a subgroup as an embedded Lie subgroup, with a named model vector space.
• TauCeti.Lie.EmbeddedLieSubgroupData.injective_mfderiv_subtypeVal: the immersion half of being an embedded submanifold, read off from the data. The topological-embedding half is Topology.IsEmbedding.subtypeVal, since K carries the subspace topology.
• TauCeti.Lie.EmbeddedLieSubgroupData.isSmoothEmbedding_subtypeVal: the smooth embedding of a subgroup with a finite-dimensional boundaryless ambient model.
• TauCeti.Lie.EmbeddedLieSubgroupData.ofIsClosed: selected data for a closed subgroup.
• TauCeti.Lie.IsEmbeddedLieSubgroup: a subgroup admits such data, with TauCeti.Lie.isEmbeddedLieSubgroup_iff its characterization.
• TauCeti.Lie.EmbeddedLieSubgroupData.isEmbeddedLieSubgroup: data for a model space in the universe of G exhibits K as an embedded Lie subgroup.
• TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed: the closed-subgroup theorem with its model space, the data for a closed subgroup with model space its Lie algebra.
• TauCeti.Lie.isEmbeddedLieSubgroup_of_isClosed: the closed-subgroup (Cartan) theorem.
• TauCeti.Lie.discreteTopology_iff_lieSubalgebraOfSubgroup_eq_bot: a closed subgroup is discrete exactly when its Lie algebra is trivial.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Theorem 20.12.
• J. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups (2012), Section 9.1.

structure TauCeti.Lie.EmbeddedLieSubgroupData {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] (K : Subgroup G) (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] : Type (max u_1 w)

Embedded-Lie-subgroup data for a subgroup K of a charted group G, with model vector space E': a smooth structure on K, for its subspace topology and with the boundaryless model 𝓘(ℝ, E'), making K a Lie group whose inclusion into G is smooth and has a split differential everywhere.

The inclusion is a topological embedding for free, since K carries the subspace topology; the split differential is the smooth half of being an embedded submanifold.

• chartedSpace : ChartedSpace E' ↥K

  the charts of K, with model space E'

• lieGroup : LieGroup (modelWithCornersSelf ℝ E') ↑⊤ ↥K

  the charts are smoothly compatible and the inherited group operations are smooth

• contMDiff_subtypeVal : ContMDiff (modelWithCornersSelf ℝ E') I ↑⊤ fun (x : ↥K) => ↑x

  the inclusion into the ambient group is smooth

• isDiffImmersionAt_subtypeVal (k : ↥K) : IsDiffImmersionAt (modelWithCornersSelf ℝ E') I (fun (x : ↥K) => ↑x) k

  the differential of the inclusion has a continuous left inverse at every point

theorem TauCeti.Lie.EmbeddedLieSubgroupData.injective_mfderiv_subtypeVal {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] {K : Subgroup G} {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (d : EmbeddedLieSubgroupData I K E') (k : ↥K) : have x := d.chartedSpace; Function.Injective ⇑((mfderiv% fun (x : ↥K) => ↑x) k)

The differential of the inclusion of an embedded Lie subgroup is injective at every point, which is the usual phrasing of the immersion half of being an embedded submanifold.

theorem TauCeti.Lie.EmbeddedLieSubgroupData.isSmoothEmbedding_subtypeVal {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] {K : Subgroup G} {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [I.Boundaryless] (d : EmbeddedLieSubgroupData I K E') : have x := d.chartedSpace; Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ E') I ↑⊤ fun (k : ↥K) => ↑k

The inclusion of an embedded Lie subgroup is a smooth embedding.

def TauCeti.Lie.IsEmbeddedLieSubgroup {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] (K : Subgroup G) : Prop

K is an embedded Lie subgroup: it carries TauCeti.Lie.EmbeddedLieSubgroupData for some model vector space.

The model space is quantified over the universe of G, which is where the Lie algebra of G lives, exactly as Mathlib's Manifold.IsImmersionAt pins the universe of its complement.

theorem TauCeti.Lie.isEmbeddedLieSubgroup_iff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] {K : Subgroup G} : IsEmbeddedLieSubgroup K ↔ ∃ (E' : Type w) (x : NormedAddCommGroup E') (x_1 : NormedSpace ℝ E'), Nonempty (EmbeddedLieSubgroupData I K E')

Characterization of TauCeti.Lie.IsEmbeddedLieSubgroup: K is an embedded Lie subgroup exactly when it carries embedded-Lie-subgroup data for some model vector space in the universe of G. This is the elimination rule matching the introduction rule TauCeti.Lie.EmbeddedLieSubgroupData.isEmbeddedLieSubgroup.

theorem TauCeti.Lie.EmbeddedLieSubgroupData.isEmbeddedLieSubgroup {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] {K : Subgroup G} {E' : Type w} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (d : EmbeddedLieSubgroupData I K E') : IsEmbeddedLieSubgroup K

Embedded-Lie-subgroup data with a model space in the universe of G exhibits K as an embedded Lie subgroup.

theorem TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] {K : Subgroup G} (hK : IsClosed ↑K) : have x := ⋯; Nonempty (EmbeddedLieSubgroupData I K ↥(lieSubalgebraOfSubgroup K).toSubmodule)

The closed-subgroup theorem, with its model space. A closed subgroup of a finite-dimensional real Lie group carries embedded-Lie-subgroup data whose model vector space is the Lie algebra TauCeti.Lie.lieSubalgebraOfSubgroup of the subgroup.

noncomputable def TauCeti.Lie.EmbeddedLieSubgroupData.ofIsClosed {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) : EmbeddedLieSubgroupData I K ↥(lieSubalgebraOfSubgroup K).toSubmodule

The embedded Lie-subgroup structure selected for a closed subgroup, with its Lie algebra as model space.

theorem TauCeti.Lie.isEmbeddedLieSubgroup_of_isClosed {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] {K : Subgroup G} (hK : IsClosed ↑K) : IsEmbeddedLieSubgroup K

The closed-subgroup (Cartan) theorem. A closed subgroup of a finite-dimensional real Lie group is an embedded Lie subgroup: it is a Lie group for its subspace topology, and its inclusion is smooth with everywhere split differential.

theorem TauCeti.Lie.discreteTopology_iff_lieSubalgebraOfSubgroup_eq_bot {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) : DiscreteTopology ↥K ↔ lieSubalgebraOfSubgroup K = ⊥

A closed subgroup is discrete exactly when its Lie algebra is trivial. If K is discrete, each one-parameter subgroup lying in K is constant, so its generator vanishes. Conversely, by the closed-subgroup theorem K is a manifold modelled on its Lie algebra, which is then the zero space, so the points of K are open.