Ramified isotypic foundations

Conjugation, polynomial Frobenius, the single-isotype reduction, and the adjoin-root structure.

See GQ2.RamifiedPack for the paper-facing overview, source citations, and deviations.

§TwoPowerConj: conjugates of t are 2-power powers of t

theorem GQ2.RamifiedPack.conj_pow_eq {C : Type u_1} [Group C] (z t : C) (N : ℕ) : z * t ^ N * z⁻¹ = (z * t * z⁻¹) ^ N

Conjugation distributes over ℕ-powers (the MulAut.conj/map_pow massage).

theorem GQ2.RamifiedPack.inv_conj_pow_eq {C : Type u_1} [Group C] (z t : C) (N : ℕ) : z⁻¹ * t ^ N * z = (z⁻¹ * t * z) ^ N

Conjugation distributes over ℕ-powers, inverse flavor.

theorem GQ2.RamifiedPack.eq_two_pow_of_sq_eq {C : Type u_1} [Group C] {t x : C} (hd : Odd (orderOf t)) (hpos : 0 < orderOf t) (horder : orderOf x = orderOf t) (hx2 : x ^ 2 = t) : x = t ^ 2 ^ ((orderOf t).totient - 1)

The square-root step: if x² = t with x of the same odd order d, then x = t^{2^{φ(d)−1}} — from Euler's 2^{φ(d)} ≡ 1 (mod d).

theorem GQ2.RamifiedPack.conj_eq_two_pow {C : Type u_1} [Group C] (s t : C) (hgen : Subgroup.closure {s, t} = ⊤) (hrel : s⁻¹ * t * s = t ^ 2) (hodd : Odd (orderOf t)) (hpos : 0 < orderOf t) (g : C) : (∃ (j : ℕ), g⁻¹ * t * g = t ^ 2 ^ j) ∧ ∃ (j : ℕ), g * t * g⁻¹ = t ^ 2 ^ j

Every element of C = ⟨s, t⟩ conjugates t to a 2-power power of t (both directions): the S-twist is squaring (hrel), its inverse the Euler square root, and exponents compose multiplicatively along the closure induction.

§PolyFrobenius: the operator-level char-2 Frobenius and kernel stability

Design doc §3: for P over 𝔽₂, P(φ^{2^j}) = P(φ)^{2^j} in the endomorphism algebra (via expand + the trivial Frobenius of ZMod 2), so the kernel of P(t̂) is stable under any g with g⁻¹tg = t^{2^j} — combined with §TwoPowerConj this makes every isotypic component C-stable.

noncomputable def GQ2.RamifiedPack.actEnd {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] (t : C) : Module.End (ZMod 2) V

The action of t : C as a ZMod 2-linear endomorphism (any additive map is).

Equations

• GQ2.RamifiedPack.actEnd t = AddMonoidHom.toZModLinearMap 2 (DistribSMul.toAddMonoidHom V t)

theorem GQ2.RamifiedPack.actEnd_pow {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] (t : C) (n : ℕ) : actEnd (t ^ n) = actEnd t ^ n

actEnd turns group powers into endomorphism powers.

theorem GQ2.RamifiedPack.expand_two_pow_eq_pow (P : Polynomial (ZMod 2)) (j : ℕ) : (Polynomial.expand (ZMod 2) (2 ^ j)) P = P ^ 2 ^ j

The 𝔽₂-Frobenius is trivial, so expand by 2^j is literally the 2^j-th power of the polynomial.

theorem GQ2.RamifiedPack.aeval_pow_two_pow {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] (φ : Module.End (ZMod 2) V) (P : Polynomial (ZMod 2)) (j : ℕ) : (Polynomial.aeval (φ ^ 2 ^ j)) P = (Polynomial.aeval φ) P ^ 2 ^ j

The operator-level char-2 Frobenius: evaluating P at the 2^j-th power of an endomorphism is the 2^j-th power of the evaluation.

theorem GQ2.RamifiedPack.aeval_actEnd_smul {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] (t g : C) (P : Polynomial (ZMod 2)) (v : V) : ((Polynomial.aeval (actEnd t)) P) (g • v) = g • ((Polynomial.aeval (actEnd (g⁻¹ * t * g))) P) v

