Galois symbol $(F^\times)^n \to H^n(F,\mathbb{Z}/2)$

Definition

MilnorConjecture_GaloisSymbol

by vatsj · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebragalois-cohomologykummer-theory

Let $F$ be a field with $\operatorname{char} F \neq 2$ , $F^{\mathrm{sep}}$ a separable closure and $G_F = \operatorname{Gal}(F^{\mathrm{sep}}/F)$ with its Krull topology. Write $H^n(F,\mathbb{Z}/2) = H^n_{\mathrm{cts}}(G_F,\mathbb{Z}/2)$ for continuous cohomology with trivial coefficients $\mathbb{Z}/2 \cong \mu_2$ .

For $a \in F^\times$ fix a square root $\sqrt a \in F^{\mathrm{sep}}$ . The Kummer character is

\chi_a(\sigma) = \begin{cases}0 & \sigma(\sqrt a) = \sqrt a,\\ 1 & \text{otherwise,}\end{cases}

a continuous homomorphism $G_F\to\mathbb{Z}/2$ representing the Kummer class $\delta a \in H^1(F,\mu_2)$ (the boundary of the Kummer sequence). For $a_1,\dots,a_n\in F^\times$ , the Galois symbol is the class of the homogeneous cocycle

(x_0,\dots,x_n) \longmapsto \prod_{j=1}^{n}\bigl(\chi_{a_j}(x_j) - \chi_{a_j}(x_{j-1})\bigr) \;\in\; H^n(F,\mathbb{Z}/2),

the homogeneous form of $(\sigma_1,\dots,\sigma_n)\mapsto \chi_{a_1}(\sigma_1)\cdots\chi_{a_n}(\sigma_n)$ , i.e. the cup product $\delta a_1 \cup \cdots \cup \delta a_n$ . For $n = 0$ it is the class of the constant $1$ .

These are exactly the values of the norm residue homomorphism on symbols.

Formalization Note H F n, kummerChar a and galoisSymbol a are sorry-free; continuity, additivity, invariance and the cocycle identity are proved in the file. The class does not depend on the choice of $\sqrt a$ , since $\chi_a$ does not.

Definition code

import Mathlib
import Definitions.Def_MilnorConjecture_HomogeneousCochains

/-!
# The Galois symbol `(F^×)ⁿ → Hⁿ(F, ℤ/2)`

For a field `F` with `2 ≠ 0` in `F`, write `F^sep` for its separable closure and
`G_F = Gal(F^sep/F)` for the absolute Galois group with its Krull topology. For `a ∈ F^×` fix a
square root `√a ∈ F^sep` and let `χ_a : G_F → ℤ/2` be the Kummer character,
`χ_a(σ) = 0` if `σ(√a) = √a` and `χ_a(σ) = 1` otherwise.

The Galois symbol of `(a₁, …, aₙ)` is the class in `Hⁿ_cts(G_F, ℤ/2)` of the homogeneous
cocycle `(x₀, …, xₙ) ↦ ∏ⱼ (χ_{aⱼ}(xⱼ) - χ_{aⱼ}(xⱼ₋₁))`, which is the homogeneous form of the
inhomogeneous cocycle `(σ₁, …, σₙ) ↦ χ_{a₁}(σ₁) ⋯ χ_{aₙ}(σₙ)`, i.e. of the cup product
`δa₁ ∪ ⋯ ∪ δaₙ` of Kummer classes.
-/

namespace MilnorConjecture

section Cochain

variable {G R : Type*} [CommRing R]

/-- Function-level homogeneous coboundary `(δf)(y) = ∑ᵢ (-1)ⁱ f(y ∘ ∂ᵢ)`. -/
def fcob {m : ℕ} (f : (Fin m → G) → R) (y : Fin (m + 1) → G) : R :=
  ∑ i : Fin (m + 1), (-1 : R) ^ (i : ℕ) * f (y ∘ i.succAbove)

