The tautological action of the diffeomorphism group

The self-diffeomorphism group M ≃ₘ^n⟮I, I⟯ M acts on the underlying manifold by evaluation: φ • x = φ x. This file records that action, its faithfulness, and continuity in the point.

The action formalization mirrors Mathlib's Homeomorph.applyMulAction (Mathlib.Topology.Algebra.ConstMulAction, added in Kim Morrison's mathlib4#40135), which generalizes Equiv.Perm.applyMulAction.

The evaluation action and the forgetful homomorphism Diff(M) → Homeomorph(M) are the basic API relating the abstract group Diff(M) to the space it acts on: faithfulness identifies a diffeomorphism with the permutation of M it induces, and continuity in the point records that each diffeomorphism acts by a homeomorphism.

Main definitions

• Diffeomorph.applyMulAction: the MulAction (M ≃ₘ^n⟮I, I⟯ M) M with φ • x = φ x.
• Diffeomorph.applyFaithfulSMul: the action is faithful.
• Diffeomorph.applyContinuousConstSMul: each diffeomorphism acts continuously.
• Diffeomorph.applySubgroupContinuousConstSMul: subgroups inherit continuity in the point.

Main statements

• Diffeomorph.isFixedPt_zpow_iff_minimalPeriod_dvd: a point is fixed by f ^ k exactly when its minimal period under f divides k.
• Diffeomorph.exists_zpow_apply_eq_iff: the orbit of a periodic point under the integer powers of f consists of its iterates below the minimal period.

@[instance_reducible]

instance Diffeomorph.applyMulAction {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : MulAction (Diffeomorph I I M M n) M

The tautological action of the self-diffeomorphism group on the manifold by evaluation.

@[simp]

theorem Diffeomorph.smul_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (f : Diffeomorph I I M M n) (x : M) : f • x = f x

The tautological action of M ≃ₘ^n⟮I, I⟯ M on M is given by evaluation.

@[simp]

theorem Diffeomorph.toPermHom_eq_toPerm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : MulAction.toPermHom (Diffeomorph I I M M n) M = toPerm

The action homomorphism of the tautological diffeomorphism action is the forgetful homomorphism to permutations.

theorem Diffeomorph.isFixedPt_zpow_iff_minimalPeriod_dvd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (f : Diffeomorph I I M M n) (x : M) (k : ℤ) : Function.IsFixedPt (⇑(f ^ k)) x ↔ ↑(Function.minimalPeriod (⇑f) x) ∣ k

A point x is a fixed point of the power f ^ k of a self-diffeomorphism exactly when the minimal period of x under f divides k.

theorem Diffeomorph.exists_zpow_apply_eq_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {f : Diffeomorph I I M M n} {x : M} (hx : x ∈ Function.periodicPts ⇑f) {y : M} : (∃ (k : ℤ), (f ^ k) x = y) ↔ ∃ j < Function.minimalPeriod (⇑f) x, (⇑f)^[j] x = y

For a periodic point x of a self-diffeomorphism f, the points (f ^ k) x with k ∈ ℤ are the iterates f^[j] x with j below the least period of x.

instance Diffeomorph.applyFaithfulSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : FaithfulSMul (Diffeomorph I I M M n) M

The tautological action of M ≃ₘ^n⟮I, I⟯ M on M is faithful.

instance Diffeomorph.applyContinuousConstSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : ContinuousConstSMul (Diffeomorph I I M M n) M

The action of each self-diffeomorphism on M is continuous.

@[reducible, inline]

abbrev Diffeomorph.applySubgroupContinuousConstSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (G : Subgroup (Diffeomorph I I M M n)) : ContinuousConstSMul (↥G) M

A subgroup of the self-diffeomorphism group acts continuously on M in the point, by the generic subgroup transfer for ContinuousConstSMul.