Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Equal total degree does not classify maps from a disconnected domain

Statement refuted

For every closed oriented smooth m-manifold M, possibly disconnected, two maps M→Sm are homotopic if and only if their total degree, the sum of the signed degrees on the connected components, agrees. Counterexample: for m≥1 take M=Sm⊔Sm, let c be a constant map of Sm into Sm, and put f=id⁡⊔ c and g=c⊔id⁡. Both maps have total degree 1, but they are not homotopic.

Facts & Assumptions

Given: An integer m≥1, the closed oriented smooth manifold M=Sm⊔Sm with the orientation of each copy, the identity id⁡ of Sm and a constant map c:Sm→Sm (Euclidean spheres and closed balls as subspaces of Rn, Smooth manifolds and their smooth charts).

[F1]

The identity map of an oriented closed manifold has degree 1, while a constant map has degree 0: the identity has degree 1 by the cited composition proposition, and a constant map factors through a point and has empty regular fibre over any value other than its constant, so the regular-value formula gives degree 0 (Degree is multiplicative under composition, Regular-value formula for degree, Degree of a proper smooth map by compact-support cohomology).

[F2]

The total degree of a map on a disjoint union of closed oriented components is the sum of the degrees of its restrictions, and a homotopy of maps of M restricts on each component to a homotopy of the restrictions; degrees of proper smooth homotopic maps between closed oriented manifolds agree, and for continuous self-maps of a sphere homotopic maps have equal degree (Degree of a proper smooth map by compact-support cohomology, Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Degree is invariant under proper smooth homotopy, Degree is homotopy invariant and multiplicative under composition).

[F3]

The Hopf classification requires a connected domain, so it does not apply to M; the connectedness hypothesis is recorded as load-bearing (The Hopf degree theorem for oriented domains, Connectedness is needed for a single degree invariant).

Counterexample

technique · constructive
1.1F1F2givenconstruct

(Equal total degrees.) Let f=id⁡⊔c and g=c⊔id⁡ on M=Sm⊔Sm. The restrictions to the two components have degrees 1 and 0 in the first case and 0 and 1 in the second, so by [F2] both total degrees equal 1+0=1=0+1.

2.1F1F2step 1.1

(No homotopy exists.) Suppose H:M×I→Sm were a homotopy from f to g. Its restriction to the first copy Sm×I is a homotopy from id⁡ to c between continuous self-maps of the sphere; by the sphere homotopy invariance recorded in [F2], deg⁡(id⁡)=deg⁡(c), contradicting 1≠0 from [F1].

3.1F3step 2.1discharge-construct∎

There is therefore a closed oriented smooth m-manifold, namely Sm⊔Sm, and two maps on it whose total degrees agree but which are not homotopic; the total degree is not a complete invariant for disconnected domains, exactly as recorded in the connectedness remark.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources