/-
Copyright (c) 2026 The MM project. All rights reserved.
Released under Apache 2.0 license as described in the LICENSE file.
Authors: MM project (batch 365-A, owner's directive)

# FLM §7.1 (printed 144--150): the CENTRAL EXTENSION of a lattice, transcribed strictly

Owner's directive: transcribe §7.1's definitions about the central extension, in a file that depends on
Mathlib only.  The book's own words, in order:

* **(7.1.6)** "Let `(ê, ·)` be a central extension of `L` by a finite cyclic group
  `⟨κ⟩ = ⟨κ | κ^s = 1⟩` of order `s > 0`: `1 → ⟨κ⟩ → ê → L → 1`."
* **(7.1.8)/(7.1.9)** "Denote by `c₀ : L × L → ℤ/sℤ` the associated commutator map, so that
  `aba⁻¹b⁻¹ = κ^{c₀(ā,b̄)}` for `a, b ∈ ê`."
* **(7.1.10)--(7.1.12)** a section `e : L → ê`, `α ↦ e_α`, with `e₀ = 1`, and the corresponding
  2-cocycle `ε₀ : L × L → ℤ/sℤ`, with `e_α e_β = κ^{ε₀(α,β)} e_{α+β}`.
* **(7.1.13)** the four relations, "for `α, β, γ ∈ L`":
  `ε₀(α,β) + ε₀(α+β,γ) = ε₀(β,γ) + ε₀(α,β+γ)`, `ε₀(α,β) - ε₀(β,α) = c₀(α,β)`,
  `ε₀(α,0) = ε₀(0,α) = 0`.
* **(7.1.14)** "We assume that the field `F` contains a primitive `s`-th root of unity.  Fix such
  `ω ∈ F^×`" and **(7.1.15)/(7.1.16)** "define the faithful character `χ : ⟨κ⟩ → F^×` by the condition
  `χ(κ) = ω`".

**Point of record (owner's suspicion, checked here).**  The chapter-8 front object
`MM.FLM861Book.CentralExtension` is `eps : L → L → Fˣ` with three laws --- it has NO `s`, NO `ω`, NO
`χ`, NO `c₀`, and no finite cyclic group `⟨κ⟩`.  That is the image of the present structure under `χ`
(`eps = χ ∘ ε₀`), and (7.1.13)'s commutator identity is thereby LOST AS DATA: there it can only be
recovered as the derived `ε(α,β)ε(β,α)⁻¹`.  What the derived object cannot see at all, and what this
file therefore restores, is: the ORDER `s` of `⟨κ⟩` (which is what makes `ω` primitive and `χ` faithful
mean something), and the commutator map `c₀` as a `ℤ/sℤ`-valued form of the extension.

NEXT (measured, not done here): (7.1.13) makes `c₀` ℤ-BILINEAR and alternating, `c₀(α+β,γ) = c₀(α,γ) +
c₀(β,γ)`, `c₀(α,β) = -c₀(β,α)`; the proofs are additive rearrangements of the cocycle and commutator
identities in `ℤ/sℤ`, done next.
-/

import Mathlib

namespace MM.FLM71

universe u v

/-- **(7.1.6) with (7.1.8), (7.1.10)--(7.1.13)**: a central extension of `L` by a finite cyclic group
`⟨κ | κ^s = 1⟩` of order `s > 0`, in the equivalent section form the book uses from (7.1.10) on: the
commutator map `c₀ : L × L → ℤ/sℤ` of (7.1.8) and the 2-cocycle `ε₀ : L × L → ℤ/sℤ` of a section `e`
with `e₀ = 1`, subject to the four relations (7.1.13). -/
structure CentralExtension (L : Type v) [AddCommGroup L] where
  /-- (7.1.6): the order `s > 0` of `⟨κ⟩`. -/
  s : ℕ
  /-- (7.1.6): `s > 0`. -/
  s_pos : 0 < s
  /-- (7.1.8): the commutator map `c₀ : L × L → ℤ/sℤ`, `aba⁻¹b⁻¹ = κ^{c₀(ā,b̄)}`. -/
  c0 : L → L → ZMod s
  /-- (7.1.11): the 2-cocycle `ε₀` of a section `e` with `e₀ = 1`, (7.1.12). -/
  eps0 : L → L → ZMod s
  /-- (7.1.13), first relation: the cocycle identity (associativity of the twisted multiplication). -/
  eps0_cocycle : ∀ a b c : L, eps0 a b + eps0 (a + b) c = eps0 b c + eps0 a (b + c)
  /-- (7.1.13), second relation: `ε₀(α,β) - ε₀(β,α) = c₀(α,β)`. -/
  eps0_commutator : ∀ a b : L, eps0 a b - eps0 b a = c0 a b
  /-- (7.1.13), third relation: `ε₀(0,α) = 0`. -/
  eps0_zero_left : ∀ a : L, eps0 0 a = 0
  /-- (7.1.13), fourth relation: `ε₀(α,0) = 0`. -/
  eps0_zero_right : ∀ a : L, eps0 a 0 = 0

namespace CentralExtension

variable {L : Type v} [AddCommGroup L] (E : CentralExtension L)

/-- (7.1.9) with (7.1.13): the commutator map is ALTERNATING, `c₀(α,α) = 0` --- `a a a⁻¹ a⁻¹ = 1`. -/
theorem c0_self (a : L) : E.c0 a a = 0 := by
  have h := E.eps0_commutator a a
  rw [sub_self] at h
  exact h.symm

/-- (7.1.13) with (7.1.8): `c₀(0,α) = 0` (`0 = 1` in the extension). -/
theorem c0_zero_left (a : L) : E.c0 0 a = 0 := by
  have h := E.eps0_commutator 0 a
  rw [E.eps0_zero_left a, E.eps0_zero_right a, sub_zero] at h
  exact h.symm

/-- (7.1.13) with (7.1.8): `c₀(α,0) = 0`. -/
theorem c0_zero_right (a : L) : E.c0 a 0 = 0 := by
  have h := E.eps0_commutator a 0
  rw [E.eps0_zero_right a, E.eps0_zero_left a, sub_zero] at h
  exact h.symm

end CentralExtension

/-- **(7.1.14)--(7.1.16)**: "We assume that the field `F` contains a primitive `s`-th root of unity.
Fix such `ω ∈ F^×`" and "define the faithful character `χ : ⟨κ⟩ → F^×` by `χ(κ) = ω`", i.e.
`χ(x) = ω^x` on `⟨κ⟩ ≅ ℤ/sℤ`. -/
structure Realization {L : Type v} [AddCommGroup L] (E : CentralExtension L) (F : Type u)
    [Field F] where
  /-- (7.1.14): the fixed primitive `s`-th root of unity `ω ∈ F^×`. -/
  omega : F
  /-- (7.1.14): `ω^s = 1`. -/
  omega_pow_s : omega ^ E.s = 1
  /-- (7.1.14): `ω` is PRIMITIVE: `ω^k = 1` only for `s ∣ k`. -/
  omega_primitive : ∀ k : ℤ, omega ^ k = 1 → (E.s : ℤ) ∣ k

namespace Realization

variable {L : Type v} [AddCommGroup L] {E : CentralExtension L} {F : Type u} [Field F]
variable (R : Realization E F)

/-- (7.1.14): `ω ≠ 0`, since `ω^s = 1` with `s > 0`. -/
theorem omega_ne_zero : R.omega ≠ 0 := by
  intro h
  have hs : E.s ≠ 0 := Nat.pos_iff_ne_zero.mp E.s_pos
  have h1 := R.omega_pow_s
  rw [h, zero_pow hs] at h1
  exact zero_ne_one h1

/-- **(7.1.15)/(7.1.16)**: the faithful character `χ : ⟨κ⟩ = ℤ/sℤ → F^×`, `χ(κ) = ω`, i.e.
`χ(x) = ω^{x}` (the exponent read in `{0, …, s-1}`). -/
def chi : ZMod E.s → F := fun x => R.omega ^ x.val

@[simp] theorem chi_apply (x : ZMod E.s) : R.chi x = R.omega ^ x.val := rfl

/-- (7.1.15): `χ` takes values in `F^×` --- "a faithful character `χ : ⟨κ⟩ → F^×`". -/
theorem chi_ne_zero (x : ZMod E.s) : R.chi x ≠ 0 :=
  pow_ne_zero _ R.omega_ne_zero

/-- **(7.1.21) with (7.1.15)**: the commutator pairing of the extension, `c(α,β) = χ(c₀(α,β)) =
ω^{c₀(α,β)}`, as an `F`-valued form on `L`. -/
def pairing (a b : L) : F := R.omega ^ (E.c0 a b).val

/-- (7.1.15): the pairing takes values in `F^×`. -/
theorem pairing_ne_zero (a b : L) : R.pairing a b ≠ 0 :=
  pow_ne_zero _ R.omega_ne_zero

/-- (7.1.13) with (7.1.8): the pairing is ALTERNATING, `c(α,α) = 1`. -/
theorem pairing_self (a : L) : R.pairing a a = 1 := by
  simp [pairing, E.c0_self a]

end Realization

end MM.FLM71
