Degree foundations and applications

Hatcher §2.2, printed pages 134–135. This milestone defines the integral degree of a self-map of a positive-dimensional sphere from the completed ordered sphere class, proves properties (a)–(g), and applies them to tangent vector fields and free group actions.

The construction deliberately uses the first-simplex-minus-second-simplex orientation from Example 2.23. Reflections are computed by exchanging those two simplices, so the roadmap does not depend on the deferred simplicial–singular comparison theorem.

All sixteen formalization leaves are formalized locally and complete.

Formalization progress

5 definitions · 11 results

16 fully proved

Homological degree

Definition89The ordered class orients ordinary sphere homology #✓fully proved

For n : ℕ with 0 < n, construct the integral isomorphism

noncomputable def Hatcher.Sphere.integralSphereHomologyIso
    (n : ℕ) (hn : 0 < n) :
    (((AlgebraicTopology.singularHomologyFunctor AddCommGrpCat n).obj
      (AddCommGrpCat.of ℤ)).obj (TopCat.sphere.{0} n)) ≅
      AddCommGrpCat.of ℤ

Its inverse is the ordinary fundamental class obtained from Hatcher.Simplex.doubleSimplexSphereFundamentalClass through the natural positive-degree comparison between reduced and ordinary homology. Record the class and prove that it is an isomorphism. The orientation must therefore be the completed ordered double-simplex orientation, not an arbitrary choice.

The named class is Hatcher.Sphere.integralSphereFundamentalClass. The theorem Hatcher.Sphere.integralSphereHomologyIso_inv identifies it exactly with the inverse of the displayed isomorphism, while Hatcher.Sphere.integralSphereFundamentalClass_isIso records that it is a generator. Thus the ordinary orientation retains the order of the two simplex summands used in Example 2.23.

Sources

Dependencies

Statement usesDefinition 88 (The double simplex is a sphere) · Definition 71 (Reduced and ordinary homology agree in positive degrees)

Used byTheorem 79 (Degree is the multiplier of the ordered sphere class) · Definition 94 (The ordered sphere class orients local homology)

Theorem79Degree is the multiplier of the ordered sphere class #✓fully proved

For 0 < n and f : TopCat.sphere.{0} n ⟶ TopCat.sphere.{0} n, define

noncomputable def Hatcher.Sphere.degree
    (n : ℕ) (hn : 0 < n)
    (f : TopCat.sphere.{0} n ⟶ TopCat.sphere.{0} n) : ℤ

by conjugating the induced endomorphism of ordinary integral homology through the ordered orientation isomorphism and evaluating the resulting endomorphism of ℤ at 1.

The main result is the source-facing class equation

theorem Hatcher.Sphere.integralSphereFundamentalClass_map ... :
  integralSphereFundamentalClass n hn ≫ H.map f =
    AddCommGrpCat.asHom (degree n hn f) ≫
      integralSphereFundamentalClass n hn

together with the equivalent characterization of the conjugated endomorphism. This fixes the sign convention used by every later node.

The implementation first defines Hatcher.Sphere.degreeEndomorphism in the order ℤ → Hₙ(Sⁿ;ℤ) → Hₙ(Sⁿ;ℤ) → ℤ, then defines Hatcher.Sphere.degree by evaluating it at 1. The theorem Hatcher.Sphere.degreeEndomorphism_eq_asHom identifies this endomorphism with multiplication by the degree, and the main theorem rewrites the same fact on the ordered fundamental class.

Sources

Dependencies

Statement usesDefinition 89 (The ordered class orients ordinary sphere homology)

Used byTheorem 80 (The formal properties of degree) · Theorem 81 (A sphere reflection has degree minus one) · Theorem 83 (A fixed-point-free sphere map has antipodal degree) · Theorem 85 (A nonsurjective sphere map has degree zero) · Theorem 92 (The finite-fiber pair map carries the global degree)

Theorem80The formal properties of degree #✓fully proved

Prove that sphere degree sends the identity to 1, is multiplicative under composition, and is invariant under homotopy. The unique main result is

theorem Hatcher.Sphere.degree_eq_one_or_neg_one_of_homotopyEquiv ... :
  degree n hn f = 1 ∨ degree n hn f = -1

for the forward map of a sphere self-homotopy-equivalence. Supporting lemmas must retain the categorical composition order used by TopCat and expose the integer multiplier rather than an unspecified automorphism of homology.

