Smooth translations and diffeomorphisms from group actions

This file packages the action of an element of a group with a ContMDiffConstSMul instance as a self-diffeomorphism. Unlike Diffeomorph.smul, this construction does not require a manifold structure on the acting group or joint smoothness of the action. Smooth multiplication supplies the required smoothness of individual left translations via a self-action instance, as does smooth addition for additive translations.

Main declarations

• ContMDiffMul.contMDiffConstSMul: smooth multiplication gives smooth left translations.
• Diffeomorph.constSmul: the diffeomorphism given by a fixed element of a pointwise-smooth group action.

instance ContMDiffMul.contMDiffConstSMul {𝕜 : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] {n : WithTop ℕ∞} [ContMDiffMul I n G] : ContMDiffConstSMul I n G G

Smooth multiplication makes each left translation smooth.

instance ContMDiffAdd.contMDiffConstVAdd {𝕜 : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] {n : WithTop ℕ∞} [ContMDiffAdd I n G] : ContMDiffConstVAdd I n G G

Smooth addition makes each left translation smooth.

def Diffeomorph.constSmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] (n : WithTop ℕ∞) [ContMDiffConstSMul I n G M] (g : G) : Diffeomorph I I M M n

The diffeomorphism given by a fixed element of a pointwise Cⁿ group action. Its inverse is scalar multiplication by the inverse group element.

Equations

• Diffeomorph.constSmul I n g = { toEquiv := MulAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

def Diffeomorph.constVAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [AddGroup G] [AddAction G M] (n : WithTop ℕ∞) [ContMDiffConstVAdd I n G M] (g : G) : Diffeomorph I I M M n

The diffeomorphism given by a fixed element of a pointwise Cⁿ additive group action. Its inverse is addition by the negated group element.

Equations

• Diffeomorph.constVAdd I n g = { toEquiv := AddAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

@[simp]

theorem Diffeomorph.constSmul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] {n : WithTop ℕ∞} [ContMDiffConstSMul I n G M] (g : G) (x : M) : (constSmul I n g) x = g • x

Evaluating the diffeomorphism associated to a fixed group element agrees with its action.

@[simp]

theorem Diffeomorph.constVAdd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [AddGroup G] [AddAction G M] {n : WithTop ℕ∞} [ContMDiffConstVAdd I n G M] (g : G) (x : M) : (constVAdd I n g) x = g +ᵥ x

Evaluating the diffeomorphism associated to a fixed additive-group element agrees with its action.

@[simp]

theorem Diffeomorph.constSmul_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] {n : WithTop ℕ∞} [ContMDiffConstSMul I n G M] (g : G) (x : M) : (constSmul I n g).symm x = g⁻¹ • x

The inverse of the diffeomorphism associated to a fixed group element acts by its inverse.

@[simp]

theorem Diffeomorph.constVAdd_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [AddGroup G] [AddAction G M] {n : WithTop ℕ∞} [ContMDiffConstVAdd I n G M] (g : G) (x : M) : (constVAdd I n g).symm x = -g +ᵥ x

The inverse of the diffeomorphism associated to a fixed additive-group element acts by its negation.

theorem Diffeomorph.constSmul_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] {n : WithTop ℕ∞} [ContMDiffConstSMul I n G M] (g : G) : (constSmul I n g).symm = constSmul I n g⁻¹

Taking the inverse of a fixed-action diffeomorphism inverts the acting group element.

theorem Diffeomorph.constVAdd_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [AddGroup G] [AddAction G M] {n : WithTop ℕ∞} [ContMDiffConstVAdd I n G M] (g : G) : (constVAdd I n g).symm = constVAdd I n (-g)

Taking the inverse of a fixed-action diffeomorphism negates the acting additive-group element.