The group of self-diffeomorphisms

Mathlib's Diffeomorph I I' M M' n is the type of Cⁿ diffeomorphisms between two manifolds, with composition (Diffeomorph.trans), inverse (Diffeomorph.symm), and the identity (Diffeomorph.refl) already in place. When the source and target coincide these assemble into a group: this file equips the self-diffeomorphisms M ≃ₘ^n⟮I, I⟯ M with One, Mul, and Inv instances and proves the Group axioms, exactly as Mathlib does for Equiv.Perm (Mathlib/Algebra/Group/End.lean). The multiplication is f * g = g.trans f, so that f * g acts as the function composition f ∘ g, matching the Equiv.Perm convention.

This is the group object the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md, layer 3, "diffeomorphism groups with the C^∞ topology") asks for as its first deliverable: "The group Diff(M) := M ≃ₘ^∞⟮I, I⟯ M under composition (the Group instance is routine from the existing Diffeomorph composition and inverse)." It is the underlying group of the topological group Diff(M) whose homotopy type the Smale conjecture [Kir97, Problem 4.34] is about; the C^∞ topology making it a topological group is a separate, later layer-3 deliverable, so this file stops at the bare group structure. The construction works for every smoothness exponent n, with n = ∞ the case named by the roadmap.

Main definitions

• TauCeti.Diff I M n: notation/abbreviation for the group M ≃ₘ^n⟮I, I⟯ M of Cⁿ self-diffeomorphisms of M.
• the One, Mul, Inv, and Group instances on M ≃ₘ^n⟮I, I⟯ M.
• Diffeomorph.toPerm: the forgetful group homomorphism to the underlying permutation group Equiv.Perm M, which is injective.
• Diffeomorph.toHomeomorphHom: the forgetful group homomorphism to the underlying homeomorphism group, which is injective.

Main results

• Diffeomorph.mul_apply / one_apply / inv_apply and the coe_* companions: the group operations act by composition, the identity, and the inverse diffeomorphism.

@[instance_reducible]

instance Diffeomorph.instOne {𝕜 : 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 ℕ∞} : One (Diffeomorph I I M M n)

The identity diffeomorphism is the unit of the self-diffeomorphism group.

Equations

• Diffeomorph.instOne = { one := Diffeomorph.refl I M n }

@[instance_reducible]

instance Diffeomorph.instMul {𝕜 : 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 ℕ∞} : Mul (Diffeomorph I I M M n)

Multiplication of self-diffeomorphisms is composition: f * g follows g then f, so that it acts as f ∘ g, matching the Equiv.Perm convention.

Equations

• Diffeomorph.instMul = { mul := fun (f g : Diffeomorph I I M M n) => g.trans f }

@[instance_reducible]

instance Diffeomorph.instInv {𝕜 : 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 ℕ∞} : Inv (Diffeomorph I I M M n)

The inverse in the self-diffeomorphism group is the inverse diffeomorphism.

Equations

• Diffeomorph.instInv = { inv := fun (f : Diffeomorph I I M M n) => f.symm }

theorem Diffeomorph.trans_assoc {𝕜 : 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 ℕ∞} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_7} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H' : Type u_8} [TopologicalSpace H'] {G : Type u_9} [TopologicalSpace G] {G' : Type u_10} [TopologicalSpace G'] {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F' G'} {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_12} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] (f : Diffeomorph I I' M M' n) (g : Diffeomorph I' J M' N n) (h : Diffeomorph J J' N N' n) : (f.trans g).trans h = f.trans (g.trans h)

Composition of diffeomorphisms is associative.

@[instance_reducible]

instance Diffeomorph.instGroup {𝕜 : 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 ℕ∞} : Group (Diffeomorph I I M M n)

The Cⁿ self-diffeomorphisms of M form a group under composition, with multiplication acting as function composition.

Equations

• One or more equations did not get rendered due to their size.

theorem Diffeomorph.one_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 ℕ∞} : 1 = Diffeomorph.refl I M n

The unit of the self-diffeomorphism group is the identity diffeomorphism.

theorem Diffeomorph.mul_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 g : Diffeomorph I I M M n) : f * g = g.trans f

Multiplication in the self-diffeomorphism group is Diffeomorph.trans in composition order.

theorem Diffeomorph.inv_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) : f⁻¹ = f.symm

Inversion in the self-diffeomorphism group is the inverse diffeomorphism.

@[simp]

theorem Diffeomorph.coe_one {𝕜 : 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 ℕ∞} : ⇑1 = id

The unit self-diffeomorphism coerces to the identity function.

@[simp]

theorem Diffeomorph.coe_mul {𝕜 : 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 g : Diffeomorph I I M M n) : ⇑(f * g) = ⇑f ∘ ⇑g

Multiplication of self-diffeomorphisms coerces to function composition.

@[simp]

theorem Diffeomorph.coe_inv {𝕜 : 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) : ⇑f⁻¹ = ⇑f.symm

The inverse self-diffeomorphism coerces to the inverse diffeomorphism.

@[simp]

theorem Diffeomorph.mul_apply {𝕜 : 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 g : Diffeomorph I I M M n) (x : M) : (f * g) x = f (g x)

Multiplication of self-diffeomorphisms acts by applying the right factor, then the left.

@[simp]

theorem Diffeomorph.one_apply {𝕜 : 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 ℕ∞} (x : M) : 1 x = x

The unit self-diffeomorphism fixes every point.

@[simp]

theorem Diffeomorph.inv_apply {𝕜 : 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.symm x

The inverse in the self-diffeomorphism group acts as the inverse diffeomorphism.

@[simp]

theorem Diffeomorph.toEquiv_one {𝕜 : 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 ℕ∞} : toEquiv 1 = 1

The underlying equivalence of the unit self-diffeomorphism is the unit permutation.

@[simp]

theorem Diffeomorph.toEquiv_mul {𝕜 : 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 g : Diffeomorph I I M M n) : (f * g).toEquiv = f.toEquiv * g.toEquiv

The underlying equivalence preserves multiplication of self-diffeomorphisms.

@[simp]

theorem Diffeomorph.toEquiv_inv {𝕜 : 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) : f⁻¹.toEquiv = f.toEquiv⁻¹

The underlying equivalence preserves inversion of self-diffeomorphisms.

def Diffeomorph.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 ℕ∞} : Diffeomorph I I M M n →* Equiv.Perm M

The forgetful group homomorphism from the self-diffeomorphism group to the permutation group of the underlying set, sending a diffeomorphism to its underlying equivalence.

Equations

• Diffeomorph.toPerm = { toFun := fun (f : Diffeomorph I I M M n) => f.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Diffeomorph.toPerm_apply {𝕜 : 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) : toPerm f = f.toEquiv

The forgetful homomorphism to permutations sends a diffeomorphism to its underlying equivalence.

theorem Diffeomorph.toPerm_injective {𝕜 : 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 ℕ∞} : Function.Injective ⇑toPerm

The forgetful homomorphism to permutations is injective.

def Diffeomorph.toHomeomorphHom {𝕜 : 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 ℕ∞} : Diffeomorph I I M M n →* M ≃ₜ M

The forgetful group homomorphism from self-diffeomorphisms to self-homeomorphisms.

Equations

• Diffeomorph.toHomeomorphHom = { toFun := fun (f : Diffeomorph I I M M n) => f.toHomeomorph, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Diffeomorph.toHomeomorphHom_apply {𝕜 : 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) : toHomeomorphHom f = f.toHomeomorph

The forgetful homomorphism to self-homeomorphisms sends a diffeomorphism to its underlying homeomorphism.

theorem Diffeomorph.toHomeomorphHom_injective {𝕜 : 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 ℕ∞} : Function.Injective ⇑toHomeomorphHom

The forgetful homomorphism to self-homeomorphisms is injective.

@[reducible, inline]

abbrev TauCeti.Diff {𝕜 : 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_5) [TopologicalSpace M] [ChartedSpace H M] (n : WithTop ℕ∞) : Type u_5

Diff I M n is the group of Cⁿ self-diffeomorphisms of the manifold M modelled on I, under composition. With n = ∞ this is the group underlying Diff(M) of the geometric-topology roadmap.

Equations

• TauCeti.Diff I M n = Diffeomorph I I M M n