/-
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 directives: (a) transcribe §7.1's definitions about the central extension in a Mathlib-only
file; (b) the input of `CentralExtension` is a LATTICE `L` (§6.1's `RationalLattice`, i.e. (6.1.1)),
and the structure carries the CORE MAP `L̂ → L`.

The book's own words, in order:

* **(7.1.1)** "We start with a lattice `L` with symmetric form `(·,·)`, and we assume only that `L` is
  nondegenerate --- not necessarily even or positive definite." --- the input `R : MM.FLM61.RationalLattice`.
* **(7.1.6)** "Let `(ê, ·)` be a central extension of `L` by a finite cyclic group
  `⟨κ⟩ = ⟨κ | κ^s = 1⟩` of order `s > 0`: `1 → ⟨κ⟩ → ê → L → 1`." --- the group `Lhat`, the core map
  `pi : Lhat → L` (surjective, `ker π = ⟨κ⟩`), and the generator `kappa` of order `s`, central.
* **(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 ∈ ê`." --- read at the section (7.1.10) below.
* **(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`" (kept as laws, exactly as the book lists them):
  `ε₀(α,β) + ε₀(α+β,γ) = ε₀(β,γ) + ε₀(α,β+γ)`, `ε₀(α,β) - ε₀(β,α) = 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).**  The chapter-8 front object
`MM.FLM861Book.CentralExtension` is `eps : L → L → Fˣ` with three laws --- no `s`, no `ω`, no `χ`, no
`c₀`, no group `ê`, and NO core map.  It is the image of the present structure under `χ`, and both
(7.1.6)'s exact sequence and (7.1.13)'s commutator identity are thereby LOST AS DATA.  The faithful
transcription of (7.1.1) + (7.1.6)--(7.1.17) is the present file.

NEXT (measured, not done here): from `c0_spec`/`orderOf_kappa`, `c₀(α,α) = 0` and the ℤ-bilinearity of
`c₀`; and the comparison `eps = χ ∘ c₀` against `MM.FLM861Book.CentralExtension`.
-/

import Definitions.FLM61Lattices
import Mathlib

namespace MM.FLM71

universe u v w

/-- **(7.1.6) with (7.1.8), (7.1.10)--(7.1.13)**: a central extension of the lattice `R` by a finite
cyclic group `⟨κ | κ^s = 1⟩` of order `s > 0` --- `1 → ⟨κ⟩ → ê → L → 1` --- carrying the CORE MAP
`pi : ê → L`, a section `e` with `e₀ = 1`, its cocycle `ε₀`, the commutator map `c₀` of (7.1.8), and
the four relations (7.1.13). -/
structure CentralExtension (R : MM.FLM61.RationalLattice.{v}) where
  /-- (7.1.6): the order `s > 0` of `⟨κ⟩ = ⟨κ | κ^s = 1⟩`. -/
  s : ℕ
  /-- (7.1.6): `s > 0`. -/
  s_pos : 0 < s
  /-- (7.1.6): the extension `ê`, a group. -/
  Lhat : Type w
  /-- (7.1.6): `ê` is a group. -/
  [group : Group Lhat]
  /-- **(7.1.6), THE CORE MAP**: `ê → L` of `1 → ⟨κ⟩ → ê → L → 1`. -/
  pi : Lhat → R.L
  /-- (7.1.6): `π` is additive (`π(xy) = π(x) + π(y)`). -/
  pi_mul : ∀ x y : Lhat, pi (x * y) = pi x + pi y
  /-- (7.1.6): `π(1) = 0`. -/
  pi_one : pi 1 = 0
  /-- (7.1.6): `ê ↠ L` is onto. -/
  pi_surj : ∀ a : R.L, ∃ x : Lhat, pi x = a
  /-- (7.1.6): the generator `κ` of the cyclic group `⟨κ⟩` in the exact sequence. -/
  kappa : Lhat
  /-- (7.1.6): `⟨κ⟩` has order `s > 0`. -/
  orderOf_kappa : orderOf kappa = s
  /-- (7.1.6): the extension is CENTRAL: `κ` is central in `ê`. -/
  kappa_central : ∀ x : Lhat, kappa * x = x * kappa
  /-- (7.1.6): exactness at `ê` --- `ker π = ⟨κ⟩`. -/
  pi_eq_one_iff : ∀ x : Lhat, pi x = 0 ↔ x ∈ Subgroup.zpowers kappa
  /-- (7.1.10): a section `e : L → ê`. -/
  e : R.L → Lhat
  /-- (7.1.10): `e₀ = 1`. -/
  e_zero : e 0 = 1
  /-- (7.1.10): `e` is a section of `π`. -/
  pi_e : ∀ a : R.L, pi (e a) = a
  /-- (7.1.8)/(7.1.9) read at the section: the commutator map
  `e_α e_β e_α⁻¹ e_β⁻¹ = κ^{c₀(α,β)}`. -/
  c0 : R.L → R.L → ZMod s
  /-- (7.1.9): `aba⁻¹b⁻¹ = κ^{c₀(ā,b̄)}`, at `a = e_α`, `b = e_β`. -/
  c0_spec : ∀ a b : R.L, e a * e b * (e a)⁻¹ * (e b)⁻¹ = kappa ^ (c0 a b).val
  /-- (7.1.11): the 2-cocycle `ε₀` of the section. -/
  eps0 : R.L → R.L → ZMod s
  /-- (7.1.12): `e_α e_β = κ^{ε₀(α,β)} e_{α+β}`. -/
  eps0_spec : ∀ a b : R.L, e a * e b = kappa ^ (eps0 a b).val * e (a + b)
  /-- (7.1.13), first relation: `ε₀(α,β) + ε₀(α+β,γ) = ε₀(β,γ) + ε₀(α,β+γ)`. -/
  eps0_cocycle : ∀ a b c : R.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 : R.L, eps0 a b - eps0 b a = c0 a b
  /-- (7.1.13), third relation: `ε₀(0,α) = 0`. -/
  eps0_zero_left : ∀ a : R.L, eps0 0 a = 0
  /-- (7.1.13), fourth relation: `ε₀(α,0) = 0`. -/
  eps0_zero_right : ∀ a : R.L, eps0 a 0 = 0

attribute [instance] CentralExtension.group

namespace CentralExtension

variable {R : MM.FLM61.RationalLattice.{v}} (E : CentralExtension R)

/-- (7.1.6): the core map is a surjection `ê ↠ L` in the exact sequence. -/
theorem pi_surjective : Function.Surjective E.pi := E.pi_surj

/-- (7.1.6): `κ^s = 1` --- `⟨κ | κ^s = 1⟩`, from `orderOf κ = s`. -/
theorem kappa_pow_s : E.kappa ^ E.s = 1 := by
  rw [← E.orderOf_kappa]
  exact pow_orderOf_eq_one E.kappa

/-- (7.1.6): the class of `κ` is the kernel --- `π(κ) = 0`. -/
theorem pi_kappa : E.pi E.kappa = 0 :=
  (E.pi_eq_one_iff E.kappa).mpr (Subgroup.mem_zpowers E.kappa)

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 {R : MM.FLM61.RationalLattice.{v}} (E : CentralExtension R) (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 {R : MM.FLM61.RationalLattice.{v}} {E : CentralExtension R} {F : Type u} [Field F]
variable (Rc : Realization E F)

/-- (7.1.14): `ω ≠ 0`, since `ω^s = 1` with `s > 0`. -/
theorem omega_ne_zero : Rc.omega ≠ 0 := by
  intro h
  have hs : E.s ≠ 0 := Nat.pos_iff_ne_zero.mp E.s_pos
  have h1 := Rc.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 => Rc.omega ^ x.val

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

/-- (7.1.15): `χ` takes values in `F^×` --- "a faithful character `χ : ⟨κ⟩ → F^×`". -/
theorem chi_ne_zero (x : ZMod E.s) : Rc.chi x ≠ 0 :=
  pow_ne_zero _ Rc.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 : R.L) : F := Rc.omega ^ (E.c0 a b).val

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

end Realization

end MM.FLM71
