The Lie subalgebra of a subgroup

For a subgroup K of a Lie group G the derivations whose one-parameter subgroup never leaves K,

𝔨 = {X : 𝔤 | ∀ t : ℝ, lieExp (t • X) ∈ K},

are the candidate Lie algebra of K. TauCeti.Lie.lieSubalgebraOfSubgroup K is the Lie subalgebra of 𝔤 they generate, defined for every subgroup, and this file proves that for a closed K the generating set is already a Lie subalgebra, so that the generation is inert and membership is exactly the defining condition (TauCeti.Lie.mem_lieSubalgebraOfSubgroup).

Addition and the bracket produce the new element as a limit of elements of K, each using a different piece of the Layer 0/1 machinery; scalars involve no limit at all:

• scalars are free: t • (c • X) = (t * c) • X reparametrises the exponential line of X, so the one-parameter subgroup of c • X is a reparametrisation of that of X and lands in K on the nose;
• addition is the Trotter product formula TauCeti.Lie.tendsto_lieExp_smul_mul_lieExp_smul_pow, which exhibits lieExp (t • (X + Y)) as a limit of products of elements of K;
• the bracket is the infinitesimal adjoint. If X and Y both generate one-parameter subgroups inside K then so does Ad (lieExp (s • X)) Y, by the conjugation formula TauCeti.Lie.conj_lieExp; the curve s ↦ Ad (lieExp (s • X)) Y therefore runs inside 𝔨 and starts at Y, and its derivative at 0 is ⁅X, Y⁆ by TauCeti.Lie.hasDerivAt_Ad_lieExp_smul_apply_zero, the derivation-level form of the Layer 1 theorem TauCeti.Lie.hasDerivAt_tangentAd_mulInvariantExp_smul_apply_zero. A difference quotient of a curve in a linear subspace stays in that subspace, so ⁅X, Y⁆ lies in its closure.

Why the definition generates, and closedness

The definition of lieSubalgebraOfSubgroup is total in K, as the roadmap specifies it, because it takes the Lie subalgebra generated by 𝔨 rather than asserting that 𝔨 is one. That the generating set is itself a subalgebra is true for an arbitrary subgroup — for X, Y ∈ 𝔨 the subgroup generated by the two one-parameter subgroups is arcwise connected, hence an immersed Lie subgroup of K whose Lie algebra contains X + Y and ⁅X, Y⁆ — but that argument is the subalgebra ↔ immersed-subgroup correspondence, which the roadmap schedules two layers later (Layer 4, exists_immersedLieSubgroup_lieSubalgebra) and which is not available here.

What is available without it is the closed case: only the scalar closure survives with no topological hypothesis, since both the Trotter formula and the difference quotient produce the new element as a limit of elements of K, never as an element of K on the nose. TauCeti.Lie.isClosed_setOf_forall_lieExp_smul_mem turns those limits back into membership, and it is the only place closedness is used. So for a closed K the generation collapses (TauCeti.Lie.coe_lieSubalgebraOfSubgroup), which is the hypothesis under which the next Layer 2 target — the closed-subgroup theorem, promoting K to an embedded Lie subgroup with Lie(K) = 𝔨 — is stated.

Main definitions

• TauCeti.Lie.lieSubalgebraOfSubgroup: the Lie algebra of a subgroup.

Main results