Do not formalize the converse “equal degree implies homotopic”; Hatcher postpones it to Corollary 4.25.

The supporting API records degree_id, degree_comp, and degree_eq_of_homotopy, together with their conjugated-endomorphism forms. For a self-homotopy-equivalence, the degrees of the forward and inverse maps multiply to one, yielding isUnit_degree_of_homotopyEquiv and the displayed main theorem. Homeomorphism specializations are also exposed for the later reflection and group-action calculations.

Sources

Dependencies

Statement usesTheorem 79 (Degree is the multiplier of the ordered sphere class)

Used byTheorem 82 (The antipodal map has degree determined by dimension) · Theorem 81 (A sphere reflection has degree minus one) · Theorem 83 (A fixed-point-free sphere map has antipodal degree) · Definition 90 (Degree gives a character of a sphere action) · Theorem 86 (A nonvanishing tangent field forces odd dimension) · Theorem 99 (A local homeomorphism has local degree plus or minus one)

Definition92A punctured sphere is Euclidean space #✓fully proved

For every p : TopCat.sphere.{0} n, construct a stereographic homeomorphism

noncomputable def Hatcher.Sphere.puncturedSphereHomeomorphEuclidean
    (n : ℕ) (p : TopCat.sphere.{0} n) :
    ({p}ᶜ : Set (TopCat.sphere.{0} n)) ≃ₜ EuclideanSpace ℝ (Fin n)

and publish the resulting contractibility of the punctured sphere. Reuse Mathlib's stereographic' and the project's existing sphere chart conventions; do not create a competing public sphere model.

Formalized in Hatcher/Sphere/PuncturedStereographic.lean. The construction uses the existing sphereULiftHomeomorph once, restricts it to the complements of the selected point and its raw-sphere image, and then applies Mathlib's stereographic chart. The public puncturedSphereContractibleSpace instance is transported across this exact homeomorphism.

Sources

Dependencies

Proof usesDefinition 91 (Stereographic models for hemispheres and the equator)

Used byTheorem 85 (A nonsurjective sphere map has degree zero) · Definition 94 (The ordered sphere class orients local homology)

Theorem85A nonsurjective sphere map has degree zero #✓fully proved

For 0 < n and f : TopCat.sphere.{0} n ⟶ TopCat.sphere.{0} n, prove

theorem Hatcher.Sphere.degree_eq_zero_of_not_surjective
    (hf : ¬ Function.Surjective f) :
    degree n hn f = 0

Choose a point outside the image, factor f through the punctured sphere, and use its contractibility to show that the induced top-dimensional homology map vanishes. The proof must identify the actual degree multiplier; merely showing that some abstract endomorphism is zero is not the final statement.

Formalized in Hatcher/Sphere/NonsurjectiveDegree.lean. The chosen missed point gives an explicit TopCat factorization through its complement. The published contractibility instance and positive-degree reduced-to-ordinary comparison make the intermediate ordinary homology object zero, so the conjugated integer endomorphism defining degree is literally the zero map.

Sources

Dependencies

Statement usesTheorem 79 (Degree is the multiplier of the ordered sphere class)

Proof usesDefinition 92 (A punctured sphere is Euclidean space) · Theorem 75 (Reduced homology of a contractible space vanishes)

Reflections and fixed points

Theorem77Swapping the double simplex negates its fundamental class #✓fully proved

Define the automorphism of Hatcher.Simplex.doubleSimplex n induced by exchanging its two standard-simplex summands. Its restrictions to the common ordered boundary must agree, so the map descends through the pushout.

Prove at chain level that the swap sends the first-simplex-minus-second- simplex cycle to its negative. The main result is the corresponding homology formula

theorem Hatcher.Simplex.doubleSimplexFundamentalClass_map_swap ... :
  doubleSimplexFundamentalClass R n ≫
      (Hatcher.Reduced.homologyFunctor R n).map
        (doubleSimplexSwapIso n).hom =
    -doubleSimplexFundamentalClass R n

with integral coefficients as the source-facing specialization.

The formalization constructs the pushout involution explicitly, proves its action on both canonical singular simplices, and establishes the negation formula first for the augmented chain cycle and then for its reduced-homology class. The result is coefficient-general in every abelian target category with the required coproducts.

Sources

Dependencies

