The zero-sphere

The unit sphere of a one-dimensional real normed space consists of a point p on it and its antipode -p. It is therefore finite and discrete, and its path components are its two points: the component of -p is the only path component other than that of p.

These are the inputs for the degree-zero computation of the reduced homology of spheres, which is the base case of the induction on dimension through the suspension isomorphism.

Main results

• TauCeti.sphere_eq_pair_of_finrank_eq_one: the unit sphere is {p, -p}.
• TauCeti.discreteTopology_sphere_of_finrank_eq_one: the unit sphere is discrete.
• TauCeti.zerothHomotopySphereUnique: the path component of -p is the unique path component other than that of p.

theorem TauCeti.sphere_eq_pair_of_finrank_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) {p : E} (hp : p ∈ Metric.sphere 0 1) : Metric.sphere 0 1 = {p, -p}

The unit sphere of a one-dimensional real normed space consists of a point on it and its antipode.

theorem TauCeti.finite_sphere_of_finrank_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) : Finite ↑(Metric.sphere 0 1)

The unit sphere of a one-dimensional real normed space is finite.

theorem TauCeti.discreteTopology_sphere_of_finrank_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) : DiscreteTopology ↑(Metric.sphere 0 1)

The unit sphere of a one-dimensional real normed space is discrete.

theorem TauCeti.zerothHomotopy_mk_neg_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) : ZerothHomotopy.mk (-p) ≠ ZerothHomotopy.mk p

On the unit sphere of a one-dimensional real normed space, a point and its antipode lie in distinct path components.

@[instance_reducible]

def TauCeti.zerothHomotopySphereUnique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) : Unique { c : ZerothHomotopy ↑(Metric.sphere 0 1) // c ≠ ZerothHomotopy.mk p }

On the unit sphere of a one-dimensional real normed space, the path component of -p is the unique path component other than that of p.

Equations

• TauCeti.zerothHomotopySphereUnique h p = { default := ⟨ZerothHomotopy.mk (-p), ⋯⟩, uniq := ⋯ }

@[simp]

theorem TauCeti.zerothHomotopySphereUnique_default {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) : default = ⟨ZerothHomotopy.mk (-p), ⋯⟩