/-- `(x₀, …, xₙ) ↦ ∏ⱼ (χⱼ(xⱼ) - χⱼ(xⱼ₋₁))` for functions `χ₁, …, χₙ : G → R`. -/
def prodCochain {n : ℕ} (χ : Fin n → G → R) (x : Fin (n + 1) → G) : R :=
  ∏ j : Fin n, (χ j (x j.succ) - χ j (x j.castSucc))

lemma prodCochain_succ {n : ℕ} (χ : Fin (n + 1) → G → R) (x : Fin (n + 2) → G) :
    prodCochain χ x = (χ 0 (x 1) - χ 0 (x 0)) * prodCochain (Fin.tail χ) (Fin.tail x) := by
  rw [prodCochain, Fin.prod_univ_succ]
  rfl

/-- Leibniz rule for multiplying by the coboundary of a `0`-cochain:
`δ(δχ · Ψ) = -(δχ · δΨ)`. -/
lemma fcob_mul_tail {m : ℕ} (χ : G → R) (Ψ : (Fin (m + 1) → G) → R) (y : Fin (m + 3) → G) :
    fcob (fun x : Fin (m + 2) → G ↦ (χ (x 1) - χ (x 0)) * Ψ (Fin.tail x)) y =
      -((χ (y 1) - χ (y 0)) * fcob Ψ (Fin.tail y)) := by
  simp only [fcob]
  rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fin.sum_univ_succ (n := m + 1), mul_add, neg_add,
    ← add_assoc]
  congr 1
  · have h1 : (Fin.succ 0 : Fin (m + 3)).succAbove 1 = 2 := by
      rw [show (1 : Fin (m + 2)) = Fin.succ 0 from rfl, Fin.succ_succAbove_succ]; rfl
    have h2 : Fin.tail (y ∘ (Fin.succ 0 : Fin (m + 3)).succAbove) = fun i ↦ y i.succ.succ := by
      funext i
      simp only [Fin.tail, Function.comp_apply, Fin.succ_succAbove_succ, Fin.succAbove_zero]
    simp only [Function.comp_apply, h1, h2, Fin.succ_succAbove_zero, Fin.succAbove_zero]
    have e3 : Fin.tail (y ∘ Fin.succ) = fun i ↦ y i.succ.succ := rfl
    have e4 : Fin.tail y ∘ Fin.succ = fun i ↦ y i.succ.succ := rfl
    rw [Fin.succ_one_eq_two, Fin.succ_zero_eq_one, e3, e4]
    simp only [Fin.val_one, Fin.val_zero, pow_one, pow_zero, one_mul]
    ring
  · rw [Finset.mul_sum, ← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun j _ ↦ ?_
    have h0 : (y ∘ j.succ.succ.succAbove) 0 = y 0 := by simp
    have h1 : (y ∘ j.succ.succ.succAbove) 1 = y 1 := by
      rw [Function.comp_apply, ← Fin.succ_zero_eq_one, Fin.succ_succAbove_succ,
        Fin.succ_succAbove_zero, Fin.succ_zero_eq_one]
    have h2 : Fin.tail (y ∘ j.succ.succ.succAbove) = Fin.tail y ∘ j.succ.succAbove := by
      funext i
      simp only [Fin.tail, Function.comp_apply, Fin.succ_succAbove_succ]
    rw [h0, h1, h2]
    simp only [Fin.val_succ]
    ring

lemma fcob_prodCochain {n : ℕ} (χ : Fin n → G → R) (y : Fin (n + 2) → G) :
    fcob (prodCochain χ) y = 0 := by
  induction n with
  | zero => simp [fcob, prodCochain, Fin.sum_univ_two]
  | succ n ih =>
    have : prodCochain χ =
        fun x ↦ (χ 0 (x 1) - χ 0 (x 0)) * prodCochain (Fin.tail χ) (Fin.tail x) :=
      funext (prodCochain_succ χ)
    rw [this, fcob_mul_tail, ih, mul_zero, neg_zero]

end Cochain

variable (F : Type) [Field F]

/-- The absolute Galois group `Gal(F^sep/F)`, with its Krull topology. -/
abbrev AbsGal : Type := Gal(SeparableClosure F/F)

/-- `Hⁿ(F, ℤ/2) := Hⁿ_cts(Gal(F^sep/F), ℤ/2)`, with `ℤ/2` a trivial representation. -/
abbrev H (n : ℕ) : Type := continuousCohomology n (trivialRep (ZMod 2) (AbsGal F) (ZMod 2))

variable [NeZero (2 : F)] {F}

instance : NeZero ((2 : ℕ) : SeparableClosure F) :=
  ⟨by
    rw [Nat.cast_ofNat, ← map_ofNat (algebraMap F (SeparableClosure F)) 2]
    exact (map_ne_zero _).mpr (NeZero.ne (2 : F))⟩

/-- A chosen square root of `a` in `F^sep`. -/
noncomputable def sqrtSep (a : Fˣ) : SeparableClosure F :=
  (IsSepClosed.exists_pow_nat_eq (algebraMap F (SeparableClosure F) a) 2).choose

lemma sqrtSep_sq (a : Fˣ) : sqrtSep a ^ 2 = algebraMap F (SeparableClosure F) a :=
  (IsSepClosed.exists_pow_nat_eq (algebraMap F (SeparableClosure F) a) 2).choose_spec

/-- The Kummer character `χ_a : Gal(F^sep/F) → ℤ/2`: `χ_a(σ) = 0` iff `σ(√a) = √a`. -/
noncomputable def kummerCharFun (a : Fˣ) (σ : AbsGal F) : ZMod 2 :=
  by classical exact if σ (sqrtSep a) = sqrtSep a then 0 else 1

lemma sqrtSep_ne_zero (a : Fˣ) : sqrtSep a ≠ 0 := by
  intro h
  have := sqrtSep_sq a
  rw [h, zero_pow two_ne_zero, eq_comm, map_eq_zero] at this
  exact a.ne_zero this

lemma neg_sqrtSep_ne (a : Fˣ) : -sqrtSep a ≠ sqrtSep a := by
  intro h
  have h2 : (2 : SeparableClosure F) * sqrtSep a = 0 := by rw [two_mul]; nth_rw 1 [← h]; ring
  rcases mul_eq_zero.mp h2 with h2 | h2
  · exact NeZero.ne ((2 : ℕ) : SeparableClosure F) (by exact_mod_cast h2)
  · exact sqrtSep_ne_zero a h2

lemma apply_sqrtSep (a : Fˣ) (σ : AbsGal F) :
    σ (sqrtSep a) = sqrtSep a ∨ σ (sqrtSep a) = -sqrtSep a := by
  apply sq_eq_sq_iff_eq_or_eq_neg.mp
  rw [← map_pow, sqrtSep_sq, AlgEquiv.commutes]

lemma kummerCharFun_mul (a : Fˣ) (σ τ : AbsGal F) :
    kummerCharFun a (σ * τ) = kummerCharFun a σ + kummerCharFun a τ := by
  have hne := neg_sqrtSep_ne a
  rcases apply_sqrtSep a τ with hτ | hτ <;> rcases apply_sqrtSep a σ with hσ | hσ <;>
    simp [kummerCharFun, AlgEquiv.mul_apply, hτ, hσ, map_neg, hne]
  decide

lemma continuous_kummerCharFun (a : Fˣ) : Continuous (kummerCharFun a) := by
  let S := MulAction.stabilizer (AbsGal F) (sqrtSep a)
  have hS : ∀ σ : AbsGal F, σ ∈ S ↔ σ (sqrtSep a) = sqrtSep a := fun σ ↦ Iff.rfl
  let E := IntermediateField.adjoin F {sqrtSep a}
  have : FiniteDimensional F E :=
    IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (sqrtSep a))
  have hle : E.fixingSubgroup ≤ S := fun σ hσ ↦
    (hS σ).mpr ((IntermediateField.mem_fixingSubgroup_iff E σ).mp hσ _
      (IntermediateField.mem_adjoin_simple_self F _))
  have hopen : IsOpen (S : Set (AbsGal F)) := Subgroup.isOpen_mono hle E.fixingSubgroup_isOpen
  have hclosed : IsClosed (S : Set (AbsGal F)) := Subgroup.isClosed_of_isOpen S hopen
  apply IsLocallyConstant.continuous
  rw [IsLocallyConstant.iff_isOpen_fiber_apply]
  intro σ
  by_cases hσ : σ (sqrtSep a) = sqrtSep a
  · convert hopen using 1
    ext τ
    by_cases hτ : τ (sqrtSep a) = sqrtSep a <;> simp [kummerCharFun, hS, hσ, hτ]
  · convert hclosed.isOpen_compl using 1
    ext τ
    by_cases hτ : τ (sqrtSep a) = sqrtSep a <;> simp [kummerCharFun, hS, hσ, hτ]