Polynomial evaluation transports across the group action by conjugating the operator.

theorem GQ2.RamifiedPack.smul_mem_ker_aeval {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] {t g : C} {j : ℕ} (hconj : g⁻¹ * t * g = t ^ 2 ^ j) (P : Polynomial (ZMod 2)) (v : V) (hv : ((Polynomial.aeval (actEnd t)) P) v = 0) : ((Polynomial.aeval (actEnd t)) P) (g • v) = 0

Kernel stability (design doc §3): if g⁻¹tg = t^{2^j} then the kernel of any P(t̂) is g-stable — P(t^{2^j}) = P(t)^{2^j} and powers of a vanishing operator vanish.

§SingleIsotype: V is killed by ONE irreducible factor of X^d − 1

Design doc §2–3, with a lighter route than torsion-internal-decomposition: if every irreducible-factor kernel were ⊥, every Q(t̂) would be injective, so their product (X^d − 1)(t̂) = 0 would be injective on V ≠ 0 — contradiction. The nonzero kernel is C-stable (§PolyFrobenius + §TwoPowerConj), so hsimple promotes it to ⊤.

theorem GQ2.RamifiedPack.list_prod_injective {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] (L : List (Module.End (ZMod 2) V)) (h : ∀ f ∈ L, Function.Injective ⇑f) : Function.Injective ⇑L.prod

A product of injective endomorphisms is injective (List-form — Module.End is noncommutative, so no Multiset.prod).

theorem GQ2.RamifiedPack.aeval_X_pow_orderOf_sub_one {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] (t : C) : (Polynomial.aeval (actEnd t)) (Polynomial.X ^ orderOf t - 1) = 0

(X^d − 1)(t̂) = 0 for d := orderOf t.

theorem GQ2.RamifiedPack.exists_single_isotype {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] [Finite V] (s t : C) (hgen : Subgroup.closure {s, t} = ⊤) (hrel : s⁻¹ * t * s = t ^ 2) (hodd : Odd (orderOf t)) (hpos : 0 < orderOf t) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : V), v ≠ 0) : ∃ (P : Polynomial (ZMod 2)), P.Monic ∧ Irreducible P ∧ P ∣ Polynomial.X ^ orderOf t - 1 ∧ ∀ (v : V), ((Polynomial.aeval (actEnd t)) P) v = 0

The single isotype (design doc §2–3): with C = ⟨s,t⟩, t of odd order, and V a nonzero simple C-module, there is ONE monic irreducible P ∣ X^d − 1 with P(t̂) = 0 on all of V.

§AdjoinRootStructure: V is a vector space over D := AdjoinRoot P

Design doc §2's payoff: with P(t̂) = 0 on V (§SingleIsotype), V is a module over 𝔽₂[X]/(P) = AdjoinRoot P — a FIELD — so it is automatically free: V ≃ D^s, with t acting as the scalar root P. No Maschke, no complements.

theorem GQ2.RamifiedPack.card_adjoinRoot (P : Polynomial (ZMod 2)) (hmon : P.Monic) : Nat.card (AdjoinRoot P) = 2 ^ P.natDegree

#(AdjoinRoot P) = 2^{deg P} for monic P over 𝔽₂ (the power basis).

theorem GQ2.RamifiedPack.exists_isotypic_equiv {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V] [DistribMulAction C V] [Finite V] (t : C) (P : Polynomial (ZMod 2)) (hirr : Irreducible P) (hkill : ∀ (v : V), ((Polynomial.aeval (actEnd t)) P) v = 0) (hVne : ∃ (v : V), v ≠ 0) : ∃ (s : ℕ) (e : V ≃+ (Fin s → AdjoinRoot P)), 1 ≤ s ∧ ∀ (v : V) (j : Fin s), e (t • v) j = AdjoinRoot.root P * e v j

The free D-structure (design doc §2): with P monic irreducible killing t̂ on V, there is an additive equivalence e : V ≃+ (Fin s → AdjoinRoot P), s ≥ 1, under which t acts as multiplication by root P in every coordinate.