/-
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

open scoped TensorProduct

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

/-! ## (7.1.17)--(7.1.30): the `L̂`-module `F{L}` and the elements `ι(a)`

The book, verbatim: **(7.1.17)** "Denote by `F^χ` the one-dimensional space `F` viewed as a
`⟨κ⟩`-module on which `⟨κ⟩` acts according to `χ`: `κ · 1 = ω`."  **(7.1.18)** "denote by `F{L}` the
induced `L̂`-module `F{L} = Ind F^χ = F[L̂] ⊗ F^χ = F[L̂]/(κ − ω)F[L̂]`" (see (1.5.5)).  **(7.1.19)**
"For `a ∈ L`, we set `ι(a) = a ⊗ 1 ∈ F{L}`."  **(7.1.29)/(7.1.30)** the action of `L̂` on `F{L}` is
`e_α · e_β = ε(α,β) e_{α+β}` and `κ · e_β = ω e_β`.  Linearly `F{L} = F[L]`, spanned by the `ι(a)`
((7.1.23)); that carrier is transcribed here. -/

namespace CentralExtension

variable {R : MM.FLM61.RationalLattice.{v}} {F : Type u} [Field F]

/-- **(7.1.19)**: `ι(a) = a ⊗ 1 ∈ F{L}`, where `F{L} = F[L]` linearly ((7.1.18)/(7.1.23)). -/
noncomputable def iota (a : R.L) : (R.L →₀ F) := Finsupp.single a 1

/-- **(7.1.24)**: the multiplicative 2-cocycle of the section, `ε(α,β) = ω^{ε₀(α,β)} ∈ F^×`. -/
noncomputable def eps (E : CentralExtension R) (Rc : Realization E F) (a b : R.L) : F :=
  Rc.omega ^ (E.eps0 a b).val

/-- (7.1.27): `ε(0,α) = 1`. -/
theorem eps_zero_left (E : CentralExtension R) (Rc : Realization E F) (a : R.L) :
    eps E Rc 0 a = 1 := by
  simp [eps, E.eps0_zero_left a]

/-- (7.1.28): `ε(α,0) = 1`. -/
theorem eps_zero_right (E : CentralExtension R) (Rc : Realization E F) (a : R.L) :
    eps E Rc a 0 = 1 := by
  simp [eps, E.eps0_zero_right a]

/-- **(7.1.29)**: the action of the section element `e_α` on `F{L}`:
`e_α · ι(β) = ε(α,β) ι(α+β)`. -/
noncomputable def secAction (E : CentralExtension R) (Rc : Realization E F) (a : R.L) :
    (R.L →₀ F) →ₗ[F] (R.L →₀ F) :=
  Finsupp.linearCombination F fun b => eps E Rc a b • Finsupp.single (a + b) (1 : F)

/-- **(7.1.30)**: `κ · ι(β) = ω ι(β)` --- `κ` acts as multiplication by `ω = χ(κ)`. -/
noncomputable def kappaAction (Rc : Realization E F) : (R.L →₀ F) →ₗ[F] (R.L →₀ F) :=
  Rc.omega • LinearMap.id

/-- **(7.1.17) with (7.1.30)**: `κ` acts on every `ι(a)` by `ω = χ(κ)`. -/
theorem kappaAction_iota (Rc : Realization E F) (a : R.L) :
    kappaAction Rc (iota a) = Rc.omega • iota a := by
  simp [kappaAction, LinearMap.smul_apply]

end CentralExtension

/-! ## (7.1.1)--(7.1.5) and (7.1.31): `𝔥 = L_F`, `M(1) = S(𝔥̂_-)`, `V_L = M(1) ⊗ F{L}`

The book: **(7.1.1)** "we set `𝔥 = L_F = L ⊗_ℤ F`, a finite-dimensional `F`-vector space with
nonsingular symmetric form `(·,·)`, and we identify `L` with `L ⊗ 1 ⊂ 𝔥`."  **(7.1.2)/(7.1.3)** the
affine Lie algebra `𝔤 = ⊕_n 𝔥 ⊗ t^n ⊕ Fc ⊕ Fd` and its Heisenberg subalgebra
`𝔥̂ = 𝔥̂' = ⊕_{n ≠ 0} 𝔥 ⊗ t^n ⊕ Fc`.  **(7.1.4)** "Consider the usual `Q`-graded `𝔥̂`-irreducible
`𝔤`-module `M(1) = S(𝔥̂_-)`", where `𝔥̂_- = ⊕_{n < 0} 𝔥 ⊗ t^n`, with `c` acting as `1`.  **(7.1.31)**
"Set `V_L = M(1) ⊗ F{L} = S(𝔥̂_-) ⊗ F{L}`" --- the tensor product of the two constructions above, over `F`.

