Documentation

Q2Presentation.Induction.TerminalBridgeGroupTheory

Generic helpers #

source
theorem Q2Presentation.Induction.TerminalBridge.dvd_two_pow_dvd_odd_eq_one {d r m : ℕ} (hodd : Odd m) (h1 : d ∣ 2 ^ r) (h2 : d ∣ m) :
d = 1

A common divisor of 2^r and an odd number is 1.

source
theorem Q2Presentation.Induction.TerminalBridge.eq_one_of_conj_eq_sq {G : Type u_1} [Group G] [Finite G] (h2 : IsPGroup 2 G) (s t : G) (hrel : s * t * s⁻¹ = t ^ 2) :
t = 1

The tame relation dies in a finite 2-group: if s·t·s⁻¹ = t² then t = 1.

The normal-product decomposition #

source
theorem Q2Presentation.Induction.TerminalBridge.mem_sup_of_normal_left (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) (hNn : N.Normal) (L : Subgroup Yt.Y) (x : Yt.Y) (hx : x ∈ N ⊔ L) :
∃ n ∈ N, ∃ l ∈ L, x = n * l

Elementwise decomposition of the join with a normal left factor.

source
theorem Q2Presentation.Induction.TerminalBridge.sup_normal_of_normal (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) (hNn : N.Normal) (L : Subgroup Yt.Y) (hLn : L.Normal) :
(N ⊔ L).Normal

The join of two normal subgroups is normal.

source
instance Q2Presentation.Induction.TerminalBridge.instSupLYNormal (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] :
(N ⊔ Yt.LY).Normal

The join with the wild kernel is normal (statement-level instance).

The odd kernel against the 2-group data #

source
theorem Q2Presentation.Induction.TerminalBridge.N_inf_LY_eq_bot (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) (hodd : Odd (Nat.card ↥N)) :
N ⊓ Yt.LY = ⊥

Odd ∩ 2-group is trivial: Ñ ⊓ L_Y = ⊥.

source
theorem Q2Presentation.Induction.TerminalBridge.pair_injective (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (y : Yt.Y) (hH : Yt.piY y = 1) (hQ : (QuotientGroup.mk' N) y = 1) :
y = 1

Injectivity of the pair (π_Y, ρ_Q).

source
theorem Q2Presentation.Induction.TerminalBridge.pair_surjective (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (y1 y2 : Yt.Y) (hagree : (QuotientGroup.mk' (N ⊔ Yt.LY)) y1 = (QuotientGroup.mk' (N ⊔ Yt.LY)) y2) :
∃ (y : Yt.Y), Yt.piY y = Yt.piY y1 ∧ (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y2

Fibre surjectivity of the pair: any H₂-agreeing pair of values is hit.

The decoration descends to Q #

source
theorem Q2Presentation.Induction.TerminalBridge.thetaY_kills_odd (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) (hodd : Odd (Nat.card ↥N)) (n : Yt.Y) (hn : n ∈ N) :
Yt.thetaY n = 1

Elements of odd-order subgroups die under the elementary decoration.

source
def Q2Presentation.Induction.TerminalBridge.thetaQ (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) :
Yt.Y ⧸ N →* Multiplicative Yt.E

The decoration descended to Q = Y/Ñ.

Equations
Instances For
    source
    @[simp]
    theorem Q2Presentation.Induction.TerminalBridge.thetaQ_mk (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (y : Yt.Y) :
    (thetaQ Yt N hodd) ((QuotientGroup.mk' N) y) = Yt.thetaY y
    source
    theorem Q2Presentation.Induction.TerminalBridge.surjective_of_projections (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) {G : Type u_1} [Group G] [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (f : G →* Yt.Y) (hH : Function.Surjective ⇑(Yt.piY.comp f)) (hQ : Function.Surjective ⇑((QuotientGroup.mk' N).comp f)) :
    Function.Surjective ⇑f

    Surjectivity transport: a hom whose H- and Q-projections are onto is onto (odd kernel against 2-group index; one CRT exponent).