The involution-orbit datum is an equivariant factor set (Lemma 6.2)

GQ2.invOrbitDatum N gbar (defined in GQ2/OrbitData.lean) is the paper's involution-orbit cocycle E_ḡ (Lemma 6.2, eqs. (67)–(73)): for an involution ḡ of C = G/N, the factor set f_g(x,y) = Σ_{u} x_{u} y_{uḡ} (summed over the ⟨ḡ⟩-coset transversal, realized as Quotient.out) together with the nonzero orientation corrections m^g_c(x) = Σ_u ε_c(u)·x_{π_c(u)} x_{π_c(u)ḡ}.

This file proves isEquivariantFactorSet_invOrbitDatum: the seven IsEquivariantFactorSet identities, the hard ones being (71) m_quad and (72) m_mul. Own file (imports only OrbitData); consumed by the kappa0_exists orbit sum in the §9 layer.

The transversal bookkeeping (eqs. (67), (74))

Write O := C ⧸ ⟨ḡ⟩ for the coset space, u.out : C the canonical representative. For c : C, left translation u ↦ ↑(c⁻¹ · u.out) is a bijection piEquiv c : O ≃ O (the paper's π_c), and ε_c(u) ∈ 𝔽₂ records whether c⁻¹·u.out is already the canonical rep of its coset (ε = 0) or the twisted one π_c(u)·ḡ (ε = 1). With ḡ² = 1 the coset is {π, πḡ}, so c⁻¹·u.out ∈ {π_c(u), π_c(u)·ḡ} — the decomposition (67).

No axioms; Ax = ∅.

theorem GQ2.mk_mul_out_eq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar a w : G ⧸ N) : ↑(a * Quotient.out ↑w) = ↑(a * w)

Left translation commutes with the ⟨ḡ⟩-coset projection past a chosen representative: ↑(a · (↑w).out) = ↑(a · w) in O.

noncomputable def GQ2.piEquiv {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) : (G ⧸ N) ⧸ Subgroup.zpowers gbar ≃ (G ⧸ N) ⧸ Subgroup.zpowers gbar