• TauCeti.Lie.lieExp_smul_add_mem, TauCeti.Lie.lieExp_smul_smul_mem and TauCeti.Lie.lieExp_smul_lie_mem: the three closure properties, stated on the defining condition itself so that they can be used without producing the bundled subalgebra.
• TauCeti.Lie.hasDerivAt_Ad_lieExp_smul_apply_zero: the adjoint orbit s ↦ Ad (lieExp (s • X)) Y has derivative ⁅X, Y⁆ at the origin. This is the derivation-level infinitesimal adjoint, the analytic input to bracket closure.
• TauCeti.Lie.finiteDimensional_lieSubalgebraOfSubgroup: finite-dimensional subgroup models.
• TauCeti.Lie.lieSubalgebraOfSubgroup_le_iff: the universal property of the generated subalgebra, for an arbitrary subgroup.
• TauCeti.Lie.lieSubalgebraOfSubgroup_induction: induction on the generated subalgebra, for an arbitrary subgroup.
• TauCeti.Lie.mem_lieSubalgebraOfSubgroup and TauCeti.Lie.coe_lieSubalgebraOfSubgroup: for a closed subgroup, the Lie algebra of K is exactly 𝔨.
• TauCeti.Lie.isClosed_setOf_forall_lieExp_smul_mem: the candidate Lie algebra is a closed subset of 𝔤.
• TauCeti.Lie.Ad_mem_lieSubalgebraOfSubgroup: the Lie algebra of K is invariant under the adjoint action of the normalizer of K.
• TauCeti.Lie.lieSubalgebraOfSubgroup_le_comap_Ad_sub_id: for g in the normalizer of K, Ad g - 1 maps Lie(K) into itself, in the form that Submodule.mapQ consumes.
• TauCeti.Lie.lieSubalgebraOfSubgroup_inf: for closed subgroups, the Lie algebra of an intersection is the intersection of the Lie algebras.
• TauCeti.Lie.lieSubalgebraOfSubgroup_map_conj: the Lie algebra of a conjugate of a subgroup is the adjoint image of its Lie algebra.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 2, "The Lie subalgebra of a subgroup".
• J. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups, Springer (2012), Section 9.1.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Theorem 20.12.

The three closure properties

theorem TauCeti.Lie.lieExp_smul_zero_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] (K : Subgroup G) (t : ℝ) : lieExp (t • 0) ∈ K

The zero derivation generates the trivial one-parameter subgroup, which lies in every subgroup.

theorem TauCeti.Lie.lieExp_smul_smul_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {X : LeftInvariantDerivation I G} (hX : ∀ (t : ℝ), lieExp (t • X) ∈ K) (c t : ℝ) : lieExp (t • c • X) ∈ K

Scalar closure. Rescaling a derivation reparametrises its one-parameter subgroup, so the condition defining the Lie algebra of a subgroup is invariant under scalars. No hypothesis on the subgroup is needed.

theorem TauCeti.Lie.lieExp_smul_add_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) {X Y : LeftInvariantDerivation I G} (hX : ∀ (t : ℝ), lieExp (t • X) ∈ K) (hY : ∀ (t : ℝ), lieExp (t • Y) ∈ K) (t : ℝ) : lieExp (t • (X + Y)) ∈ K

Additive closure, from the Trotter product formula: lieExp (t • (X + Y)) is the limit of the powers (lieExp ((t / n) • X) * lieExp ((t / n) • Y)) ^ n, each of which lies in K, so a closed K contains the limit.

theorem TauCeti.Lie.isClosed_setOf_forall_lieExp_smul_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) : IsClosed {X : LeftInvariantDerivation I G | ∀ (t : ℝ), lieExp (t • X) ∈ K}

The candidate Lie algebra of a closed subgroup is closed. It is an intersection over the time parameter of preimages of K under the continuous maps X ↦ lieExp (t • X).

theorem TauCeti.Lie.lieExp_smul_Ad_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑K) {Y : LeftInvariantDerivation I G} (hY : ∀ (t : ℝ), lieExp (t • Y) ∈ K) (t : ℝ) : lieExp (t • (Ad g) Y) ∈ K

The adjoint action of an element of the normalizer of K preserves the defining condition: conjugating the one-parameter subgroup of Y by g ∈ N(K) is the one-parameter subgroup of Ad g Y, and stays inside K.

The derivative of the adjoint orbit

theorem TauCeti.Lie.hasDerivAt_Ad_lieExp_smul_apply_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] (X Y : LeftInvariantDerivation I G) : HasDerivAt (fun (s : ℝ) => (Ad (lieExp (s • X))) Y) ⁅X, Y⁆ 0

The infinitesimal adjoint, on derivations. The adjoint orbit s ↦ Ad (lieExp (s • X)) Y has derivative ⁅X, Y⁆ at s = 0.

This is TauCeti.Lie.hasDerivAt_tangentAd_mulInvariantExp_smul_apply_zero, the same statement for the tangent space at the identity, transported across the canonical isometric identification TauCeti.Lie.leftInvariantDerivationLinearIsometryEquivModelVectorSpace of LeftInvariantDerivation I G with the model space E. Bracket closure below is the only consumer so far: it is what makes ⁅X, Y⁆ a limit of difference quotients of a curve in 𝔨.

