Mod-two comparison of integer degree

Arithmetic and topological wrappers connecting parity of an integer degree with its reduction in ZMod 2. The file provides cast/parity lemmas and comparison theorems for degreeOfIso and the oriented degree API. Native coefficient-reduction and sphere top-class constructions are supplied by the dedicated coefficient-reduction modules.

1. Arithmetic parity / cast bridges ℤ → ZMod 2

These are pure arithmetic facts about the mod-2 reduction ring hom Int.castRingHom (ZMod 2); they carry the entire "comparison" between the integer phrasing Odd z and the F₂ phrasing (z : ZMod 2) = 1. They are independent of all topology.

theorem SphereOddDegree.intCast_zmodTwo_eq_one_iff_odd (z : ℤ) : ↑z = 1 ↔ Odd z

The parity bridge. For an integer z, its reduction in ZMod 2 is 1 iff z is odd. This is the entire comparison content of Route A: it converts the F₂ statement (degree f : ZMod 2) = 1 into the integer statement Odd (degree f) and back.

theorem SphereOddDegree.intCast_zmodTwo_eq_zero_iff_even (z : ℤ) : ↑z = 0 ↔ Even z

For an integer z, its reduction in ZMod 2 is 0 iff z is even.

theorem SphereOddDegree.Odd.intCast_zmodTwo {z : ℤ} (h : Odd z) : ↑z = 1

Forward direction of the parity bridge: an odd integer reduces to 1.

theorem SphereOddDegree.odd_of_intCast_zmodTwo_eq_one {z : ℤ} (h : ↑z = 1) : Odd z

Backward direction of the parity bridge: an integer reducing to 1 is odd.

theorem SphereOddDegree.Even.intCast_zmodTwo {z : ℤ} (h : Even z) : ↑z = 0

An even integer reduces to 0.

theorem SphereOddDegree.even_of_intCast_zmodTwo_eq_zero {z : ℤ} (h : ↑z = 0) : Even z

An integer reducing to 0 is even.

theorem SphereOddDegree.intCast_zmodTwo_eq_zero_or_one (z : ℤ) : ↑z = 0 ∨ ↑z = 1

The mod-2 reduction of any integer is either 0 or 1.

theorem SphereOddDegree.intCast_zmodTwo_mul (z w : ℤ) : ↑(z * w) = ↑z * ↑w

Multiplicativity of the reduction. Reduction mod 2 is a ring hom, so it takes products to products. This is the algebraic shadow of degree multiplicativity degree (g ∘ f) = degree g * degree f.

theorem SphereOddDegree.intCast_zmodTwo_eq_one_of_eq_one_or_neg_one {z : ℤ} (h : z = 1 ∨ z = -1) : ↑z = 1

Conversion-free corollary. Any integer that is 1 or -1 reduces to 1 in ZMod 2. This applies directly to ±1 degrees (homeomorphisms, the antipodal map) without going through Odd.

1b. Parity equivalences and reversed cast bridges

These complete the elementary parity algebra needed by the ModTwoTopClassComparison branch, so that no downstream module has to re-prove it. They are pure arithmetic, independent of all topology.

theorem SphereOddDegree.odd_iff_intCast_zmodTwo_eq_one (z : ℤ) : Odd z ↔ ↑z = 1

Reversed form of the parity bridge: z is odd iff its reduction in ZMod 2 is 1. Convenient when the hypothesis is phrased as Odd z.

theorem SphereOddDegree.even_iff_intCast_zmodTwo_eq_zero (z : ℤ) : Even z ↔ ↑z = 0

Reversed form of the even cast bridge: z is even iff its reduction in ZMod 2 is 0.

theorem SphereOddDegree.odd_iff_not_even (z : ℤ) : Odd z ↔ ¬Even z

An integer is odd iff it is not even (project-local re-export of Int.not_even_iff_odd, in the Odd ↔ ¬ Even orientation).

theorem SphereOddDegree.not_even_iff_odd (z : ℤ) : ¬Even z ↔ Odd z

An integer fails to be even iff it is odd (project-local re-export of Int.not_even_iff_odd).

1c. Scalar action over ZMod 2

The algebraic shadow of the top-class fixed-point condition: in any ZMod 2 -module, a scalar fixes a nonzero vector iff the scalar is 1. This is exactly the step that turns f_* z = a • z with z ≠ 0 into a = 1, used by the top-homology scalar branch. It needs no one-dimensionality: ZMod 2 = {0, 1}.

