Smooth circle presentations

The geometric presentation of an oriented knot in a manifold is a smooth embedding of the standard oriented circle into that manifold. This file specializes TauCeti.SmoothEmbedding to that source, without introducing a privileged Knot type, and supplies the two canonical kinds of reparametrization of the circle:

• rotation by a : Circle, which preserves the standard orientation;
• complex conjugation, which reverses it.

The rotations use Mathlib's smooth scalar-action diffeomorphisms for the analytic Lie group Circle; reflection is the smooth inversion map of that group. The resulting operations on TauCeti.SmoothCircleEmbedding are instances of the general source-reparametrization operation TauCeti.SmoothEmbedding.compDiffeomorph. In particular, they preserve the image and commute with transport by a diffeomorphism of the ambient manifold.

This is the first geometric presentation requested by layer 4 of the geometric-topology roadmap. A parametrization gives the image circle its orientation. A framing is deliberately not included here: defining a push-off as a framing requires the tubular-neighbourhood interface from layer 1. The unoriented presentation is likewise a later quotient by orientation-reversing reparametrizations, rather than a second bundled embedding type.

Main definitions

• TauCeti.circleRotationHom: the smooth rotation action of Circle on itself.
• TauCeti.circleReflection: complex conjugation as a self-diffeomorphism of Circle.
• TauCeti.SmoothCircleEmbedding: smooth embeddings of the standard circle into a manifold.
• TauCeti.SmoothCircleEmbedding.rotate: orientation-preserving reparametrization by a rotation.
• TauCeti.SmoothCircleEmbedding.reverse: orientation-reversing reparametrization by conjugation.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1.

noncomputable def TauCeti.circleRotationHom : Circle →* Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) Circle ↑⊤

Rotations of the complex unit circle, as smooth self-diffeomorphisms.

Equations

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

@[simp]

theorem TauCeti.circleRotationHom_apply_apply (a x : Circle) : (circleRotationHom a) x = a * x

A circle rotation acts by multiplication on the complex unit circle.

theorem TauCeti.circleRotationHom_injective : Function.Injective ⇑circleRotationHom

The homomorphism from circle rotations to circle diffeomorphisms is injective.

noncomputable def TauCeti.circleReflection : Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) Circle ↑⊤

Complex conjugation, as the orientation-reversing smooth self-diffeomorphism of the circle.

Equations

• TauCeti.circleReflection = { toEquiv := Equiv.inv Circle, contMDiff_toFun := TauCeti.circleReflection._proof_1✝, contMDiff_invFun := TauCeti.circleReflection._proof_1✝ }

@[simp]

theorem TauCeti.circleReflection_apply (x : Circle) : circleReflection x = x⁻¹

Reflection of the complex unit circle is inversion.

@[simp]

theorem TauCeti.circleReflection_mul_self : circleReflection * circleReflection = 1

Reflection of the circle is an involution.

@[simp]

theorem TauCeti.circleReflection_inv : circleReflection⁻¹ = circleReflection

Reflection is its own inverse as a circle diffeomorphism.

@[simp]

theorem TauCeti.circleReflection_mul_circleRotationHom (a : Circle) : circleReflection * circleRotationHom a = circleRotationHom a⁻¹ * circleReflection

Reflection conjugates rotation by a to rotation by a⁻¹.

@[reducible, inline]

abbrev TauCeti.SmoothCircleEmbedding {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Type u_3

A smooth circle presentation in a manifold modelled on I is a smooth embedding of the standard complex unit circle into the manifold. Its parametrization orients the image circle.

Equations

• TauCeti.SmoothCircleEmbedding I M = TauCeti.SmoothEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) I (↑⊤) Circle M

noncomputable def TauCeti.SmoothCircleEmbedding.rotate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (a : Circle) : SmoothCircleEmbedding I M

Reparametrize a smooth circle embedding by the orientation-preserving rotation x ↦ a * x. This changes the marked parametrization but not the oriented image.

Equations

• f.rotate a = TauCeti.SmoothEmbedding.compDiffeomorph f (TauCeti.circleRotationHom a)

@[simp]

theorem TauCeti.SmoothCircleEmbedding.rotate_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (a x : Circle) : (f.rotate a) x = f (a * x)

Rotating a smooth circle embedding precomposes its underlying map with multiplication on the circle.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.rotate_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) : f.rotate 1 = f

Rotation by 1 does not change a smooth circle embedding.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.rotate_rotate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (a b : Circle) : (f.rotate b).rotate a = f.rotate (b * a)

Successive rotations multiply their parameters.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.range_rotate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (a : Circle) : Set.range ⇑(f.rotate a) = Set.range ⇑f

Rotation does not change the image of a smooth circle embedding.

@[instance_reducible]

noncomputable instance TauCeti.SmoothCircleEmbedding.instMulActionCircle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] : MulAction Circle (SmoothCircleEmbedding I M)

Circle rotation acts on smooth circle embeddings by reparametrization.

Equations

• TauCeti.SmoothCircleEmbedding.instMulActionCircle = { smul := fun (a : Circle) (f : TauCeti.SmoothCircleEmbedding I M) => f.rotate a, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.SmoothCircleEmbedding.smul_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (a : Circle) (f : SmoothCircleEmbedding I M) : a • f = f.rotate a

The circle action on smooth circle embeddings is rotation of the source.

noncomputable def TauCeti.SmoothCircleEmbedding.reverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) : SmoothCircleEmbedding I M

Reverse the orientation of a smooth circle presentation by precomposing with complex conjugation.

Equations

• f.reverse = TauCeti.SmoothEmbedding.compDiffeomorph f TauCeti.circleReflection

@[simp]

theorem TauCeti.SmoothCircleEmbedding.reverse_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (x : Circle) : f.reverse x = f x⁻¹

Reversing a smooth circle presentation sends the parameter x to x⁻¹.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.reverse_reverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) : f.reverse.reverse = f

Reversing a smooth circle presentation twice gives the original presentation.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.range_reverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) : Set.range ⇑f.reverse = Set.range ⇑f

Orientation reversal does not change the image of a smooth circle embedding.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.reverse_rotate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : SmoothCircleEmbedding I M) (a : Circle) : (f.rotate a).reverse = f.reverse.rotate a⁻¹

Reversing after rotation by a is rotating the reversed presentation by a⁻¹.

instance TauCeti.SmoothCircleEmbedding.instSMulCommClassDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] : SMulCommClass (Diff I M ↑⊤) Circle (SmoothCircleEmbedding I M)

Ambient diffeomorphisms commute with rotation of a smooth circle presentation.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.reverse_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (e : Diff I M ↑⊤) (f : SmoothCircleEmbedding I M) : reverse (SmoothEmbedding.transDiffeomorph f e) = e • f.reverse

Ambient diffeomorphisms commute with orientation reversal of a smooth circle presentation.