$\mathrm{Diff}^r(M)$ and its (weak) $C^r$ topology

Definition

ClosingLemma_DiffeoCrTopology

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-topologydynamical-systemsmanifolds

Let $M$ be a smooth manifold modelled on $\mathbb R^n$ (without boundary) and let $r\ge 0$ be an integer. Write $\mathrm{Diff}^r(M)$ for the set of $C^r$ diffeomorphisms $g\colon M\to M$ .

For $f\in\mathrm{Diff}^r(M)$ , charts $(\varphi,U)$ and $(\psi,V)$ of the smooth structure of $M$ , a compact set $K\subseteq U$ with $f(K)\subseteq V$ , and $\varepsilon>0$ , the basic neighbourhood $\mathcal N^r(f;\varphi,\psi,K,\varepsilon)$ is the set of $g\in\mathrm{Diff}^r(M)$ such that

$g(K)\subseteq V$ , and
for every $x\in\varphi(K)$ and every $0\le k\le r$ ,

\big\|D^k(\psi\circ g\circ\varphi^{-1})(x)-D^k(\psi\circ f\circ\varphi^{-1})(x)\big\|<\varepsilon ,

where $D^k$ is the $k$ -th Fréchet derivative (a $k$ -linear map, with the operator norm).

The (weak) $C^r$ topology on $\mathrm{Diff}^r(M)$ is the topology generated by all such basic neighbourhoods. On a compact manifold it coincides with the strong (Whitney) $C^r$ topology. This is the topology in which "a $C^r$ -small perturbation of $f$ " is measured in the closing lemma.

Formalization Note $\mathrm{Diff}^r(M)$ is Diffeomorph (𝓡 n) (𝓡 n) M M r. Charts range over the maximal $C^\infty$ atlas IsManifold.maximalAtlas (𝓡 n) ∞ M. Local representatives are composed as total functions on $\mathbb R^n$ ; since $\varphi(K)$ lies in the open set $\varphi(U)$ and $g(K)\subseteq V$ , their derivatives at points of $\varphi(K)$ agree with those of the genuine local representative. The topology is a def (crTopology r) with a scoped instance, so it does not clash with other topologies on diffeomorphism groups.

Definition code

import Mathlib

/-!
# `C^r` diffeomorphisms of a closed manifold and the weak `C^r` topology

Setting for the Prove2Me mission "Closing lemma for `C^r` diffeomorphisms".

* `ClosingLemma.Diff n M r` : the space `Diff^r(M)` of `C^r` diffeomorphisms of a smooth
  manifold `M` modelled on `ℝⁿ` (no boundary).
* `ClosingLemma.crBasicNhd` : Hirsch's basic set `𝒩^r(f; (φ,U), (ψ,V), K, ε)`.
* `ClosingLemma.crTopology` : the weak (compact-open) `C^r` topology, generated by these sets
  (Hirsch, *Differential Topology*, Ch. 2, §1).  For compact `M` it coincides with the strong
  (Whitney) `C^r` topology.
-/

open scoped Manifold ContDiff Topology

namespace ClosingLemma

/-- `Diff^r(M)`: the `C^r` diffeomorphisms of a manifold `M` modelled on `ℝⁿ`
(boundaryless model `𝓡 n`). -/
abbrev Diff (n : ℕ) (M : Type*) [TopologicalSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (r : ℕ) :=
  Diffeomorph (𝓡 n) (𝓡 n) M M (r : WithTop ℕ∞)

variable {n : ℕ} {M : Type*} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M]

/-- Hirsch's basic set `𝒩^r(f; (φ,U), (ψ,V), K, ε)`: the diffeomorphisms `g` with
`g(K) ⊆ V = ψ.source` whose local representative `ψ ∘ g ∘ φ⁻¹` has all derivatives of order
`0, 1, …, r` within `ε` of those of `ψ ∘ f ∘ φ⁻¹` at every point of `φ(K)`. -/
def crBasicNhd (r : ℕ) (f : Diff n M r)
    (φ ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (K : Set M) (ε : ℝ) :
    Set (Diff n M r) :=
  {g | Set.MapsTo g K ψ.source ∧ ∀ x ∈ φ '' K, ∀ k ≤ r,
    ‖iteratedFDeriv ℝ k (ψ ∘ g ∘ φ.symm) x - iteratedFDeriv ℝ k (ψ ∘ f ∘ φ.symm) x‖ < ε}

/-- The admissible basic sets: `φ, ψ` are charts of the smooth structure of `M`,
`K ⊆ φ.source` is compact, `f(K) ⊆ ψ.source`, and `ε > 0`. -/
def crBasicNhds (r : ℕ) : Set (Set (Diff n M r)) :=
  {S | ∃ (f : Diff n M r) (φ ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
    (K : Set M) (ε : ℝ),
    φ ∈ IsManifold.maximalAtlas (𝓡 n) ∞ M ∧ ψ ∈ IsManifold.maximalAtlas (𝓡 n) ∞ M ∧
    IsCompact K ∧ K ⊆ φ.source ∧ Set.MapsTo f K ψ.source ∧ 0 < ε ∧
    S = crBasicNhd r f φ ψ K ε}

/-- The weak `C^r` topology on `Diff^r(M)`, generated by the basic sets `crBasicNhds r`. -/
abbrev crTopology (r : ℕ) : TopologicalSpace (Diff n M r) :=
  TopologicalSpace.generateFrom (crBasicNhds r)

scoped instance (r : ℕ) : TopologicalSpace (Diff n M r) := crTopology r

end ClosingLemma

Source

M. W. Hirsch, Differential Topology, Springer GTM 33, Chapter 2, Section 1 (the weak/compact-open C^r topology, basic neighbourhoods N^r(f; (φ,U), (ψ,V), K, ε)); Diff^r(M) as in Open Problem Garden, "Closing Lemma for Diffeomorphism (Dynamical Systems)", posted by Jailton Viana, April 24th, 2013, https://www.openproblemgarden.org/op/closing_lemma_for_diffeomorphism_dynamical_systems (the boxed Conjecture; bibliography: Bonatti–Díaz–Viana, Dynamics beyond uniform hyperbolicity, Encyclopaedia of Mathematical Sciences vol. 102, Springer 2005)

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Diffr(M)\mathrm{Diff}^r(M)Diffr(M) and its (weak) CrC^rCr topology

$\mathrm{Diff}^r(M)$ and its (weak) $C^r$ topology