The `L̂`-action on `V_L` is the action on the SECOND factor alone ((7.1.29)/(7.1.30) of the previous
section, made into operators here); the Heisenberg modes `a(n)` of (7.1.5) act on `M(1)`, i.e. on the
first factor, and are transcribed with the Heisenberg machinery. -/

/-- **(7.1.1)**: `𝔥 = L_F = L ⊗_ℤ F`, the `F`-vector space of the book, with `L` identified inside it
as `L ⊗ 1`. -/
abbrev h (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] :=
  F ⊗[ℤ] R.L

/-- **(7.1.3)**: `𝔥̂_- = ⊕_{n < 0} 𝔥 ⊗ t^n`, indexed by `ℕ+` so that `(n, a)` is `a ⊗ t^{-n}`; this is
the negative half on which `M(1) = S(𝔥̂_-)` is built (the `c`-part acts as `1` and is not carried). -/
abbrev heisMinus (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] := ℕ+ →₀ (h R F)

/-- **(7.1.4)**: `M(1) = S(𝔥̂_-)`, "the usual `Q`-graded `𝔥̂`-irreducible `𝔤`-module", `c` acting as 1. -/
abbrev M1 (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] := SymmetricAlgebra F (heisMinus R F)

/-- **(7.1.31)**: `V_L = M(1) ⊗ F{L} = S(𝔥̂_-) ⊗ F{L}` --- the tensor product (over `F`) of the Fock
half `M(1)` of (7.1.4) with the `L̂`-module `F{L}` of (7.1.18). -/
abbrev VL (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] := M1 R F ⊗[F] (R.L →₀ F)

namespace CentralExtension

variable {R : MM.FLM61.RationalLattice.{v}} {F : Type u} [Field F]

/-- **(7.1.19) inside `V_L`**: the element `ι(a) = 1 ⊗ ι(a)`, i.e. the image of `ι(a) ∈ F{L}` under
`M(1) ⊗ F{L}` with `1 ∈ M(1)` the vacuum. -/
noncomputable def iotaVL (a : R.L) : VL R F :=
  (1 : M1 R F) ⊗ₜ[F] iota (R := R) (F := F) a

/-- **(7.1.30) on `V_L`**: `κ` acts on `V_L` through the second factor, `κ · (m ⊗ ι(β)) = ω (m ⊗ ι(β))`. -/
noncomputable def kappaActionVL (Rc : Realization E F) : VL R F →ₗ[F] VL R F :=
  TensorProduct.map LinearMap.id (kappaAction Rc)

/-- **(7.1.29) on `V_L`**: the section element `e_α` acts on `V_L` through the second factor,
`e_α · (m ⊗ ι(β)) = m ⊗ (ε(α,β) ι(α+β))`. -/
noncomputable def secActionVL (E : CentralExtension R) (Rc : Realization E F) (a : R.L) :
    VL R F →ₗ[F] VL R F :=
  TensorProduct.map LinearMap.id (secAction E Rc a)

/-- (7.1.31) with (7.1.30): on `ι(a)`, `κ` acts by `ω` --- `iotaVL` lands in the `ω`-eigenspace. -/
theorem kappaActionVL_iotaVL (Rc : Realization E F) (a : R.L) :
    kappaActionVL Rc (iotaVL (R := R) (F := F) a) = Rc.omega • iotaVL (R := R) (F := F) a := by
  simp [kappaActionVL, iotaVL, kappaAction, LinearMap.smul_apply,
    TensorProduct.map_tmul, TensorProduct.tmul_smul]

end CentralExtension

/-! ## (7.1.4)/(7.1.5): the Heisenberg modes `a(n)` on `M(1) = S(𝔥̂_-)`

The book: **(7.1.4)** "Consider the usual `Q`-graded `𝔥̂`-irreducible `𝔤`-module `M(1) = S(𝔥̂_-)`, with
`c` acting as `1`, `d` acting as the degree operator and `𝔥` acting trivially.  As in (4.1.3), we use the
notation `a(n)` for the action of `a ⊗ t^n` on `S(𝔥̂_-)`, for `a ∈ 𝔥` and `n ∈ ℤ`, so that
`[a(m), β(n)] = (a,β) m δ_{m+n,0}`, `[d, a(m)] = m a(m)`" --- (7.1.5).