Bracket closure

theorem TauCeti.Lie.lieExp_smul_lie_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) {X Y : LeftInvariantDerivation I G} (hX : ∀ (t : ℝ), lieExp (t • X) ∈ K) (hY : ∀ (t : ℝ), lieExp (t • Y) ∈ K) (t : ℝ) : lieExp (t • ⁅X, Y⁆) ∈ K

Bracket closure. The curve s ↦ Ad (lieExp (s • X)) Y takes its values in the candidate Lie algebra of K, starts at Y and has derivative ⁅X, Y⁆ at s = 0; its difference quotients therefore lie in the linear span, and the bracket is their limit.

The Lie subalgebra

noncomputable def TauCeti.Lie.lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] (K : Subgroup G) : LieSubalgebra ℝ (LeftInvariantDerivation I G)

The Lie algebra of a subgroup. For a subgroup K of a Lie group G, the Lie subalgebra of 𝔤 generated by the derivations whose one-parameter subgroup lies entirely in K. It is the candidate Lie K, identified with the honest Lie algebra of K by the closed-subgroup theorem.

The generating set is itself a Lie subalgebra — for a closed K this is coe_lieSubalgebraOfSubgroup below, and for an arbitrary K it is a Layer 4 statement not available here — so generating is inert; it is what makes the definition total in K. See the module docstring.

instance TauCeti.Lie.finiteDimensional_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] (K : Subgroup G) : FiniteDimensional ℝ ↥(lieSubalgebraOfSubgroup K).toSubmodule

The model given by the Lie algebra of a subgroup is finite-dimensional.

theorem TauCeti.Lie.mem_lieSubalgebraOfSubgroup_of_forall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {X : LeftInvariantDerivation I G} (hX : ∀ (t : ℝ), lieExp (t • X) ∈ K) : X ∈ lieSubalgebraOfSubgroup K

A derivation whose one-parameter subgroup lies in K lies in the Lie algebra of K. This direction needs no hypothesis on K.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_le_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {L : LieSubalgebra ℝ (LeftInvariantDerivation I G)} : lieSubalgebraOfSubgroup K ≤ L ↔ ∀ (X : LeftInvariantDerivation I G), (∀ (t : ℝ), lieExp (t • X) ∈ K) → X ∈ L

The universal property of the Lie algebra of a subgroup. It is the least Lie subalgebra containing every derivation whose one-parameter subgroup lies in K, so a Lie subalgebra contains it as soon as it contains those derivations. No hypothesis on K is needed; together with mem_lieSubalgebraOfSubgroup_of_forall this is the elimination rule for an arbitrary subgroup.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_induction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {p : (X : LeftInvariantDerivation I G) → X ∈ lieSubalgebraOfSubgroup K → Prop} (mem : ∀ (X : LeftInvariantDerivation I G) (h : ∀ (t : ℝ), lieExp (t • X) ∈ K), p X ⋯) (zero : p 0 ⋯) (add : ∀ (X Y : LeftInvariantDerivation I G) (hX : X ∈ lieSubalgebraOfSubgroup K) (hY : Y ∈ lieSubalgebraOfSubgroup K), p X hX → p Y hY → p (X + Y) ⋯) (smul : ∀ (c : ℝ) (X : LeftInvariantDerivation I G) (hX : X ∈ lieSubalgebraOfSubgroup K), p X hX → p (c • X) ⋯) (lie : ∀ (X Y : LeftInvariantDerivation I G) (hX : X ∈ lieSubalgebraOfSubgroup K) (hY : Y ∈ lieSubalgebraOfSubgroup K), p X hX → p Y hY → p ⁅X, Y⁆ ⋯) {X : LeftInvariantDerivation I G} (hX : X ∈ lieSubalgebraOfSubgroup K) : p X hX

Induction on the Lie algebra of a subgroup. A property that holds for every derivation whose one-parameter subgroup lies in K and for 0, and is preserved by addition, scalar multiplication and the bracket, holds on all of Lie(K). This is LieSubalgebra.lieSpan_induction for the generating set, exposed across the module boundary, where the definition does not unfold.

@[simp]

theorem TauCeti.Lie.mem_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) {X : LeftInvariantDerivation I G} : X ∈ lieSubalgebraOfSubgroup K ↔ ∀ (t : ℝ), lieExp (t • X) ∈ K

The Lie algebra of a closed subgroup is exactly 𝔨: the three closure properties make the defining condition a Lie subalgebra, so generating it adds nothing.

theorem TauCeti.Lie.coe_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) : ↑(lieSubalgebraOfSubgroup K) = {X : LeftInvariantDerivation I G | ∀ (t : ℝ), lieExp (t • X) ∈ K}

The Lie algebra of a closed subgroup is exactly 𝔨, as sets.

theorem TauCeti.Lie.lieExp_smul_mem_of_mem_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) {X : LeftInvariantDerivation I G} (hX : X ∈ lieSubalgebraOfSubgroup K) (t : ℝ) : lieExp (t • X) ∈ K

The one-parameter subgroup generated by an element of the Lie algebra of a closed subgroup K lies in K.

theorem TauCeti.Lie.lieExp_mem_of_mem_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) {X : LeftInvariantDerivation I G} (hX : X ∈ lieSubalgebraOfSubgroup K) : lieExp X ∈ K

The exponential of an element of the Lie algebra of a closed subgroup K lies in K.

theorem TauCeti.Lie.isClosed_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (hK : IsClosed ↑K) : IsClosed ↑(lieSubalgebraOfSubgroup K)

The Lie algebra of a closed subgroup is a closed subset of 𝔤. This is what makes the closed-subgroup theorem's complement argument available: 𝔨 is a closed linear subspace of a finite-dimensional space, hence has a linear complement on which the exponential is transverse.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K K' : Subgroup G} (h : K ≤ K') : lieSubalgebraOfSubgroup K ≤ lieSubalgebraOfSubgroup K'

Monotonicity. A larger subgroup has a larger Lie algebra.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_inf {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K K' : Subgroup G} (hK : IsClosed ↑K) (hK' : IsClosed ↑K') : lieSubalgebraOfSubgroup (K ⊓ K') = lieSubalgebraOfSubgroup K ⊓ lieSubalgebraOfSubgroup K'

The Lie algebra of an intersection is the intersection of the Lie algebras. For closed subgroups both sides say that the one-parameter subgroup of X lies in each factor, so the statement is an interchange of the two quantifiers. Closedness is what collapses each generated subalgebra to that defining condition; without it only ≤ is available, from lieSubalgebraOfSubgroup_mono. This is how a subgroup cut out by two independent conditions — such as the special unitary group, unitary and of determinant one — has its Lie algebra computed one condition at a time.

@[simp]

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] : lieSubalgebraOfSubgroup ⊤ = ⊤

The Lie algebra of the whole group is the whole Lie algebra.

theorem TauCeti.Lie.Ad_mem_lieSubalgebraOfSubgroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑K) {X : LeftInvariantDerivation I G} (hX : X ∈ lieSubalgebraOfSubgroup K) : (Ad g) X ∈ lieSubalgebraOfSubgroup K

The Lie algebra of K is invariant under the adjoint action of the normalizer of K. Conjugating by g ∈ N(K) carries the one-parameter subgroup of X to the one of Ad g X, which therefore also stays in K. This is the bundled form of lieExp_smul_Ad_mem, the statement that makes the adjoint orbit of the bracket proof run inside 𝔨. No hypothesis on K is needed: Ad g is an automorphism of 𝔤 preserving the generating set, hence preserves the subalgebra it generates.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_le_comap_Ad_sub_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑K) : (lieSubalgebraOfSubgroup K).toSubmodule ≤ Submodule.comap (↑(Ad g).toLinearEquiv - LinearMap.id) (lieSubalgebraOfSubgroup K).toSubmodule

Ad g - 1 preserves the Lie algebra of K for g ∈ N(K), in the form that lets it descend to the quotient 𝔤 ⧸ Lie(K) through Submodule.mapQ.

theorem TauCeti.Lie.lieSubalgebraOfSubgroup_map_conj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] {K : Subgroup G} (g : G) : lieSubalgebraOfSubgroup (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) K) = LieSubalgebra.map (Ad g).toLieHom (lieSubalgebraOfSubgroup K)

The Lie algebra of a conjugate of a subgroup is the adjoint image of its Lie algebra.