/-- The Kummer character as a continuous map. -/
noncomputable def kummerChar (a : Fˣ) : C(AbsGal F, ZMod 2) :=
  ⟨kummerCharFun a, continuous_kummerCharFun a⟩

/-- The homogeneous cocycle `(x₀, …, xₙ) ↦ ∏ⱼ (χ_{aⱼ}(xⱼ) - χ_{aⱼ}(xⱼ₋₁))`. -/
noncomputable def symbolCochain {n : ℕ} (a : Fin n → Fˣ) : C(Fin (n + 1) → AbsGal F, ZMod 2) :=
  ⟨prodCochain (fun j ↦ kummerChar (a j)), by
    unfold prodCochain; fun_prop⟩

lemma symbolCochain_invariant {n : ℕ} (a : Fin n → Fˣ) (g : AbsGal F)
    (v : Fin (n + 1) → AbsGal F) : symbolCochain a (fun i ↦ g * v i) = symbolCochain a v := by
  simp only [symbolCochain, ContinuousMap.coe_mk, prodCochain, kummerChar, kummerCharFun_mul]
  congr 1; funext j; ring

lemma coboundary_symbolCochain {n : ℕ} (a : Fin n → Fˣ) :
    coboundary (n + 1) (symbolCochain a) = 0 := by
  ext y
  rw [coboundary_apply, ContinuousMap.zero_apply]
  have := fcob_prodCochain (fun j ↦ kummerChar (a j)) y
  simpa [fcob, symbolCochain, zsmul_eq_mul] using this