π_c (paper (67)): left translation by c⁻¹ on the ⟨ḡ⟩-coset space, u ↦ ↑(c⁻¹·u.out). A bijection with inverse u ↦ ↑(c·u.out).

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.zpowers_sq_dichotomy {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (hg2 : gbar * gbar = 1) {t : G ⧸ N} (ht : t ∈ Subgroup.zpowers gbar) : t = 1 ∨ t = gbar

With ḡ² = 1 the cyclic subgroup ⟨ḡ⟩ is {1, ḡ}.

theorem GQ2.coset_out_decomp {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (hg2 : gbar * gbar = 1) (c : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : c⁻¹ * Quotient.out u = Quotient.out ↑(c⁻¹ * Quotient.out u) ∨ c⁻¹ * Quotient.out u = Quotient.out ↑(c⁻¹ * Quotient.out u) * gbar

Eq. (67): with ḡ² = 1, c⁻¹·u.out is either the canonical representative π_c(u) of its ⟨ḡ⟩-coset (ε = 0) or the twist π_c(u)·ḡ (ε = 1).

theorem GQ2.invOrbitDatum_f_apply {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (x y : RegRep N) : (invOrbitDatum N gbar).f x y = ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar), x (Quotient.out u) * y (Quotient.out u * gbar)

Unfolding lemma for invOrbitDatum's factor set (definitional).

theorem GQ2.invOrbitDatum_m_apply {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) (x : RegRep N) : (invOrbitDatum N gbar).m c x = ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar), (if c⁻¹ * Quotient.out u = Quotient.out ↑(c⁻¹ * Quotient.out u) then 0 else 1) * (x (Quotient.out ↑(c⁻¹ * Quotient.out u)) * x (Quotient.out ↑(c⁻¹ * Quotient.out u) * gbar))

Unfolding lemma for invOrbitDatum's corrections (definitional).

noncomputable def GQ2.piElt {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : G ⧸ N

The canonical ⟨ḡ⟩-coset representative of c⁻¹·u.out — the paper's π_c(u) (an element).

Equations

• GQ2.piElt N gbar c u = Quotient.out ↑(c⁻¹ * Quotient.out u)

noncomputable def GQ2.epsFun {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : ZMod 2

The orientation bit ε_c(u) (paper (67)): 0 if c⁻¹·u.out is already canonical, else 1.

Equations

• GQ2.epsFun N gbar c u = if c⁻¹ * Quotient.out u = GQ2.piElt N gbar c u then 0 else 1

theorem GQ2.piElt_eq_out {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : piElt N gbar c u = Quotient.out ((piEquiv N gbar c) u)

theorem GQ2.invOrbitDatum_m_apply' {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c : G ⧸ N) (x : RegRep N) : (invOrbitDatum N gbar).m c x = ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar), epsFun N gbar c u * (x (piElt N gbar c u) * x (piElt N gbar c u * gbar))

m in piElt/epsFun form (definitional).

theorem GQ2.coset_out_decomp' {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (hg2 : gbar * gbar = 1) (c : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : c⁻¹ * Quotient.out u = piElt N gbar c u ∨ c⁻¹ * Quotient.out u = piElt N gbar c u * gbar

(67) restated in piElt form.

theorem GQ2.square_term_out {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (hg2 : gbar * gbar = 1) (x : RegRep N) (a : G ⧸ N) : x a * x (a * gbar) = x (Quotient.out ↑a) * x (Quotient.out ↑a * gbar)

Shift-invariance of the square term (ḡ²=1): x_a x_{aḡ} depends only on the coset of a, so it equals x_{π} x_{πḡ} for the canonical rep π = (↑a).out.

theorem GQ2.piEquiv_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c d : G ⧸ N) : piEquiv N gbar (c * d) = (piEquiv N gbar c).trans (piEquiv N gbar d)

Paper (74), coset half: π_{cd} = π_d ∘ π_c as maps on the coset space.

theorem GQ2.piElt_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar c d : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : piElt N gbar (c * d) u = piElt N gbar d ((piEquiv N gbar c) u)

Paper (74), representative form: π_{cd}(u) = π_d(π_c(u)).

theorem GQ2.epsFun_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) (hg2 : gbar * gbar = 1) (c d : G ⧸ N) (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar) : epsFun N gbar (c * d) u = epsFun N gbar c u + epsFun N gbar d ((piEquiv N gbar c) u)

Paper (74), orientation half: ε_{cd}(u) = ε_c(u) + ε_d(π_c(u)) in 𝔽₂ (the g-exponents add mod 2). The 4-case bash on (ε_c, ε_d); the mixed cases use ḡ²=1 and mul_right_eq_self.

theorem GQ2.invOrbitDatum_f_add_left {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) [Finite (G ⧸ N)] (x x' y : RegRep N) : (invOrbitDatum N gbar).f (x + x') y = (invOrbitDatum N gbar).f x y + (invOrbitDatum N gbar).f x' y

Left-additivity of the involution factor set.

theorem GQ2.invOrbitDatum_f_add_right {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) [Finite (G ⧸ N)] (x y y' : RegRep N) : (invOrbitDatum N gbar).f x (y + y') = (invOrbitDatum N gbar).f x y + (invOrbitDatum N gbar).f x y'

Right-additivity of the involution factor set.

theorem GQ2.isEquivariantFactorSet_invOrbitDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) [Finite (G ⧸ N)] (hg2 : gbar * gbar = 1) : IsEquivariantFactorSet (fun (x : RegRep N) => ∑ᶠ (u : (G ⧸ N) ⧸ Subgroup.zpowers gbar), x (Quotient.out u) * x (Quotient.out u * gbar)) (invOrbitDatum N gbar)

The involution-orbit datum is an equivariant factor set (Lemma 6.2, eqs. (71)–(73)) for its square map q_g x = Σ_u x_{u} x_{uḡ}. Needs the involution hypothesis ḡ² = 1.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (67) = ⟦eq-piepsilon⟧
• eq. (71) = ⟦eq-halforbitquadratic⟧
• eq. (73) = ⟦eq-kappahalforbit⟧
• Lemma 6.2 = ⟦lem-halforbitcocycle⟧