On `S(𝔥̂_-)`: `a(n)` for `n < 0` is CREATION, multiplication by the generator `a ⊗ t^n`; `a(n)` for
`n > 0` is ANNIHILATION, the derivation contracting `a' ⊗ t^{-n}` to `n (a, a')`; `a(0) = 0`, because `𝔥`
acts trivially on `M(1)`.  The only input is the CONTRACTION functional `(a, ·) : 𝔥 → F` of (7.1.1), which
here is the ℤ-bilinear form `R.form` of §6.1 base-changed to `𝔥 = L_F` ((6.1.5)/(6.1.17)); it enters
through `annih` below, and the commutator `[a(m), β(n)] = (a,β) m δ_{m+n,0}` is proved from the two
constructions (next).  The degree operator `d` of (7.1.5) is the `ℕ+`-gradation of `heisMinus`. -/

variable {R : MM.FLM61.RationalLattice.{v}} {F : Type u} [Field F]

/-- (7.1.5): the functional `a' ⊗ t^{-n} ↦ n · φ(a')` by which the annihilation mode `a(n)` contracts,
for a contraction functional `φ = (a, ·) : 𝔥 → F` of (7.1.1). -/
noncomputable def annih (n : ℕ+) (φ : h R F →ₗ[F] F) : heisMinus R F →ₗ[F] F :=
  (n : F) • φ.comp (Finsupp.lapply n)

/-- (7.1.4): CREATION `a(-n)`, `n ≥ 1`: multiplication by the generator `a ⊗ t^{-n}` of `S(𝔥̂_-)`. -/
noncomputable def creation (n : ℕ+) (v : h R F) : M1 R F →ₗ[F] M1 R F :=
  LinearMap.mulLeft F (SymmetricAlgebra.ι F (heisMinus R F) (Finsupp.single n v))

/-- (7.1.5): the derivation `D_φ` of `S(𝔥̂_-)` with `D_φ(v) = φ v` on `𝔥̂_-`, obtained as the first-order
exponential of a derivation through the dual numbers `F[ε]/ε²`: `v ↦ v + ε φ(v)`. -/
noncomputable def dualNumberLift (φ : heisMinus R F →ₗ[F] F) :
    M1 R F →ₗ[F] TrivSqZeroExt (M1 R F) (M1 R F) :=
  SymmetricAlgebra.lift
    { toFun := fun v =>
        TrivSqZeroExt.inl (SymmetricAlgebra.ι F (heisMinus R F) v) + TrivSqZeroExt.inr (φ v • (1 : M1 R F))
      map_add' := by
        intro v w
        refine TrivSqZeroExt.ext ?_ ?_
        · simp only [TrivSqZeroExt.fst_add, TrivSqZeroExt.fst_inl, TrivSqZeroExt.fst_inr, map_add]
          abel
        · simp only [TrivSqZeroExt.snd_add, TrivSqZeroExt.snd_inl, TrivSqZeroExt.snd_inr, map_add,
            add_smul]
          abel
      map_smul' := by
        intro (c : F) v
        refine TrivSqZeroExt.ext ?_ ?_
        · simp only [TrivSqZeroExt.fst_smul, TrivSqZeroExt.fst_add, TrivSqZeroExt.fst_inl,
            TrivSqZeroExt.fst_inr, map_smul]
          simp
        · simp only [TrivSqZeroExt.snd_smul, TrivSqZeroExt.snd_add, TrivSqZeroExt.snd_inl,
            TrivSqZeroExt.snd_inr, map_smul]
          simp [smul_smul] }

/-- (7.1.5): the derivation of `S(𝔥̂_-)` determined by the functional `φ`. -/
noncomputable def derivOf (φ : heisMinus R F →ₗ[F] F) : M1 R F →ₗ[F] M1 R F :=
  ((TrivSqZeroExt.sndHom (M1 R F) (M1 R F)).restrictScalars F).comp (dualNumberLift φ)

/-- (7.1.5): ANNIHILATION `a(n)`, `n ≥ 1`: the derivation contracting `a' ⊗ t^{-n}` to `n (a, a')`. -/
noncomputable def annihilation (n : ℕ+) (φ : h R F →ₗ[F] F) : M1 R F →ₗ[F] M1 R F :=
  derivOf (annih n φ)

