Documentation

GQ2.KummerSurjectivity

Surjectivity of kummerClassK #

This file proves GQ2.kummerClassK_surjective, the former B12 axiom interface, in-repo.

This file is the hom/kernel layer (B12-1): it turns a degree-1 class c โˆˆ Hยน(G_k, ๐”ฝโ‚‚) โ€” via H1mk_surjective, some cocycle z โˆˆ Zยน โ€” into an open, index-2 subgroup of G_k = k.fixingSubgroup (its kernel, when z โ‰  0), plus the bookkeeping needed to reconnect a Kummer cocycle to z at the end (eq_of_zero_set, mem_zHom_ker) and the z = 0 base case (kummerClassK_one). It lives strictly upstream of Foundations/Axioms.lean (imports only GQ2.EvensKahn + Mathlib) so the eventual flip is the zero-churn B11 pattern.

The Krull bridge GQ2.KummerKrullBridge.exists_quadratic_of_open_index_two consumes zHom_ker_isOpen and zHom_index_ker to produce the quadratic subextension. The capstone is assembled below as kummerClassK_surjective' after five private field-theory ports; Foundations/Axioms.lean exposes it under the public interface name.

source
theorem GQ2.KummerSurjectivity.fixingSubgroup_smul_zmod_two_eq_self (k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])) (g : โ†ฅk.fixingSubgroup) (m : ZMod 2) :
g โ€ข m = m

The k.fixingSubgroup-action on ZMod 2 is trivial (it factors through Kummer's trivial action on ๐”ฝโ‚‚). This is the htriv input of mem_Z1_iff_of_trivial for G = G_k.

source
noncomputable def GQ2.KummerSurjectivity.zHom (k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])) (z : โ†ฅ(ContCoh.Z1 (โ†ฅk.fixingSubgroup) (ZMod 2))) :
โ†ฅk.fixingSubgroup โ†’* Multiplicative (ZMod 2)

A degree-1 cocycle z โˆˆ Zยน(G_k, ๐”ฝโ‚‚) as a genuine group homomorphism G_k โ†’* Multiplicative (ZMod 2) (trivial action โ‡’ z is additive, Z1_apply_one โ‡’ z 1 = 0). Its kernel is the index-2 subgroup that the Krull bridge (B12-2) turns into a quadratic subextension.

Equations
  • GQ2.KummerSurjectivity.zHom k z = { toFun := fun (g : โ†ฅk.fixingSubgroup) => Multiplicative.ofAdd (โ†‘z g), map_one' := โ‹ฏ, map_mul' := โ‹ฏ }
Instances For
    source
    theorem GQ2.KummerSurjectivity.mem_zHom_ker {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} {z : โ†ฅ(ContCoh.Z1 (โ†ฅk.fixingSubgroup) (ZMod 2))} {g : โ†ฅk.fixingSubgroup} :
    g โˆˆ (zHom k z).ker โ†” โ†‘z g = 0

    The kernel of zHom is exactly the zero-set of the cocycle.

    source
    theorem GQ2.KummerSurjectivity.zHom_ker_isOpen {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} (z : โ†ฅ(ContCoh.Z1 (โ†ฅk.fixingSubgroup) (ZMod 2))) :
    IsOpen โ†‘(zHom k z).ker

    The kernel of zHom is open: it is the preimage of the (open, discrete) point {0} under the continuous cocycle z.

    source
    theorem GQ2.KummerSurjectivity.zHom_surjective {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} {z : โ†ฅ(ContCoh.Z1 (โ†ฅk.fixingSubgroup) (ZMod 2))} (hz : โ†‘z โ‰  0) :
    Function.Surjective โ‡‘(zHom k z)

    When the cocycle is nonzero, zHom is surjective (its 2-element codomain leaves no room for a proper nontrivial image).

    source
    theorem GQ2.KummerSurjectivity.zHom_index_ker {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} {z : โ†ฅ(ContCoh.Z1 (โ†ฅk.fixingSubgroup) (ZMod 2))} (hz : โ†‘z โ‰  0) :
    (zHom k z).ker.index = 2

    When the cocycle is nonzero, the kernel has index 2.

    source
    theorem GQ2.KummerSurjectivity.eq_of_zero_set {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} {f f' : โ†ฅk.fixingSubgroup โ†’ ZMod 2} (h : โˆ€ (g : โ†ฅk.fixingSubgroup), f g = 0 โ†” f' g = 0) :
    f = f'

    Two ๐”ฝโ‚‚-valued functions with the same zero-set are equal (the only nonzero value is 1). This reconnects a Kummer cocycle to z in the capstone (B12-3): equal kernels โ‡’ equal cocycles โ‡’ equal Hยน-classes.

    source
    theorem GQ2.KummerSurjectivity.kummerClassK_one {k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])} :
    kummerClassK k 1 = 0

    The z = 0 base case. [1] = 0: the Kummer class of the unit 1 vanishes. Ported (direct proof) from HilbertLedger.kummerClassK_one, which is downstream of the axiom file. sqrtCl 1 is a square root of 1 in โ„šฬ„โ‚‚, hence ยฑ1 โˆˆ โ„šโ‚‚, hence Galois-fixed, so the cocycle is identically 0.

    B12-3: private field-theory ports + the capstone #

    Ports (verbatim-modulo-namespace) of the field-theory lemmas the capstone needs, from files that sit downstream of Foundations/Axioms.lean: fixingSubgroup_adjoin_simple, mem_bot_iff_mem, exists_sqrt_generator, fixingSubgroup_subgroupOf_eq_stabilizer (GQ2/QuadraticAdjoin.lean) and kcf_root_indep' (GQ2/HilbertLedger.lean). Kept private so they cannot clash with the downstream originals or with B12-2's private degree lemmas. The B12-2 Krull bridge exists_quadratic_of_open_index_two is imported from GQ2.KummerKrullBridge (same namespace).

    source
    theorem GQ2.KummerSurjectivity.kummerClassK_surjective' (k : IntermediateField โ„š_[2] (AlgebraicClosure โ„š_[2])) [FiniteDimensional โ„š_[2] โ†ฅk] :
    Function.Surjective (kummerClassK k)

    The capstone (B12-3): every degree-1 class c โˆˆ Hยน(G_k, ๐”ฝโ‚‚) is a Kummer class kummerClassK k a. If the representing cocycle z is 0, c = kummerClassK k 1; otherwise its kernel is an open index-2 subgroup, which the B12-2 bridge turns into a quadratic L = kโŸฎฮดโŸฏ, and completing the square exhibits d โˆˆ kหฃ whose Kummer cocycle vanishes on exactly ker z = Stab ฮด โ€” so, both being ๐”ฝโ‚‚-homs, kummerClassK k d = c. Consumed by Foundations/Axioms.lean at the The theorem is exposed under the former interface name, so downstream consumers require no special adapter.