The semidirect atom calculus and the ω_χ-decomposition

Split off from GQ2.KeystoneDelta (design §§1–2). This file provides:

• the raw semidirect calculus on V × C₀ (pmul, pone, associativity) with the transported product maps jmap/Jmap and their multiplicativity;
• the three T-valued defect atoms mDef/conjDef/uDef and the product formula JDefT = conjDef · uDef · mDef, with the mDef/conjDef atom identities;
• the ω_χ-decomposition χ ∘ JDef = kappa0 (datχ χ) + inflScalar (eχ χ) via the equivariant zero-form factor-set datum datChi.

See GQ2.KeystoneDelta for the umbrella module docstring.

The raw semidirect calculus on V × C₀

def GQ2.SectionEight.AffineTLift.pmul {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (p q : DD.Vmod × DD.C0) : DD.Vmod × DD.C0

The semidirect product on raw pairs (lemma_6_22's convention).

Equations

• GQ2.SectionEight.AffineTLift.pmul p q = (p.1 + p.2 • q.1, p.2 * q.2)

def GQ2.SectionEight.AffineTLift.pone {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} : DD.Vmod × DD.C0

The semidirect identity.

Equations

• GQ2.SectionEight.AffineTLift.pone = (0, 1)

theorem GQ2.SectionEight.AffineTLift.pmul_assoc {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (p q r : DD.Vmod × DD.C0) : pmul (pmul p q) r = pmul p (pmul q r)

theorem GQ2.SectionEight.AffineTLift.pone_pmul {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (p : DD.Vmod × DD.C0) : pmul pone p = p

theorem GQ2.SectionEight.AffineTLift.pmul_pone {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (p : DD.Vmod × DD.C0) : pmul p pone = p

noncomputable def GQ2.SectionEight.AffineTLift.jmap {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) (σ : DD.C0 →* Bg ⧸ D.T) (p : DD.Vmod × DD.C0) : Bg ⧸ D.T

The transported product map into Q = Bg/T: jmap (v, cc) = iV(v)·σ(cc).

Equations

• GQ2.SectionEight.AffineTLift.jmap DD σ p = (GQ2.SectionEight.AffineTLift.iV DD) (Multiplicative.ofAdd p.1) * σ p.2

theorem GQ2.SectionEight.AffineTLift.jmap_mul {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q : DD.Vmod × DD.C0) : jmap DD σ p * jmap DD σ q = jmap DD σ (pmul p q)

jmap is multiplicative for the semidirect product.

theorem GQ2.SectionEight.AffineTLift.jmap_pone {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} : jmap DD σ pone = 1

The pointwise product lift J and the defect atoms

noncomputable def GQ2.SectionEight.AffineTLift.Jmap {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (p : DD.Vmod × DD.C0) : Bg

The pointwise product lift into Bg: J (v, cc) = mV(v)·uσ(cc).

Equations

• GQ2.SectionEight.AffineTLift.Jmap S p = ↑(S.mV p.1) * S.uσ p.2

theorem GQ2.SectionEight.AffineTLift.Jmap_defect_mem {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q : DD.Vmod × DD.C0) : Jmap S p * Jmap S q * (Jmap S (pmul p q))⁻¹ ∈ D.T

The J-defect lands in T.

noncomputable def GQ2.SectionEight.AffineTLift.JDefT {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q : DD.Vmod × DD.C0) : ↥D.T

The J-defect as a T-element.

Equations

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

The three atoms

theorem GQ2.SectionEight.AffineTLift.mDef_mem {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v w : DD.Vmod) : ↑(S.mV v) * ↑(S.mV w) * (↑(S.mV (v + w)))⁻¹ ∈ D.T

The mV-additivity defect mDef v w = mV(v)·mV(w)·mV(v+w)⁻¹ ∈ T.

noncomputable def GQ2.SectionEight.AffineTLift.mDef {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v w : DD.Vmod) : ↥D.T

mDef v w := mV(v)·mV(w)·mV(v+w)⁻¹, the mV-additivity defect.

Equations

• GQ2.SectionEight.AffineTLift.mDef DD S v w = ⟨↑(S.mV v) * ↑(S.mV w) * (↑(S.mV (v + w)))⁻¹, ⋯⟩

theorem GQ2.SectionEight.AffineTLift.conjDef_mem {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (w : DD.Vmod) : S.uσ cc * ↑(S.mV w) * (S.uσ cc)⁻¹ * (↑(S.mV (cc • w)))⁻¹ ∈ D.T

The conjugation defect conjDef cc w = uσ(cc)·mV(w)·uσ(cc)⁻¹·mV(cc•w)⁻¹ ∈ T.

noncomputable def GQ2.SectionEight.AffineTLift.conjDef {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (w : DD.Vmod) : ↥D.T

conjDef cc w, the conjugation defect of the sections.

Equations

• GQ2.SectionEight.AffineTLift.conjDef DD S hσ cc w = ⟨S.uσ cc * ↑(S.mV w) * (S.uσ cc)⁻¹ * (↑(S.mV (cc • w)))⁻¹, ⋯⟩

theorem GQ2.SectionEight.AffineTLift.uDef_mem {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (cc dd : DD.C0) : S.uσ cc * S.uσ dd * (S.uσ (cc * dd))⁻¹ ∈ D.T

The uσ-multiplicativity defect uDef cc dd = uσ(cc)·uσ(dd)·uσ(cc·dd)⁻¹ ∈ T — the class e of Lemma 8.7.

noncomputable def GQ2.SectionEight.AffineTLift.uDef {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (cc dd : DD.C0) : ↥D.T

uDef cc dd, the base extension class e at cochain level.

Equations

• GQ2.SectionEight.AffineTLift.uDef DD S cc dd = ⟨S.uσ cc * S.uσ dd * (S.uσ (cc * dd))⁻¹, ⋯⟩

theorem GQ2.SectionEight.AffineTLift.M_comm_T {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {m t : Bg} (hm : m ∈ D.M) (ht : t ∈ D.T) : m * t = t * m

M commutes with T elementwise (commutation form of M_cent_T).

theorem GQ2.SectionEight.AffineTLift.JDefT_eq {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q : DD.Vmod × DD.C0) : JDefT S hσ p q = conjDef DD S hσ p.2 q.1 * uDef DD S p.2 q.2 * mDef DD S p.1 (p.2 • q.1)

The product formula: the J-defect is the all-T product conjDef · uDef · mDef (M abelian, T centralized by M).

The mDef-atom identities (through the abelian ↥D.M)

@[implicit_reducible]

def GQ2.SectionEight.AffineTLift.commGroupM {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} : CommGroup ↥D.M

↥D.M is commutative (file-local instance — the underlying Mul is definitionally the subgroup one, so no diamond escapes this leaf).

Equations

• GQ2.SectionEight.AffineTLift.commGroupM = { toGroup := inferInstance, mul_comm := ⋯ }

theorem GQ2.SectionEight.AffineTLift.mDef_symm {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v w : DD.Vmod) : mDef DD S v w = mDef DD S w v

theorem GQ2.SectionEight.AffineTLift.mDef_self {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v : DD.Vmod) : mDef DD S v v = 1

theorem GQ2.SectionEight.AffineTLift.mDef_zero_left {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (w : DD.Vmod) : mDef DD S 0 w = 1

theorem GQ2.SectionEight.AffineTLift.mDef_cocycle {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v w x : DD.Vmod) : mDef DD S (v + w) x * mDef DD S v w = mDef DD S v (w + x) * mDef DD S w x

The mDef-cocycle identity (the f_cocycle field of the zero-form factor set).

The conjDef-atom identities

theorem GQ2.SectionEight.AffineTLift.mV_add_split {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (w w' : DD.Vmod) : ↑(S.mV (w + w')) = (↑(mDef DD S w w'))⁻¹ * ↑(S.mV w) * ↑(S.mV w')

mV(w+w') split through the defect: mV(w+w') = mDef(w,w')⁻¹ · mV w · mV w'.

theorem GQ2.SectionEight.AffineTLift.conjDef_add {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (w w' : DD.Vmod) : conjDef DD S hσ cc (w + w') = ⟨S.uσ cc * (↑(mDef DD S w w'))⁻¹ * (S.uσ cc)⁻¹, ⋯⟩ * conjDef DD S hσ cc w * conjDef DD S hσ cc w' * mDef DD S (cc • w) (cc • w')

The conjDef additivity defect (m_quad-shape): conjugating the mV-split by uσ cc.

theorem GQ2.SectionEight.AffineTLift.conjDef_mul {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc dd : DD.C0) (v : DD.Vmod) : conjDef DD S hσ (cc * dd) v = ⟨S.uσ cc * ↑(conjDef DD S hσ dd v) * (S.uσ cc)⁻¹, ⋯⟩ * conjDef DD S hσ cc (dd • v)

The conjDef composition law (m_mul-shape): splitting uσ(cc·dd) through uDef.

theorem GQ2.SectionEight.AffineTLift.conjDef_one_left {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (w : DD.Vmod) : conjDef DD S hσ 1 w = 1

conjDef at the identity of C₀ is trivial.

theorem GQ2.SectionEight.AffineTLift.conjDef_zero_right {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) : conjDef DD S hσ cc 0 = 1

conjDef at the zero vector is trivial.

The zero-form factor set of the χ-pushout (design §2)

noncomputable def GQ2.SectionEight.AffineTLift.datChi {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) : FactorSet DD.C0 DD.Vmod

The χ-pushout factor-set datum: f_χ := χ ∘ mDef, m_χ := χ ∘ conjDef. Together with the scalar e_χ := χ ∘ uDef this is the explicit (130)-normal form of the χ-pushout cover (chiJDef_eq).

Equations

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

theorem GQ2.SectionEight.AffineTLift.isEquivariantFactorSet_datChi {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) : IsEquivariantFactorSet (fun (x : DD.Vmod) => 0) (datChi DD S hσ χ)

datChi is an equivariant factor-set datum for the zero form.

theorem GQ2.SectionEight.AffineTLift.chiJDef_eq {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (p q : DD.Vmod × DD.C0) : ↑χ (JDefT S hσ p q) = kappa0 (datChi DD S hσ χ) p q + ↑χ (uDef DD S p.2 q.2)

The ω_χ-decomposition (design §2): the χ-pushforward of the J-defect is the base cocycle of datChi plus the inflated scalar e_χ = χ ∘ uDef — the explicit (130)-normal form of the χ-pushout cover.