Statement usesDefinition 66 (The ordered difference of the two simplices is a cycle) · Theorem 76 (The double-simplex difference generates reduced homology)

Used byTheorem 78 (Coordinate sign changes on the sphere)

Theorem78Coordinate sign changes on the sphere #✓fully proved

Construct a sphere homeomorphism that changes the signs of an arbitrary finite set of coordinates. Define the one-coordinate reflections and the all-coordinate antipodal homeomorphism as special cases, with composition formulas for disjoint or symmetric-difference sign sets.

For the final coordinate, prove that the sign change fixes the equator, exchanges the two closed hemispheres, and corresponds under Hatcher.Simplex.doubleSimplexIsoSphere to the double-simplex swap. The main compatibility result is

theorem Hatcher.Sphere.doubleSimplexSwap_isoSphere ... :
  (Hatcher.Simplex.doubleSimplexSwapIso n).hom ≫
      (Hatcher.Simplex.doubleSimplexIsoSphere n).hom =
    (Hatcher.Simplex.doubleSimplexIsoSphere n).hom ≫
      (coordinateReflectionIso n (Fin.last n)).hom

Formalized in Hatcher/Sphere/CoordinateSignChanges.lean and Hatcher/Singular/DoubleSimplexSphere.lean. Coordinate sign changes are restrictions of a coordinatewise linear isometry of Euclidean space, so their homeomorphism, composition, reflection, and antipodal laws share one model. The last-coordinate calculation is performed on the two explicit hemisphere parametrizations defining doubleSimplexIsoSphere, which proves the displayed compatibility as an equality of the actual TopCat morphisms.

Sources

Dependencies

Statement usesTheorem 77 (Swapping the double simplex negates its fundamental class) · Definition 88 (The double simplex is a sphere)

Used byTheorem 82 (The antipodal map has degree determined by dimension) · Theorem 81 (A sphere reflection has degree minus one) · Theorem 84 (Only the antipodal group acts freely on an even sphere)

Theorem81A sphere reflection has degree minus one #✓fully proved

For a unit normal vector v, define the Euclidean reflection of Sⁿ across the equatorial subsphere orthogonal to v. It fixes that equator pointwise and interchanges the two complementary hemispheres. For 0 < n, prove

theorem Hatcher.Sphere.degree_reflection ... :
  degree n hn (reflectionIso n v).hom = -1

Compute the last-coordinate reflection by transporting the double-simplex swap formula and its negation of the named class. Prove that an orthogonal change of coordinates carries an arbitrary unit normal to the last coordinate, then use conjugacy and multiplicativity of degree. Record every coordinate reflection as a specialization for the antipodal factorization.

Formalized in Hatcher/Sphere/ReflectionDegree.lean. The reflection is the restriction of Mathlib's orthogonal reflection in the complement of the normal line. It fixes the defined equator and exchanges its closed hemispheres. A Householder reflection carries an arbitrary unit normal to the final coordinate; the completed double-simplex orientation computes that coordinate reflection's degree, and the explicit orthogonal conjugacy transports the result to every normal vector. degree_coordinateReflection records the coordinate special case.

Sources

Dependencies

Statement usesTheorem 79 (Degree is the multiplier of the ordered sphere class) · Theorem 78 (Coordinate sign changes on the sphere)

Proof usesTheorem 80 (The formal properties of degree)

Used byTheorem 82 (The antipodal map has degree determined by dimension)

Theorem82The antipodal map has degree determined by dimension #✓fully proved

Factor the antipodal homeomorphism of Sⁿ into the n+1 coordinate reflections and prove, for 0 < n,

theorem Hatcher.Sphere.degree_antipodal ... :
  degree n hn (antipodalIso n).hom = (-1 : ℤ) ^ (n + 1)

The factorization must be an equality of the explicit coordinate sign-change maps, so multiplicativity of degree applies without an unspecified homotopic replacement.

Hatcher.Sphere.coordinateReflectionComposite composes a concrete ordered list of coordinate reflections, with the head reflection applied first. For a duplicate-free list it equals the sign change on exactly the listed coordinates. The theorem coordinateReflectionComposite_finRange therefore identifies the list of all n+1 coordinates with antipodalIso n before the degree calculation is performed.

Sources

Dependencies

Statement usesTheorem 78 (Coordinate sign changes on the sphere)