/-- The Galois symbol `(a₁, …, aₙ) ↦ δa₁ ∪ ⋯ ∪ δaₙ ∈ Hⁿ(F, ℤ/2)`. -/
noncomputable def galoisSymbol {n : ℕ} (a : Fin n → Fˣ) : H F n :=
  classOf (ZMod 2) n (symbolCochain a) (symbolCochain_invariant a) (coboundary_symbolCochain a)

end MilnorConjecture

Source

V. Voevodsky, Motivic cohomology with Z/2-coefficients, Publ. Math. IHES 98 (2003), 59-104, https://doi.org/10.1007/s10240-003-0010-6, p. 59 (Introduction, eqs. (1)-(3)): the Kummer boundary k^* -> H^1(k, mu_2) and its multiplicative extension K^M_*(k) -> H^*(k, mu_2^{(x)*}).

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `Def_MilnorConjecture_GaloisSymbol`

Everything lives in the namespace MilnorConjecture. The file imports Mathlib and the bundle file Def_MilnorConjecture_HomogeneousCochains, whose relevant definitions are unfolded below where used.

Imported bundle definitions (unfolded)

In the imported file, $k, G, M$ are types in one common universe with: $k$ a ring with a topology; $G$ a group with a topology making it a topological group, and locally compact; $M$ an additive commutative group, a $k$ -module, with a topology making it a topological additive group, with continuous scalar multiplication $k \times M \to M$ . For classOf one additionally assumes $k$ is a topological ring.