theorem SphereOddDegree.zmodTwo_smul_eq_self_iff {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {x : M} (hx : x ≠ 0) (a : ZMod 2) : a • x = x ↔ a = 1

Scalar action over ZMod 2. For a nonzero vector x in a ZMod 2 -module, a • x = x iff a = 1. (The only other scalar is 0, which sends x to 0 ≠ x.)

2. Mod-2 reduction of the conditional degree (Route A)

We attach the parity statement to the genuine integer degree degreeOfIso e f by reducing it modulo 2. Every statement is conditional on a chosen identification e : SphereTopHomologyIso n, like the rest of the degree API.

theorem SphereOddDegree.degreeOfIso_intCast_zmodTwo_eq_one_iff_odd {n : ℕ} (e : SphereTopHomologyIso n) (f : C(Sphere n, Sphere n)) : ↑(degreeOfIso e f) = 1 ↔ Odd (degreeOfIso e f)

The mod-2 degree comparison theorem. The reduction of the integer degree to ZMod 2 equals 1 iff the integer degree is odd. This is the precise sense in which "(degree f : ZMod 2) = 1" and "Odd (degree f)" are interchangeable — the two phrasings of the final odd-degree theorem.

theorem SphereOddDegree.degreeOfIso_comp_intCast_zmodTwo {n : ℕ} (e : SphereTopHomologyIso n) (f g : C(Sphere n, Sphere n)) : ↑(degreeOfIso e (g.comp f)) = ↑(degreeOfIso e g) * ↑(degreeOfIso e f)

Multiplicativity of the mod-2 degree. The reduction of the degree of a composite is the product of the reductions. This descends degreeOfIso_comp through the reduction ring hom.

theorem SphereOddDegree.degreeOfIso_homeomorph_intCast_zmodTwo_eq_one {n : ℕ} (e : SphereTopHomologyIso n) (h : Sphere n ≃ₜ Sphere n) : ↑(degreeOfIso e ↑h) = 1

The mod-2 degree of a self-homeomorphism is 1 (its integer degree is ±1, hence odd).

theorem SphereOddDegree.degreeOfIso_antipodal_intCast_zmodTwo_eq_one {n : ℕ} (e : SphereTopHomologyIso n) : ↑(degreeOfIso e (antipodal n)) = 1

The mod-2 degree of the antipodal map is 1. This is the F₂ phrasing of the proved parity fact Odd (degree (antipodal n)), and the parity content of the classical value degree (antipodal n) = (-1)^(n+1) (which is ≡ 1 mod 2).

theorem SphereOddDegree.degreeOfIso_antipodal_intCast_zmodTwo_eq_neg_one_pow {n : ℕ} (e : SphereTopHomologyIso n) : ↑(degreeOfIso e (antipodal n)) = ↑((-1) ^ (n + 1))

Mod-2 agreement with the target value, in ZMod 2. The reduction of the antipodal degree equals the reduction of (-1)^(n+1); both are 1.

3. Oriented-degree wrappers

The same mod-2 comparison statements on the bundled SphereOrientation.degree.

theorem SphereOddDegree.SphereOrientation.degree_intCast_zmodTwo_eq_one_iff_odd (o : SphereOrientation) {n : ℕ} (f : C(Sphere n, Sphere n)) : ↑(o.degree f) = 1 ↔ Odd (o.degree f)

The reduction of the integer degree to ZMod 2 is 1 iff the degree is odd.

theorem SphereOddDegree.SphereOrientation.degree_comp_intCast_zmodTwo (o : SphereOrientation) {n : ℕ} (f g : C(Sphere n, Sphere n)) : ↑(o.degree (g.comp f)) = ↑(o.degree g) * ↑(o.degree f)

Multiplicativity of the mod-2 degree on the bundled orientation.

theorem SphereOddDegree.SphereOrientation.degree_homeomorph_intCast_zmodTwo_eq_one (o : SphereOrientation) {n : ℕ} (h : Sphere n ≃ₜ Sphere n) : ↑(o.degree ↑h) = 1

The mod-2 degree of a self-homeomorphism is 1.

theorem SphereOddDegree.SphereOrientation.degree_antipodal_intCast_zmodTwo_eq_one (o : SphereOrientation) {n : ℕ} : ↑(o.degree (antipodal n)) = 1

The mod-2 degree of the antipodal map is 1.