Proof usesTheorem 80 (The formal properties of degree) · Theorem 81 (A sphere reflection has degree minus one)

Used byTheorem 83 (A fixed-point-free sphere map has antipodal degree) · Theorem 86 (A nonvanishing tangent field forces odd dimension)

Theorem83A fixed-point-free sphere map has antipodal degree #✓fully proved

Let 0 < n and f : TopCat.sphere.{0} n ⟶ TopCat.sphere.{0} n. Under hf : ∀ x, f x ≠ x, construct Hatcher's homotopy obtained by normalizing

(1-t)f(x) - tx.

Prove that the unnormalized vector never vanishes, that normalization remains on the unit sphere, and that the endpoints are f and the antipodal map. The main source-facing conclusion is

theorem Hatcher.Sphere.degree_eq_neg_one_pow_of_fixedPointFree ... :
  degree n hn f = (-1 : ℤ) ^ (n + 1)

Formalized in Hatcher/Sphere/FixedPointFreeDegree.lean. Taking norms of a hypothetical zero of the unnormalized segment forces its two coefficients to agree and be nonzero, so scalar cancellation would make f(x)=x. This proves normalization is continuous on the whole cylinder. Its endpoints are the original map and the completed explicit antipodal isomorphism, and homotopy invariance transports the antipodal degree formula to f.

Sources

Dependencies

Statement usesTheorem 79 (Degree is the multiplier of the ordered sphere class)

Proof usesTheorem 80 (The formal properties of degree) · Theorem 82 (The antipodal map has degree determined by dimension)

Used byTheorem 84 (Only the antipodal group acts freely on an even sphere)

Tangent fields

Structure6Tangent vector fields and normalization #✓fully proved

Define Hatcher.Sphere.TangentVectorField n as a continuous ambient vector field on TopCat.sphere.{0} n whose value at x is orthogonal to x. Define TangentVectorField.Nonvanishing pointwise.

For a nonvanishing field, construct its normalized field and prove continuity, orthogonality, unit norm, and equality of its zero set with that of the original field. The representation must match Hatcher's ambient formula and must not introduce a tangent-bundle dependency.

Formalized in Hatcher/Sphere/TangentVectorField.lean. The public API also records the continuous ambient-point map, its unit norm, pointwise nonvanishing, and preservation of both the zero set and nonvanishing under normalization.

Sources

Dependencies

Used byTheorem 87 (A sphere has a nonvanishing tangent field exactly in odd dimension) · Definition 93 (Odd spheres have a nonvanishing tangent field) · Theorem 86 (A nonvanishing tangent field forces odd dimension)

Theorem86A nonvanishing tangent field forces odd dimension #✓fully proved

For 0 < n, normalize a nonvanishing tangent vector field and construct the continuous homotopy

(t,x) ↦ (cos(πt))x + (sin(πt))v(x)

from the identity of Sⁿ to the antipodal map. Orthogonality and unit norm must prove that the formula stays on the sphere. Comparing endpoint degrees then yields the main result

theorem Hatcher.Sphere.odd_of_nonvanishingTangentVectorField ... : Odd n

Formalized in Hatcher/Sphere/TangentFieldObstruction.lean. The supporting declaration identityHomotopyAntipodalOfNonvanishingTangentVectorField is the explicit cosine--sine homotopy; its norm calculation uses the normalized field's unit norm and its orthogonality to the ambient sphere point.

Sources

Dependencies

Statement usesStructure 6 (Tangent vector fields and normalization)

Proof usesTheorem 80 (The formal properties of degree) · Theorem 82 (The antipodal map has degree determined by dimension)

Used byTheorem 87 (A sphere has a nonvanishing tangent field exactly in odd dimension)

Definition93Odd spheres have a nonvanishing tangent field #✓fully proved

Given Odd n, pair the n+1 ambient coordinates and define Hatcher's quarter-turn field

(x₁,x₂,…,x₂ₖ₋₁,x₂ₖ) ↦ (-x₂,x₁,…,-x₂ₖ,x₂ₖ₋₁).

Construct

noncomputable def Hatcher.Sphere.nonvanishingTangentVectorFieldOfOdd ... :
  TangentVectorField n

and prove that it has unit norm, hence is nowhere zero. The construction must handle the coordinate reindexing explicitly and retain continuity as part of the bundled field.

