Smooth conjugation in a Lie group

This file packages conjugation by an element of a Lie group as a smooth self-diffeomorphism. The resulting map from the group to its group of smooth self-diffeomorphisms is a group homomorphism. Differentiating each conjugation diffeomorphism at the identity yields the group adjoint action developed in subsequent files.

Main definitions

• TauCeti.Lie.conjDiffeomorph: conjugation by g as a smooth diffeomorphism.
• TauCeti.Lie.conj: the conjugation homomorphism into smooth self-diffeomorphisms.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The group adjoint".

@[instance_reducible]

instance TauCeti.Lie.instTopologicalSpaceConjAct {G : Type u_4} [topG : TopologicalSpace G] : TopologicalSpace (ConjAct G)

The conjugation-action copy of a Lie group carries the original topology.

@[instance_reducible]

instance TauCeti.Lie.instChartedSpaceConjAct {H : Type u_3} [TopologicalSpace H] {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] : ChartedSpace H (ConjAct G)

The conjugation-action copy of a Lie group carries the original manifold charts.

theorem TauCeti.Lie.contMDiff_conj_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 * p.2 * p.1⁻¹

Conjugation is jointly C^n. The map (g, x) ↦ g * x * g⁻¹ on a Lie group is C^n as a map out of the product manifold; this is the manifold counterpart of IsTopologicalGroup.continuous_conj_prod.

instance TauCeti.Lie.instContMDiffSMulConjAct {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] : ContMDiffSMul I I n (ConjAct G) G

Conjugation is a smooth action of the conjugation-action copy of a Lie group on the group.

def TauCeti.Lie.conjDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] (g : G) : Diffeomorph I I G G n

Conjugation by g, sending x to g * x * g⁻¹, as a smooth self-diffeomorphism.

@[simp]

theorem TauCeti.Lie.conjDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] (g x : G) : (conjDiffeomorph g) x = g * x * g⁻¹

@[simp]

theorem TauCeti.Lie.conjDiffeomorph_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] (g x : G) : (conjDiffeomorph g).symm x = g⁻¹ * x * g

def TauCeti.Lie.conj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] : G →* Diff I G n

Smooth conjugation is a group homomorphism from G to its group of smooth self-diffeomorphisms.

@[simp]

theorem TauCeti.Lie.conj_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [topG : TopologicalSpace G] [chartsG : ChartedSpace H G] [Group G] {n : WithTop ℕ∞} [LieGroup I n G] (g : G) : conj g = conjDiffeomorph g