Documentation

GQ2.RegularIsometry

The isometric regular embedding #

The C-equivariant split embedding of a ramified simple faithful quadratic 𝔽₂[C]-module (V, q) into a regular module W = PermW C N = 𝔽₂[C]^N, carrying the pulled-back form Q_W := q ∘ r (r the equivariant retraction) together with an equivariant factor-set datum for it. This upgrades RegularSummand.lemma_6_11 (a pure module embedding) to an isometry Q_W ∘ ι = q, and supplies an equivariant FactorSet on W — the datum-side input of the §6.2 orbit route to SectionSix.lemma_6_17_vanish.

What regular_isometric_embedding delivers #

From lemma_6_11 we obtain N, the equivariant embedding ι : V →+ W, the equivariant retraction r : W →+ V, and r ∘ ι = id. Setting Q_W := q ∘ r:

The two equivariances are re-expressed in the PermW DistribMulAction form ι (h • v) = h • ι v and r (h • F) = h • r F — the shape RepIndependence.lemma_6_14 consumes.

This mirrors the ramified branch of KappaNormalForm.kappa0_exists_tame, but exposes ι, r, datW and the isometry instead of immediately collapsing them to ∃ dat, IsEquivariantFactorSet q dat on V. The exposed package is what the §6.3 orbit computation (Lemmas 6.14–6.17) transports through.

Relation to the full f2b interface / the remaining core #

The full f2b result additionally asks for datW = sumDatum (orbit datums) — the §6.2 orbit decomposition of Q_W into square/free/involution orbit polynomials ((75)/(76)/Lemma 6.2), whose per-orbit equivariance is banked (isEquivariantFactorSet_{square,free,inv}OrbitDatum in SectionNine/InvolutionDatum). The banked normal form exists_datum_of_invariant_quadratic deliberately takes the single invariant-biadditive β-refinement route (docs/orchestration/p17e-kappa0-scoping.md), so it produces datW but not its orbit-sum form; recovering the latter is the combinatorial core of the orbit route. This file supplies the datum-independent isometric-embedding infrastructure that either route (the orbit route or the flagged β-route) consumes.

No axioms; Ax = ∅ (std-3 throughout, inheriting only the axioms of lemma_6_11).

source
theorem GQ2.regular_isometric_embedding {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hgen : Subgroup.closure {c tameSigma, c tameTau} = ⊤) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hinv : QuadraticFp2.IsInvariant C q) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) :
∃ (N : ℕ) (ι : V →+ PermW C N) (r : PermW C N →+ V) (datW : FactorSet C (PermW C N)), IsEquivariantFactorSet (fun (F : PermW C N) => q (r F)) datW ∧ (∀ (v : V), q (r (ι v)) = q v) ∧ (∀ (h : C) (v : V), ι (h • v) = h • ι v) ∧ (∀ (h : C) (F : PermW C N), r (h • F) = h • r F) ∧ ∀ (v : V), r (ι v) = v

The isometric regular embedding (the Lemma 6.17 vanishing proof, P1 + the β-datum): a ramified simple faithful 2-torsion quadratic 𝔽₂[C]-module (V, q) embeds C-equivariantly as a split summand of a regular module W = 𝔽₂[C]^N, carrying the pulled-back form Q_W := q ∘ r and an equivariant factor-set datum for it, so that ι is an isometry Q_W (ι v) = q v.

Everything is extracted from lemma_6_11's module split (equivariance, retraction) plus the permutation-module normal form exists_datum_of_invariant_quadratic; the isometry is free from r (ι v) = v.

The orbit-sum isometric embedding #

Reindex the foundation's regular summand 𝔽₂[C] to RegRep N along e : C ≃* G ⧸ N, then apply the §6.2 orbit decomposition (OrbitDecomp.isEquivariantFactorSet_orbitSumDatum) to the pulled-back form. The C ≅ AbsGalQ2 ⧸ ker ρ instantiation of e stays with f2c/f2d.

source
def GQ2.reSummand {C : Type} [Group C] {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (e : C ≃* G ⧸ N) :
(C → ZMod 2) ≃+ RegRep N

Reindex a single regular summand 𝔽₂[C] to RegRep N along e : C ≃* G ⧸ N.

Equations
  • GQ2.reSummand N e = { toFun := fun (f : C → ZMod 2) (h : G ⧸ N) => f (e.symm h), invFun := fun (g : GQ2.RegRep N) (c : C) => g (e c), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
    source
    def GQ2.reBlock {C : Type} [Group C] {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (e : C ≃* G ⧸ N) (K : ℕ) :
    (Fin K → C → ZMod 2) ≃+ (Fin K → RegRep N)

    The blockwise reindex 𝔽₂[C]^K ≃+ (Fin K → RegRep N).

    Equations
    Instances For
      source
      theorem GQ2.regular_isometric_embedding_orbit {C : Type} [Group C] {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [TopologicalSpace C] [Finite C] [Fintype (G ⧸ N)] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (e : C ≃* G ⧸ N) (cT : ↑Ttame.toProfinite.toTop →ₜ* C) (hgen : Subgroup.closure {cT tameSigma, cT tameTau} = ⊤) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hinv : QuadraticFp2.IsInvariant C q) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), cT tameTau • v ≠ v) :
      ∃ (K : ℕ) (ι : V →+ Fin K → RegRep N) (r : (Fin K → RegRep N) →+ V), IsEquivariantFactorSet (fun (F : Fin K → RegRep N) => q (r F)) (OrbitVanish.sumDatum (orbitIndexSet N fun (F : Fin K → RegRep N) => q (r F)) (orbitDatum N)) ∧ (∀ (v : V), q (r (ι v)) = q v) ∧ (∀ (a : C) (v : V), ι (a • v) = e a • ι v) ∧ ∀ (v : V), r (ι v) = v

      The orbit-sum isometric embedding (the Lemma 6.17 vanishing proof): a ramified simple faithful quadratic 𝔽₂[C]-module (V, q) embeds C-equivariantly (through e : C ≃* G ⧸ N) as a split summand of Fin K → RegRep N, carrying the pulled-back form Q_W := q ∘ r together with the §6.2 orbit-sum datum sumDatum (orbitIndexSet Q_W) orbitDatum for it, an isometry. This is the full the Lemma 6.17 vanishing proof interface with datW definitionally the orbit sum — the shape OrbitVanish.Q0loc_vanish_of_datum_decomp consumes.