Sliceness does not depend on a parametrization given by a lift

Smooth and topological sliceness (TauCeti.IsSmoothlySlice, TauCeti.IsTopologicallySlice) are stated for a parametrized knot K : S¹ → Sⁿ, but they do not depend on the parametrization: if K' = K ∘ σ for a diffeomorphism σ of the circle given by a lift (below), then K' is slice exactly when K is. That every diffeomorphism of the circle is given by such a lift is not proved here. A slice disc Φ for K is reparametrized along with the knot, by a diffeomorphism D of the closed unit disc which is σ on the boundary circle: Φ ∘ D is a slice disc for K' (TauCeti.IsSmoothSliceDisc.comp_diffeomorph), so K' is slice exactly when K is (TauCeti.isSmoothlySlice_congr_diffeomorph).

For an orientation-preserving σ, given by a lift F, σ (Circle.exp x) = Circle.exp (F x) with F (x + 2π) = F x + 2π and F' > 0, the disc diffeomorphism is TauCeti.circleLiftDiscDiffeomorph, which interpolates radially between the identity near the centre and σ near the boundary. An orientation-reversing σ, with a lift satisfying F (x + 2π) = F x - 2π and F' < 0, is the reversal z ↦ z⁻¹ followed by an orientation-preserving diffeomorphism, and sliceness is invariant under reversal (TauCeti.isSmoothlySlice_reverse_iff).

Main results

• TauCeti.isSmoothlySlice_congr_lift, TauCeti.isTopologicallySlice_congr_lift: sliceness is invariant under reparametrization by an orientation-preserving diffeomorphism of the circle with a lift.
• TauCeti.isSmoothlySlice_congr_lift_of_deriv_neg, TauCeti.isTopologicallySlice_congr_lift_of_deriv_neg: the same for an orientation-reversing diffeomorphism of the circle with a lift.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 8, for slice knots.

Reparametrization by a diffeomorphism of the circle

theorem TauCeti.isSmoothlySlice_congr_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {K K' : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)} {σ : Circle → Circle} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (hσ : ∀ (x : ℝ), σ (Circle.exp x) = Circle.exp (F x)) (hK' : ∀ (z : Circle), K' z = K (σ z)) : IsSmoothlySlice K' ↔ IsSmoothlySlice K

Smooth sliceness does not depend on the parametrization. If σ is an orientation-preserving diffeomorphism of the circle with lift F, that is σ (Circle.exp x) = Circle.exp (F x) with F (x + 2π) = F x + 2π and F' > 0, then K ∘ σ is smoothly slice exactly when K is.

theorem TauCeti.isTopologicallySlice_congr_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {K K' : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)} {σ : Circle → Circle} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (hσ : ∀ (x : ℝ), σ (Circle.exp x) = Circle.exp (F x)) (hK' : ∀ (z : Circle), K' z = K (σ z)) : IsTopologicallySlice K' ↔ IsTopologicallySlice K

Topological sliceness does not depend on the parametrization. If σ is an orientation-preserving diffeomorphism of the circle with lift F, then K ∘ σ is topologically slice exactly when K is.

theorem TauCeti.isSmoothlySlice_congr_lift_of_deriv_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {K K' : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)} {σ : Circle → Circle} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x - 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hneg : ∀ (x : ℝ), deriv F x < 0) (hσ : ∀ (x : ℝ), σ (Circle.exp x) = Circle.exp (F x)) (hK' : ∀ (z : Circle), K' z = K (σ z)) : IsSmoothlySlice K' ↔ IsSmoothlySlice K

Smooth sliceness does not depend on the parametrization, orientation-reversing case. If σ is a diffeomorphism of the circle with a lift F satisfying F (x + 2π) = F x - 2π and F' < 0, then K ∘ σ is smoothly slice exactly when K is.

theorem TauCeti.isTopologicallySlice_congr_lift_of_deriv_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {K K' : SmoothCircleEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)} {σ : Circle → Circle} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x - 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hneg : ∀ (x : ℝ), deriv F x < 0) (hσ : ∀ (x : ℝ), σ (Circle.exp x) = Circle.exp (F x)) (hK' : ∀ (z : Circle), K' z = K (σ z)) : IsTopologicallySlice K' ↔ IsTopologicallySlice K

Topological sliceness does not depend on the parametrization, orientation-reversing case. If σ is a diffeomorphism of the circle with a lift F satisfying F (x + 2π) = F x - 2π and F' < 0, then K ∘ σ is topologically slice exactly when K is.