trivialRep k G M is the topological $k$ -linear representation of $G$ on $M$ in which every $g \in G$ acts as the identity.
coboundary n F: for a continuous $F : G^n \to M$ , it is the continuous function $G^{n+1} \to M$

(\partial F)(y_0,\dots,y_n) = \sum_{i=0}^{n} (-1)^i\, F(y_0,\dots,\widehat{y_i},\dots,y_n),

where the hat means the $i$ -th coordinate is deleted (the $(-1)^i$ acts as an integer multiple).

curryN n F: for continuous $F : G^n \to M$ , it is the iterated currying $x_0 \mapsto (x_1 \mapsto (\cdots \mapsto F(x_0,\dots,x_{n-1})))$ , an element of the $n$ -th term $X_n$ of Mathlib's resolution, where $X_0 = M$ and $X_{m+1} = C(G, X_m)$ (continuous maps). For $n=0$ it is the value of $F$ at the empty tuple.
Mathlib's cochain complex. On $C(G,V)$ the group acts by $(g\cdot f)(x) = g\cdot f(g^{-1}x)$ ; the differentials of the resolution are $d_0(m) =$ the constant function $m$ , and $d_{m+1}(f) = (x \mapsto f) - (x \mapsto d_m(f(x)))$ . Mathlib's continuous cohomology $H^n_{\mathrm{cts}}(G, A)$ (continuousCohomology n A) is the degree- $n$ cohomology of the complex of $G$ -invariants of $X_1 \to X_2 \to X_3 \to \cdots$ (degree $n$ sitting on $X_{n+1}$ ), as a topological $k$ -module.
classOf k n F hinv hcoc: given continuous $F : G^{n+1}\to M$ with $F(gv_0,\dots,gv_n) = F(v_0,\dots,v_n)$ for all $g, v$ (hypothesis hinv) and $\partial F = 0$ as a function on $G^{n+2}$ (hypothesis hcoc), it is the cohomology class in $H^n_{\mathrm{cts}}(G, \text{trivialRep}\ k\ G\ M)$ of the invariant cocycle $\mathrm{curryN}_{n+1}(F) \in X_{n+1}^G$ . (Formally: the cycle obtained by lifting the map $k \to X_{n+1}^G$ , $1 \mapsto \mathrm{curryN}_{n+1}(F)$ , evaluated at $1$ , then projected to homology.)

Section `Cochain`

Variables in scope for this section: arbitrary types $G$ and $R$ (no structure at all on $G$ ), with $R$ a commutative ring.

fcob. For $m \in \mathbb{N}$ , a function $f : G^m \to R$ and $y \in G^{m+1}$ ,

\mathrm{fcob}(f)(y) = \sum_{i=0}^{m} (-1)^i\, f(y_0,\dots,\widehat{y_i},\dots,y_m) \in R,

(a plain, non-continuous version of the alternating face sum; y ∘ i.succAbove is $y$ with coordinate $i$ removed).

prodCochain. For $n \in \mathbb{N}$ , a family $\chi = (\chi_0,\dots,\chi_{n-1})$ of functions $\chi_j : G \to R$ , and $x = (x_0,\dots,x_n) \in G^{n+1}$ ,

\mathrm{prodCochain}(\chi)(x) = \prod_{j=0}^{n-1}\bigl(\chi_j(x_{j+1}) - \chi_j(x_j)\bigr).

Here the factor for index $j$ uses the coordinate $x_{j+1}$ (x j.succ) minus the coordinate $x_j$ (x j.castSucc). For $n = 0$ the product is empty, so $\mathrm{prodCochain}(\chi)$ is the constant function $1$ on $G^1$ .

Lemma prodCochain_succ. For $\chi : \{0,\dots,n\} \to (G \to R)$ and $x \in G^{n+2}$ :

