The finite ω₂-power machinery (Stage A)

ω₂ ∈ Ẑ = ∏_p ℤ_p is the idempotent whose ℤ₂-component is 1 and whose ℤ_ℓ-component is 0 for every prime ℓ ≠ 2 (the 2-primary projection). Its residue modulo n is the CRT idempotent: writing n = 2^a · m with m odd (a = v₂ n), it is ≡ 1 (mod 2^a) and ≡ 0 (mod m).

To raise a finite-order group element g to the ω₂-power one reduces ω₂ modulo the order of g (or any multiple of it) and takes the ordinary power. The manuscript's finite-exponent independence (lem:finiteexponent) says any two integer representatives of ω₂ modulo the exponent of the finite target give the same element; here this is finite_omega2_pow_independent_of_rep.

Main definitions:

• omega2Mod n : ZMod n — the idempotent reduced mod n.
• powOmega2 g — g to the ω₂-power, depending only on orderOf g.

Main lemmas:

• omega2Mod_eq_one_on_two_part, omega2Mod_eq_zero_on_odd_part
• finite_omega2_pow_idempotent
• finite_omega2_pow_independent_of_rep

def Q2Presentation.omega2Mod (n : ℕ) : ZMod n

The 2-primary idempotent ω₂ ∈ Ẑ reduced modulo n: the odd part raised to φ of the 2-part. It is ≡ 1 modulo the 2-part ordProj[2] n = 2 ^ (v₂ n) and ≡ 0 modulo the odd part ordCompl[2] n.

Equations

• Q2Presentation.omega2Mod n = ↑(n / 2 ^ n.factorization 2) ^ (2 ^ n.factorization 2).totient

theorem Q2Presentation.omega2Mod_eq_one_on_two_part (n : ℕ) : (ZMod.castHom ⋯ (ZMod (2 ^ n.factorization 2))) (omega2Mod n) = 1

omega2Mod n reduces to 1 modulo the 2-part ordProj[2] n.

theorem Q2Presentation.omega2Mod_eq_zero_on_odd_part (n : ℕ) : (ZMod.castHom ⋯ (ZMod (n / 2 ^ n.factorization 2))) (omega2Mod n) = 0

omega2Mod n reduces to 0 modulo the odd part ordCompl[2] n.

theorem Q2Presentation.omega2Mod_castHom {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (h : m ∣ n) : (ZMod.castHom h (ZMod m)) (omega2Mod n) = omega2Mod m

Compatibility of omega2Mod with the reduction maps ZMod n → ZMod m (m ∣ n, both nonzero): the family (omega2Mod n)ₙ is coherent.

theorem Q2Presentation.omega2Mod_idempotent {n : ℕ} (hn : n ≠ 0) : omega2Mod n * omega2Mod n = omega2Mod n

omega2Mod is idempotent in ZMod n (n ≠ 0): it is a genuine idempotent of the ring, namely the 2-primary projection.

theorem Q2Presentation.omega2Mod_val_modEq {m N : ℕ} (hm : m ≠ 0) (hN : N ≠ 0) (h : m ∣ N) : (omega2Mod N).val ≡ (omega2Mod m).val [MOD m]

(omega2Mod N).val, reduced modulo any divisor m of N, is (omega2Mod m).val. This is the numerical form of omega2Mod_castHom and is what makes the finite ω₂-power independent of the chosen modulus.

noncomputable def Q2Presentation.powOmega2 {G : Type u_1} [Group G] [Finite G] (g : G) : G

g raised to the ω₂-power in a finite group: reduce ω₂ modulo orderOf g and take the ordinary power. This depends only on g (through its order), not on any fixed verification modulus.

Equations

• Q2Presentation.powOmega2 g = g ^ (Q2Presentation.omega2Mod (orderOf g)).val

theorem Q2Presentation.finite_omega2_pow_independent_of_rep {G : Type u_1} [Group G] [Finite G] (g : G) {N : ℕ} (hN : N ≠ 0) (hdvd : orderOf g ∣ N) : g ^ (omega2Mod N).val = powOmega2 g

Finite-exponent independence (lem:finiteexponent). For any nonzero multiple N of orderOf g, raising g to the residue of ω₂ modulo N gives the intrinsic ω₂-power. In particular the fixed verification modulus of the manuscript yields the same element as the genuine profinite exponent.

theorem Q2Presentation.map_powOmega2 {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Group H] [Finite H] (φ : G →* H) (g : G) : φ (powOmega2 g) = powOmega2 (φ g)

powOmega2 is functorial: it commutes with group homomorphisms between finite groups.

theorem Q2Presentation.finite_omega2_pow_idempotent {G : Type u_1} [Group G] [Finite G] (g : G) : powOmega2 (powOmega2 g) = powOmega2 g

The ω₂-power is idempotent: powOmega2 (powOmega2 g) = powOmega2 g.

theorem Q2Presentation.powOmega2_eq_one_of_odd_order {G : Type u_1} [Group G] [Finite G] {g : G} (h : Odd (orderOf g)) : powOmega2 g = 1

If g has odd order then its ω₂-power is trivial (the 2-primary part of ⟨g⟩ is trivial).

theorem Q2Presentation.powOmega2_eq_self_of_two_power_order {G : Type u_1} [Group G] [Finite G] {g : G} (h : ∃ (k : ℕ), orderOf g = 2 ^ k) : powOmega2 g = g

If orderOf g is a power of 2 then g is fixed by the ω₂-power: the 2-primary projection acts as the identity on a 2-group. (Used for the pro-2 quotient simplification.)