The mod-2 Kummer class kˣ → H¹(k, 𝔽₂)

For a field k of characteristic ≠ 2 (we assume CharZero k, which covers ℚ₂ and all of its finite extensions — the fields the paper works over) and a ∈ kˣ, the Kummer class [a] is the class in H¹(G_k, 𝔽₂) of the explicit continuous 1-cocycle

κ_a : G_k → 𝔽₂, κ_a(g) = 0 if g·√a = √a, κ_a(g) = 1 if g·√a = −√a,

where √a is any square root of a in a fixed algebraic closure k̄. This is the connecting homomorphism of the Kummer short exact sequence 1 → μ₂ → k̄ˣ →^{(·)²} k̄ˣ → 1, specialized to n = 2, under the identification μ₂ = {±1} ⊆ k with 𝔽₂ = ZMod 2 (additive, with the trivial G_k-action, since ±1 ∈ k). See Serre, Galois Cohomology I §2 and Local Fields X, or Neukirch–Schmidt–Wingberg, Cohomology of Number Fields (Kummer theory H¹(k, μ_n) ≅ kˣ/(kˣ)ⁿ).

The Galois group is Mathlib's Field.absoluteGaloisGroup k = k̄ ≃ₐ[k] k̄ (the genuine Gal(k̄/k), k̄ = AlgebraicClosure k); we spell it out as GaloisGroup k (a reducible abbreviation, so that the MulAction on k̄ and the Krull topology are found by instance search). For k = ℚ₂ this is the project's AbsGalQ2 by definition (examples at the end certify this).

Conventions (review targets)

• Coefficients. 𝔽₂ := ZMod 2 with the trivial G_k-action (kummerTriv); the cocycle encodes the sign g·√a / √a ∈ {±1} as 0 / 1 ∈ ZMod 2. So H¹(G_k, 𝔽₂) = continuous homomorphisms G_k → 𝔽₂ (ContCoh.mem_Z1_iff_of_trivial).
• Cocycle sign. κ_a(g) = 0 ⟺ g fixes √a; κ_a(g) = 1 ⟺ g negates it. Root choice is irrelevant: κ for √a and for −√a is the same function (kummerCocycleFun_neg).

Main results (this file, all proved at the standard three axioms)

• kummerCocycleFun, kummerCocycle : ContCoh.Z1 (GaloisGroup k) (ZMod 2) — the explicit continuous 1-cocycle (continuity from openness of the stabilizer of √a in the Krull topology).
• kummerClass : kˣ → ContCoh.H1 (GaloisGroup k) (ZMod 2) — the Kummer class map.
• Stress tests: kummerCocycle_isHom (it is a continuous homomorphism), kummerClass_one ([1] = 0), kummerClass_mul ([ab] = [a] + [b], multiplicativity of the Kummer map), and kummerClass_eq_zero_iff ([a] = 0 ⟺ a is a square — injectivity of kˣ/(kˣ)² ↪ H¹, which uses the fixed-field theorem InfiniteGalois.mem_range_algebraMap_iff_fixed).

@[reducible, inline]

abbrev GQ2.Kummer.GaloisGroup (K : Type u_2) [Field K] : Type u_2

The absolute Galois group Gal(k̄/k) as k̄ ≃ₐ[k] k̄. A reducible abbreviation (so instance search sees the AlgEquiv action on k̄); definitionally Field.absoluteGaloisGroup K.

Equations

• GQ2.Kummer.GaloisGroup K = Gal(AlgebraicClosure K/K)

Coefficients: 𝔽₂ = ZMod 2 with the trivial action

@[implicit_reducible]

instance GQ2.Kummer.instDistribMulActionGaloisGroupZModOfNatNat {K : Type u_1} [Field K] : DistribMulAction (GaloisGroup K) (ZMod 2)

The trivial action of Gal(k̄/k) on 𝔽₂ = ZMod 2 (±1 ∈ k is fixed). This is the coefficient action for the Kummer class; no other action of an absolute Galois group on ZMod 2 exists, so registering it globally is safe.

Equations