\mathrm{prodCochain}(\chi)(x) = \bigl(\chi_0(x_1) - \chi_0(x_0)\bigr)\cdot \mathrm{prodCochain}(\chi_1,\dots,\chi_n)(x_1,\dots,x_{n+1}).

Lemma fcob_mul_tail. For $m \in \mathbb{N}$ , $\chi : G \to R$ , $\Psi : G^{m+1} \to R$ , $y \in G^{m+3}$ : letting $f(x) = (\chi(x_1)-\chi(x_0))\,\Psi(x_1,\dots,x_{m+1})$ for $x \in G^{m+2}$ ,

\mathrm{fcob}(f)(y) = -\Bigl(\bigl(\chi(y_1) - \chi(y_0)\bigr)\cdot \mathrm{fcob}(\Psi)(y_1,\dots,y_{m+2})\Bigr).

Lemma fcob_prodCochain. For every $n \in \mathbb{N}$ , every $\chi : \{0,\dots,n-1\} \to (G \to R)$ and every $y \in G^{n+2}$ : $\mathrm{fcob}(\mathrm{prodCochain}(\chi))(y) = 0$ .

Field-level declarations

After the section, $F$ is a type (in the lowest universe) that is a field. Initially $F$ is an explicit parameter.

AbsGal F is the group $\mathrm{Gal}(F^{\mathrm{sep}}/F)$ of $F$ -algebra automorphisms of SeparableClosure F (Mathlib's chosen separable closure $F^{\mathrm{sep}}$ of $F$ ), with group law composition ( $(\sigma\tau)(x) = \sigma(\tau(x))$ ) and Mathlib's Krull topology. Denote it $\Gamma_F$ .

H F n (for $n\in\mathbb{N}$ ) is the topological $\mathbb{Z}/2$ -module

H^n_{\mathrm{cts}}\bigl(\Gamma_F,\ \mathbb{Z}/2\bigr),

Mathlib's continuous cohomology (as above) with coefficient ring $k = \mathbb{Z}/2$ (ZMod 2, with the discrete topology) and module $M = \mathbb{Z}/2$ (discrete) with trivial $\Gamma_F$ -action. No hypothesis on the characteristic is used in AbsGal or H.

From here on the variable line adds the hypothesis $2 \neq 0$ in $F$ (NeZero (2 : F), i.e. $\operatorname{char} F \neq 2$ ), and $F$ becomes an implicit argument. This hypothesis is in scope for every remaining declaration.

Instance. Under $2 \ne 0$ in $F$ : the natural number $2$ cast into $F^{\mathrm{sep}}$ is nonzero (proved via injectivity of $F \to F^{\mathrm{sep}}$ ). This instance is available to all later declarations.

sqrtSep a. For a unit $a \in F^\times$ , $\sqrt{a} := \mathrm{sqrtSep}(a) \in F^{\mathrm{sep}}$ is some element $s$ with $s^2 = a$ (image of $a$ in $F^{\mathrm{sep}}$ ), selected by the axiom of choice from the existence statement that, in a separably closed field where $2 \neq 0$ , every element has a square root. Nothing specifies which of the two roots is chosen; the choice is fixed per $a$ but otherwise arbitrary and not related across different $a$ (e.g. no relation between $\sqrt{ab}$ and $\sqrt a\sqrt b$ is asserted).

Lemma sqrtSep_sq. $(\sqrt a)^2 = a$ in $F^{\mathrm{sep}}$ .

kummerCharFun a. For $a \in F^\times$ and $\sigma \in \Gamma_F$ ,

\chi_a(\sigma) = \begin{cases} 0 \in \mathbb{Z}/2 & \text{if } \sigma(\sqrt a) = \sqrt a,\\ 1 \in \mathbb{Z}/2 & \text{otherwise.}\end{cases}

So value $0$ means $\sigma$ fixes the chosen root, value $1$ means it does not.

Lemma sqrtSep_ne_zero. $\sqrt a \neq 0$ for every $a \in F^\times$ .

Lemma neg_sqrtSep_ne. $-\sqrt a \neq \sqrt a$ .

Lemma apply_sqrtSep. For all $a \in F^\times$ , $\sigma \in \Gamma_F$ : $\sigma(\sqrt a) = \sqrt a$ or $\sigma(\sqrt a) = -\sqrt a$ .

Lemma kummerCharFun_mul. For all $a$ , $\sigma,\tau \in \Gamma_F$ : $\chi_a(\sigma\tau) = \chi_a(\sigma) + \chi_a(\tau)$ in $\mathbb{Z}/2$ .

Lemma continuous_kummerCharFun. $\chi_a : \Gamma_F \to \mathbb{Z}/2$ is continuous (Krull topology on $\Gamma_F$ , discrete topology on $\mathbb{Z}/2$ ).

kummerChar a is $\chi_a$ packaged as a continuous map $\Gamma_F \to \mathbb{Z}/2$ .

symbolCochain a. For $n\in\mathbb{N}$ and a tuple $a = (a_0,\dots,a_{n-1})$ of units of $F$ , this is the continuous map $c_a : \Gamma_F^{\,n+1} \to \mathbb{Z}/2$ (product topology on $\Gamma_F^{n+1}$ ),

c_a(x_0,\dots,x_n) = \prod_{j=0}^{n-1}\bigl(\chi_{a_j}(x_{j+1}) - \chi_{a_j}(x_j)\bigr),

i.e. prodCochain with $G = \Gamma_F$ , $R = \mathbb{Z}/2$ , $\chi_j = \chi_{a_j}$ . (In $\mathbb{Z}/2$ subtraction equals addition.) For $n = 0$ , $c_a$ is the constant function $1$ on $\Gamma_F$ .

Lemma symbolCochain_invariant. For all $a$ , $g \in \Gamma_F$ , $v \in \Gamma_F^{n+1}$ : $c_a(gv_0,\dots,gv_n) = c_a(v_0,\dots,v_n)$ .

Lemma coboundary_symbolCochain. $\partial c_a = 0$ , i.e. for every $y \in \Gamma_F^{n+2}$ ,

\sum_{i=0}^{n+1}(-1)^i\, c_a(y_0,\dots,\widehat{y_i},\dots,y_{n+1}) = 0 \quad\text{in } \mathbb{Z}/2.

galoisSymbol a. For $n \in \mathbb{N}$ and $a = (a_0,\dots,a_{n-1}) \in (F^\times)^n$ (with $\operatorname{char}F \ne 2$ ), the output is an element of

H^n_{\mathrm{cts}}(\Gamma_F, \mathbb{Z}/2)\quad(\text{coefficients } \mathbb{Z}/2 \text{ with trivial action, over the ring } \mathbb{Z}/2),

namely classOf applied to $c_a$ (with $k = M = \mathbb{Z}/2$ , $G = \Gamma_F$ ) using the two lemmas above: the cohomology class of the $\Gamma_F$ -invariant homogeneous cocycle $\mathrm{curryN}_{n+1}(c_a)$ , i.e. $x_0 \mapsto x_1 \mapsto \cdots \mapsto x_n \mapsto c_a(x_0,\dots,x_n)$ . For $n = 0$ (empty tuple) it is the class in $H^0$ of the constant function $1$ . The definition goes through the square roots $\sqrt{a_j}$ selected by sqrtSep; the file proves no lemma about galoisSymbol itself (for example, nothing about how it depends on that choice, or about multiplicativity).

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by vatsj · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Galois symbol (F×)n→Hn(F,Z/2)(F^\times)^n \to H^n(F,\mathbb{Z}/2)(F×)n→Hn(F,Z/2)

Read-back: Def_MilnorConjecture_GaloisSymbol

Imported bundle definitions (unfolded)

Section Cochain

Field-level declarations

Galois symbol $(F^\times)^n \to H^n(F,\mathbb{Z}/2)$

Read-back: `Def_MilnorConjecture_GaloisSymbol`

Section `Cochain`