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.

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. The unoriented presentation is likewise a later quotient by orientation-reversing reparametrizations, rather than a second bundled embedding type.

The first concrete presentations are the great circles of a unit sphere: a linear isometry ι : ℂ →ₗᵢ[ℝ] E carries the standard circle onto the great circle of the sphere of E cut out by the plane ι ℂ, and the resulting smooth embedding TauCeti.SmoothCircleEmbedding.greatCircle ι is a smooth circle presentation. The unknot is the great circle of S³ ⊆ ℝ⁴ cut out by the first coordinate plane, with the orientation of the standard circle.

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.
• TauCeti.SmoothCircleEmbedding.greatCircle: the great circle cut out of a unit sphere by a linear isometric copy of the complex plane.
• TauCeti.unknot: the unknot in S³, the great circle of the first coordinate plane of ℝ⁴ (TauCeti.unknot_eq_greatCircle).

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.

@[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.

@[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.

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.

@[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.

@[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.

@[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⁻¹.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.reverse_transDiffeomorph {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] {P : Type u_4} [TopologicalSpace P] [ChartedSpace H P] [IsManifold I (↑⊤) P] (f : SmoothCircleEmbedding I M) (e : Diffeomorph I I M P ↑⊤) : reverse (SmoothEmbedding.transDiffeomorph f e) = SmoothEmbedding.transDiffeomorph f.reverse e

Ambient transport commutes with orientation reversal of a smooth circle presentation.

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.

noncomputable def TauCeti.SmoothCircleEmbedding.greatCircle {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (ι : ℂ →ₗᵢ[ℝ] E) : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)

The great circle of the unit sphere of E cut out by a linear isometric copy ι : ℂ →ₗᵢ[ℝ] E of the complex plane, parametrized by the standard circle through ι.

@[simp]

theorem TauCeti.SmoothCircleEmbedding.coe_greatCircle_apply {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (ι : ℂ →ₗᵢ[ℝ] E) (z : Circle) : ↑((greatCircle ι) z) = ι ↑z

A great circle sends a point z of the standard circle to ι z.

The unknot

noncomputable def TauCeti.complexToEuclideanFour : ℂ →ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)

The standard isometric inclusion of the complex plane into ℝ⁴ as the first coordinate plane, z ↦ (Re z, Im z, 0, 0).

@[simp]

theorem TauCeti.complexToEuclideanFour_apply (z : ℂ) : complexToEuclideanFour z = z.re • EuclideanSpace.single 0 1 + z.im • EuclideanSpace.single 1 1

theorem TauCeti.complexProdToEuclideanFour_toLp_zero (z : ℂ) : complexProdToEuclideanFour (WithLp.toLp 2 (z, 0)) = complexToEuclideanFour z

The first coordinate plane of ℝ⁴ is the image of the first factor of ℂ² under TauCeti.complexProdToEuclideanFour.

noncomputable def TauCeti.unknot : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) ↑(Metric.sphere 0 1)

The unknot in S³: the great circle cut out by the first coordinate plane of ℝ⁴, with the orientation of the standard circle.

theorem TauCeti.unknot_eq_greatCircle : unknot = SmoothCircleEmbedding.greatCircle complexToEuclideanFour

The unknot is the great circle cut out by the first coordinate plane of ℝ⁴.

@[simp]

theorem TauCeti.coe_unknot_apply (z : Circle) : ↑(unknot z) = (↑z).re • EuclideanSpace.single 0 1 + (↑z).im • EuclideanSpace.single 1 1

The unknot sends a point z of the standard circle to (Re z, Im z, 0, 0).