The Kummer class of a unit as the class of a character

Let K be a field and G_K = AbsoluteGaloisGroup K. For r ∈ Kˢ the sign rootSign r g ∈ 𝔽₂ records whether g ∈ G_K moves r. When r² = b lies in K, every g sends r to ±r, so g ↦ rootSign r g is a continuous homomorphism G_K → 𝔽₂, the Kummer character of b (TauCeti.kummerCharacter). It is the Kummer cocycle g ↦ g r / r ∈ μ₂ of TauCeti.kummerCocycleModTwo read in 𝔽₂, and when 2 is invertible in K the Kummer class (b) ∈ H¹(G_K, 𝔽₂) is the class TauCeti.ContCohomology.homClass of this character (TauCeti.kummerClass_eq_homClass). This pins the Kummer class at cochain level: an explicit cocycle computation with Kummer classes, such as a cup product of two of them or an Evens norm, can be carried out on the characters rootSign r.

For a finite extension L/K with an embedding σ : L → Kˢ, the same construction on the open subgroup G_L = galoisSubgroup K L σ of G_K gives the Kummer character TauCeti.galoisKummerCharacter σ a r of a ∈ Lˣ, for a square root r of σ a, and the Kummer class of a, carried from G_L to galoisSubgroup K L σ by TauCeti.galoisF2Iso, is its class (TauCeti.galoisF2Iso_inv_kummerClass).

Main definitions

• TauCeti.rootSign r g: 0 when g r = r and 1 otherwise.
• TauCeti.kummerCharacter b r hr: the Kummer character g ↦ rootSign r g of b = r².
• TauCeti.galoisKummerCharacter σ a r hr: the Kummer character of a ∈ Lˣ on galoisSubgroup K L σ, for r² = σ a.

Main results

• TauCeti.continuous_rootSign, TauCeti.continuous_kummerCharacter, TauCeti.continuous_galoisKummerCharacter: the characters are continuous.
• TauCeti.kummerClass_eq_homClass: the Kummer class of b is the class of its Kummer character.
• TauCeti.galoisF2Iso_inv_kummerClass: the Kummer class of a ∈ Lˣ, carried to galoisSubgroup K L σ, is the class of its Kummer character there.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1): the Kummer map sends b to the class of g ↦ g r / r.

The sign of a root

noncomputable def TauCeti.rootSign {K : Type u} [Field K] (r : SeparableClosure K) (g : AbsoluteGaloisGroup K) : ZMod 2

The sign of r under g: rootSign r g is 0 when g fixes r and 1 otherwise. When r ≠ 0, r² ∈ K, and 2 is invertible in K, it is the Kummer cocycle g ↦ g r / r ∈ μ₂ read in 𝔽₂.

Equations

• TauCeti.rootSign r g = if g r = r then 0 else 1

@[simp]

theorem TauCeti.rootSign_of_apply_eq {K : Type u} [Field K] {r : SeparableClosure K} {g : AbsoluteGaloisGroup K} (h : g r = r) : rootSign r g = 0

The sign of a root that g fixes is 0.

@[simp]

theorem TauCeti.rootSign_of_apply_ne {K : Type u} [Field K] {r : SeparableClosure K} {g : AbsoluteGaloisGroup K} (h : g r ≠ r) : rootSign r g = 1

The sign of a root that g moves is 1.

@[simp]

theorem TauCeti.rootSign_eq_zero_iff {K : Type u} [Field K] {r : SeparableClosure K} {g : AbsoluteGaloisGroup K} : rootSign r g = 0 ↔ g r = r

The sign of r under g vanishes exactly when g fixes r.

@[simp]

theorem TauCeti.rootSign_eq_one_iff {K : Type u} [Field K] {r : SeparableClosure K} {g : AbsoluteGaloisGroup K} : rootSign r g = 1 ↔ g r ≠ r

The sign of r under g is 1 exactly when g moves r.

@[simp]

theorem TauCeti.rootSign_one {K : Type u} [Field K] (r : SeparableClosure K) : rootSign r 1 = 0

The sign of r under the identity is 0.

theorem TauCeti.rootSign_mul {K : Type u} [Field K] {r : SeparableClosure K} {g h : AbsoluteGaloisGroup K} (hg : g r = r ∨ g r = -r) (hh : h r = r ∨ h r = -r) : rootSign r (g * h) = rootSign r g + rootSign r h