Formalized in Hatcher/Sphere/OddTangentField.lean. The public oddSphereCoordinateEquiv and paired-coordinate equations expose the literal quarter-turn formula, while nonvanishingTangentVectorFieldOfOdd_nonvanishing proves the resulting field is nowhere zero.

Sources

Dependencies

Statement usesStructure 6 (Tangent vector fields and normalization)

Used byTheorem 87 (A sphere has a nonvanishing tangent field exactly in odd dimension)

Theorem87A sphere has a nonvanishing tangent field exactly in odd dimension #✓fully proved

Assemble the two directions of Hatcher's Theorem 2.28. For 0 < n, prove

theorem Hatcher.Sphere.exists_nonvanishingTangentVectorField_iff_odd ... :
  (∃ v : TangentVectorField n, v.Nonvanishing) ↔ Odd n

The forward direction must use the identity-to-antipodal homotopy and the oriented degree calculation. The reverse direction must return the explicit paired-coordinate field, not merely a classical existence proof.

Formalized in Hatcher/Sphere/TangentFieldParity.lean by assembling the completed degree obstruction with nonvanishingTangentVectorFieldOfOdd and its pointwise nonvanishing theorem.

Sources

Dependencies

Statement usesStructure 6 (Tangent vector fields and normalization)

Proof usesTheorem 86 (A nonvanishing tangent field forces odd dimension) · Definition 93 (Odd spheres have a nonvanishing tangent field)

Free actions

Definition90Degree gives a character of a sphere action #✓fully proved

For a group G, define

abbrev Hatcher.Sphere.SphereAction (G : Type*) [Group G] (n : ℕ) :=
  G →* (((TopCat.sphere.{0} n : TopCat) : Type) ≃ₜ
    ((TopCat.sphere.{0} n : TopCat) : Type))

and define freeness to mean that every nonidentity group element acts without a fixed point. For 0 < n, package the degrees of the acting homeomorphisms as the multiplicative character

noncomputable def Hatcher.Sphere.sphereActionDegreeHom ... : G →* ℤˣ

Prove that its underlying integer at g is the degree of ρ g. Also record an explicit multiplicative equivalence ℤˣ ≃* Multiplicative (ZMod 2).

Hatcher.Sphere.SphereAction.IsFree records the fixed-point condition without adding a separate topological-action layer. The theorem Hatcher.Sphere.sphereActionDegreeHom_coe identifies the chosen unit with the integer degree. The explicit inverse equivalence Hatcher.Sphere.intUnitsMulEquivZModTwo is built from the homomorphism z ↦ (-1)^z, with 1 ↦ 0 and -1 ↦ 1 recorded for downstream use.

Sources

Dependencies

Statement usesTheorem 80 (The formal properties of degree)

Used byTheorem 84 (Only the antipodal group acts freely on an even sphere)

Theorem84Only the antipodal group acts freely on an even sphere #✓fully proved

Let G be a nontrivial group, 0 < n, and Even n. Prove Hatcher's Proposition 2.29 in the exact classification form

theorem Hatcher.Sphere.exists_freeSphereAction_iff_mulEquiv_zmodTwo ... :
  (∃ ρ : SphereAction G n, ρ.IsFree) ↔
    Nonempty (G ≃* Multiplicative (ZMod 2))

For the forward implication, use freeness and the fixed-point-free degree formula to prove that the action's degree character is injective, then identify its image with the two integer units. For the reverse implication, transport the explicit free antipodal ℤ/2 action across the group equivalence. Include that action and its freeness as supporting declarations. Do not assume G is finite.

The supporting theorem Hatcher.Sphere.sphereActionDegreeHom_injective_of_free_even proves the character injective directly from freeness. The implementation also publishes Hatcher.Sphere.antipodalZModTwoAction and Hatcher.Sphere.antipodalZModTwoAction_isFree; the reverse implication of the main theorem transports this literal action through the supplied group equivalence.

Sources

Dependencies

Statement usesTheorem 78 (Coordinate sign changes on the sphere) · Definition 90 (Degree gives a character of a sphere action)

Proof usesTheorem 83 (A fixed-point-free sphere map has antipodal degree)

Boundary

This milestone stops after Proposition 2.29. Local degree and Proposition 2.30 continue in the separate local-degree milestone. Examples 2.31–2.32, suspension invariance, cellular homology, the Hopf converse, and Theorem 2.27 remain deferred.