/-! ## (7.1.1) reads in a `ℤ`-base, and (7.1.5) `a(m)` for all `m ∈ ℤ`

**(6.1.3)/(6.1.6)**: the book fixes a `ℤ`-base to read the form ("we see by choosing a `ℤ`-base of `L`
that `(L,L) ⊂ (1/r)ℤ`", and nondegeneracy "amounts to the condition `det((αᵢ,αⱼ)) ≠ 0` for a `ℤ`-base").
In that base the form `(·,·)` of (7.1.1) on `𝔥 = L_F` is the `F`-bilinear form with the Gram values
`R.form (bᵢ) (bⱼ) ∈ ℚ` --- `formH` below; its partial application `formH bL a` is the contraction
functional `(a, ·)` that the annihilation modes of `annih`/`annihilation` consume.  With it, (7.1.5)'s
`a(m)` are defined for all `m ∈ ℤ`: creation for `m < 0`, `0` for `m = 0` (`𝔥` acts trivially on `M(1)`),
annihilation for `m > 0`. -/

variable {R : MM.FLM61.RationalLattice.{v}} {F : Type u} [Field F]

/-- **(6.1.3)/(6.1.5)/(6.1.17) in a `ℤ`-base**: the form of (7.1.1) on `𝔥 = L_F`, read in the base `bL`:
`F`-bilinear with the Gram values `(bᵢ, bⱼ) = R.form (bᵢ) (bⱼ) ∈ ℚ` of §6.1. -/
noncomputable def formH {κ : Type w} [Fintype κ] [DecidableEq κ]
    (bL : Module.Basis κ ℤ R.L) : (F ⊗[ℤ] R.L) →ₗ[F] (F ⊗[ℤ] R.L) →ₗ[F] F :=
  (bL.baseChange F).constr F fun i => ∑ j, (R.form (bL i) (bL j) : F) • (bL.baseChange F).coord j

/-- **(7.1.5)**: `a(m)` for all `m ∈ ℤ` --- creation `a(-n)` for `m = -n < 0`, `0` for `m = 0` (since `𝔥`
acts trivially on `M(1)`, (7.1.4)), and annihilation `a(n)` for `m = n > 0`, contracting with the
contraction functional `(a, ·) = formH bL a` of (7.1.1). -/
noncomputable def mode {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    (m : ℤ) (a : F ⊗[ℤ] R.L) : M1 R F →ₗ[F] M1 R F :=
  if hm : m < 0 then creation ⟨(-m).natAbs, Int.natAbs_pos.mpr (ne_of_gt (neg_pos.mpr hm))⟩ a
  else if hm0 : m = 0 then 0
  else annihilation ⟨m.natAbs,
      Int.natAbs_pos.mpr (ne_of_gt (lt_of_le_of_ne (le_of_not_gt hm) (Ne.symm hm0)))⟩
    (formH bL a)

/-- (7.1.5): for `m < 0`, `a(m) = a(-n)` is CREATION, multiplication by `a ⊗ t^{-n}`. -/
theorem mode_of_neg {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    {m : ℤ} (hm : m < 0) (a : F ⊗[ℤ] R.L) :
    mode (R := R) (F := F) bL m a
      = creation (R := R) (F := F) ⟨(-m).natAbs, Int.natAbs_pos.mpr (ne_of_gt (neg_pos.mpr hm))⟩ a := by
  rw [mode, dif_pos hm]

/-- (7.1.4)/(7.1.5): `a(0) = 0` --- `𝔥` acts trivially on `M(1) = S(𝔥̂_-)`. -/
theorem mode_zero {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    (a : F ⊗[ℤ] R.L) : mode (R := R) (F := F) bL 0 a = 0 := by
  rw [mode, dif_neg (lt_irrefl (0 : ℤ)), dif_pos rfl]

/-- **(7.1.24)**: `ε(α,β) = ω^{ε₀(α,β)} ≠ 0` --- `ε` takes values in `F^×`. -/
theorem eps_ne_zero {E : CentralExtension R} {Rc : Realization E F} (a b : R.L) :
    CentralExtension.eps E Rc a b ≠ 0 :=
  pow_ne_zero _ Rc.omega_ne_zero

end MM.FLM71