The sign of a root is additive on the elements that send r to ±r.

theorem TauCeti.continuous_rootSign {K : Type u} [Field K] (r : SeparableClosure K) : Continuous (rootSign r)

The sign of a root is continuous: its fibres are the stabilizer of r, which is open for the Krull topology, and its complement.

The Kummer character of a unit

noncomputable def TauCeti.kummerCharacter {K : Type u} [Field K] (b : Kˣ) (r : SeparableClosure K) (hr : r ^ 2 = (algebraMap K (SeparableClosure K)) ↑b) : AbsoluteGaloisGroup K →* Multiplicative (ZMod 2)

The Kummer character of b ∈ Kˣ, g ↦ rootSign r g for a square root r of b in Kˢ. It is a homomorphism because every g sends r to ±r.

Equations

• TauCeti.kummerCharacter b r hr = { toFun := fun (g : TauCeti.AbsoluteGaloisGroup K) => Multiplicative.ofAdd (TauCeti.rootSign r g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.toAdd_kummerCharacter {K : Type u} [Field K] (b : Kˣ) (r : SeparableClosure K) (hr : r ^ 2 = (algebraMap K (SeparableClosure K)) ↑b) (g : AbsoluteGaloisGroup K) : Multiplicative.toAdd ((kummerCharacter b r hr) g) = rootSign r g

The value of the Kummer character at g is the sign of r under g.

theorem TauCeti.continuous_kummerCharacter {K : Type u} [Field K] (b : Kˣ) (r : SeparableClosure K) (hr : r ^ 2 = (algebraMap K (SeparableClosure K)) ↑b) : Continuous ⇑(kummerCharacter b r hr)

The Kummer character is continuous: the stabilizer of r is open.

theorem TauCeti.kummerClass_eq_homClass {K : Type u} [Field K] [Invertible 2] (b : Kˣ) (r : SeparableClosure K) (hr : r ^ 2 = (algebraMap K (SeparableClosure K)) ↑b) : kummerClass b = ContCohomology.homClass (AbsoluteGaloisGroup K) (kummerCharacter b r hr) ⋯

The Kummer class is the class of the Kummer character. If r² = b, the Kummer class (b) ∈ H¹(G_K, 𝔽₂) is the class of the continuous homomorphism g ↦ rootSign r g.

The Kummer character over a finite extension

theorem TauCeti.apply_eq_or_eq_neg_of_sq_eq_galoisSubgroup {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {a : L} {r : SeparableClosure K} (hr : r ^ 2 = σ a) (γ : ↥↑(galoisSubgroup K L σ)) : ↑γ r = r ∨ ↑γ r = -r

Every element of galoisSubgroup K L σ sends a square root of σ a to ± itself.

noncomputable def TauCeti.galoisKummerCharacter {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) : ↥↑(galoisSubgroup K L σ) →* Multiplicative (ZMod 2)

The Kummer character of a ∈ Lˣ on G_L = galoisSubgroup K L σ, γ ↦ rootSign r γ for a square root r of σ a: every γ in G_L fixes σ L, hence r², so γ r = ±r.

Equations

• TauCeti.galoisKummerCharacter σ a r hr = { toFun := fun (γ : ↥↑(TauCeti.galoisSubgroup K L σ)) => Multiplicative.ofAdd (TauCeti.rootSign r ↑γ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.toAdd_galoisKummerCharacter {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (γ : ↥↑(galoisSubgroup K L σ)) : Multiplicative.toAdd ((galoisKummerCharacter σ a r hr) γ) = rootSign r ↑γ

The value of the Kummer character of a at γ is the sign of r under γ.

theorem TauCeti.continuous_galoisKummerCharacter {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) : Continuous ⇑(galoisKummerCharacter σ a r hr)

The Kummer character of a on G_L is continuous.

theorem TauCeti.galoisF2Iso_inv_kummerClass {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) : (CategoryTheory.ConcreteCategory.hom (galoisF2Iso K L σ 1).inv) (kummerClass a) = ContCohomology.homClass (↥↑(galoisSubgroup K L σ)) (galoisKummerCharacter σ a r hr) ⋯

The Kummer class of a ∈ Lˣ, carried to galoisSubgroup K L σ, is the class of its Kummer character: for a square root r of σ a, the transported class is represented by the character γ ↦ rootSign r γ.