• GQ2.Kummer.instDistribMulActionGaloisGroupZModOfNatNat = { smul := fun (x : GQ2.Kummer.GaloisGroup K) (m : ZMod 2) => m, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.Kummer.kummerTriv {K : Type u_1} [Field K] (g : GaloisGroup K) (m : ZMod 2) : g • m = m

The action on 𝔽₂ is trivial.

instance GQ2.Kummer.instContinuousSMulGaloisGroupZModOfNatNat {K : Type u_1} [Field K] : ContinuousSMul (GaloisGroup K) (ZMod 2)

The Kummer cocycle function and its pointwise algebra

noncomputable def GQ2.Kummer.kummerCocycleFun {K : Type u_1} [Field K] (α : AlgebraicClosure K) : GaloisGroup K → ZMod 2

The Kummer cocycle function κ : G_k → 𝔽₂ attached to a square root α = √a ∈ k̄: κ(g) = 0 if g fixes α, else 1.

Equations

• GQ2.Kummer.kummerCocycleFun α g = if g • α = α then 0 else 1

@[simp]

theorem GQ2.Kummer.kummerCocycleFun_eq0 {K : Type u_1} [Field K] {α : AlgebraicClosure K} {g : GaloisGroup K} (h : g • α = α) : kummerCocycleFun α g = 0

theorem GQ2.Kummer.alpha_ne_neg {K : Type u_1} [Field K] [CharZero K] {α : AlgebraicClosure K} {a : Kˣ} (hα : α ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a) : α ≠ -α

A square root of a unit is not its own negative (characteristic ≠ 2).

theorem GQ2.Kummer.kummerCocycleFun_eq1 {K : Type u_1} [Field K] [CharZero K] {α : AlgebraicClosure K} {a : Kˣ} (hα : α ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a) {g : GaloisGroup K} (h : g • α = -α) : kummerCocycleFun α g = 1

If α is a genuine square root of a unit a and g negates it, the cocycle reads 1 (here α ≠ -α, so g • α = -α really is ≠ α).

theorem GQ2.Kummer.two_values {K : Type u_1} [Field K] {α : AlgebraicClosure K} {a : Kˣ} (hα : α ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a) (g : GaloisGroup K) : g • α = α ∨ g • α = -α

The Galois image of a square root of a ∈ kˣ is ±√a.

theorem GQ2.Kummer.kummerCocycleFun_neg {K : Type u_1} [Field K] (α : AlgebraicClosure K) : kummerCocycleFun (-α) = kummerCocycleFun α

Changing the square root by a sign leaves the cocycle unchanged.

Continuity via the Krull topology

theorem GQ2.Kummer.stab_isClopen {K : Type u_1} [Field K] (α : AlgebraicClosure K) : IsClopen {g : GaloisGroup K | g • α = α}

{g | g • α = α} is (cl)open: it is the stabilizer of α, open in the Krull topology because k̄/k is algebraic (stabilizer_isOpen_of_isIntegral).

theorem GQ2.Kummer.kummerCocycleFun_continuous {K : Type u_1} [Field K] (α : AlgebraicClosure K) : Continuous (kummerCocycleFun α)

The cocycle is a continuous homomorphism

theorem GQ2.Kummer.kummerCocycleFun_hom {K : Type u_1} [Field K] [CharZero K] {α : AlgebraicClosure K} {a : Kˣ} (hα : α ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a) (g h : GaloisGroup K) : kummerCocycleFun α (g * h) = kummerCocycleFun α g + kummerCocycleFun α h

κ_a is a homomorphism: κ_a(gh) = κ_a(g) + κ_a(h). With the trivial action this is the 1-cocycle identity.

Packaging into Z¹ and H¹

noncomputable def GQ2.Kummer.kummerCocycle {K : Type u_1} [Field K] [CharZero K] {α : AlgebraicClosure K} {a : Kˣ} (hα : α ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a) : ↥(ContCoh.Z1 (GaloisGroup K) (ZMod 2))

The Kummer cocycle as an element of Z¹(G_k, 𝔽₂) (continuous 1-cocycles). Depends on a chosen square root α of the unit a.

Equations

• GQ2.Kummer.kummerCocycle hα = ⟨GQ2.Kummer.kummerCocycleFun α, ⋯⟩

noncomputable def GQ2.Kummer.sqrtOf {K : Type u_1} [Field K] (a : Kˣ) : AlgebraicClosure K

A fixed square root √a ∈ k̄ of a ∈ kˣ (exists as k̄ is algebraically closed).

Equations

• GQ2.Kummer.sqrtOf a = ⋯.choose

theorem GQ2.Kummer.sqrtOf_sq {K : Type u_1} [Field K] (a : Kˣ) : sqrtOf a ^ 2 = (algebraMap K (AlgebraicClosure K)) ↑a

noncomputable def GQ2.Kummer.kummerClass {K : Type u_1} [Field K] [CharZero K] (a : Kˣ) : ContCoh.H1 (GaloisGroup K) (ZMod 2)

The Kummer class [a] ∈ H¹(G_k, 𝔽₂) of a unit a ∈ kˣ.

Equations

• GQ2.Kummer.kummerClass a = (GQ2.ContCoh.H1mk (GQ2.Kummer.GaloisGroup K) (ZMod 2)) (GQ2.Kummer.kummerCocycle ⋯)

Stress tests

theorem GQ2.Kummer.H1mk_eq_zero_iff {K : Type u_1} [Field K] {z : ↥(ContCoh.Z1 (GaloisGroup K) (ZMod 2))} : (ContCoh.H1mk (GaloisGroup K) (ZMod 2)) z = 0 ↔ ↑z = 0

Auxiliary: under the trivial action, [z] = 0 in H¹ iff the cocycle z is the zero function (B¹ = ⊥).

theorem GQ2.Kummer.kummerClass_eq_zero_iff {K : Type u_1} [Field K] [CharZero K] (a : Kˣ) : kummerClass a = 0 ↔ IsSquare a

Stress test (injectivity of kˣ/(kˣ)² ↪ H¹). [a] = 0 iff a is a square in kˣ. The nontrivial direction uses that the fixed field of G_k is k (InfiniteGalois.mem_range_algebraMap_iff_fixed, valid since k̄/k is Galois for perfect k).

AbsGalQ2 sanity checks (faithfulness anchor)

For k = ℚ₂, GaloisGroup ℚ₂ is definitionally Field.absoluteGaloisGroup ℚ₂, i.e. the project's AbsGalQ2; so kummerClass (K := ℚ_[2]) is literally the Kummer map into H¹(G_ℚ₂, 𝔽₂).