/-
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 Definitions.FLM1AffineHeisenberg
import Mathlib

/-! ## §7.1 MAP (printed 144--149): every numbered item, its Lean home and its status

The book, verbatim in order (printed 144): "(7.1.1) We start with a lattice `L` with symmetric form
`(·,·)` ... set `𝔥 = L_ℂ = L ⊗_ℤ F`, a finite-dimensional `F`-vector space with nonsingular symmetric
form, and we identify `L` with `L ⊗ 1 ⊂ 𝔥`.  As in Section 4.1, we view `𝔥` as an ABELIAN Lie algebra and
we form the ℤ-graded untwisted affine Lie algebra `𝔥̂ = ⊕_{n∈ℤ} 𝔥 ⊗ tⁿ ⊕ Fc ⊕ Fd` (7.1.2) and its
HEISENBERG SUBALGEBRA `𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc` (7.1.3).  Consider the usual ℚ-graded `𝔥̂₀`-
irreducible `𝔥̂`-module `M(1) = S(𝔥̂₋)`, with `c` acting as 1, `d` acting as the degree operator and `𝔥̂₊`
acting trivially (7.1.4) ... we use the notation `a(n)` for the action of `a ⊗ tⁿ` on `S(𝔥̂₋)` (7.1.5)."

| FLM | Lean home | status |
| --- | --- | --- |
| (7.1.1) `𝔥 = L ⊗_ℤ F`, nonsingular symmetric form | `h R F` (below), form in a basis: `formH` | DEFINED |
| (7.1.1) `𝔥` read as an abelian Lie algebra (§4.1) | `heisAb` (§1.6/§1.7's `AbelianLieAlg.ofModule`) | DEFINED |
| (7.1.2) `𝔥̂ = ⊕_{n∈ℤ} 𝔥⊗tⁿ ⊕ Fc ⊕ Fd`, ℤ-graded | `hhat` = §1.6's `AffineExt F 𝔥`; bracket `affineBracket`; the Lie laws are §1.6's `affine_isLieAlgebra` | DEFINED (carrier + bracket + laws) |
| (7.1.3) `𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥⊗tⁿ ⊕ Fc` | `IsInHeis0` (`x.1 0 = 0`) --- the `t⁰`-free part of `𝔥̂` | DEFINED; the subalgebra-closure is the target of (7.1.6)/(7.1.7) |
| (7.1.4) `M(1) = S(𝔥̂₋)`, `c ↦ 1`, `d` = degree, `𝔥̂₊ ↦ 0` | `M1 R F` = `S(heisMinus)`; `d`, `annihilation`, `creation`, `degreeEnd` | DEFINED |
| (7.1.5) the notation `a(n)` | `mode`, `modeVL`, `annihilation` | DEFINED |
| (7.1.6)/(7.1.7) `[a(m), b(n)] = m(a,b) δ_{m+n,0} c` on `M(1)` | `mode_commutator`, `d_commutator_mode` | STATED |
| (7.1.8)/(7.1.9) the commutator map `c₀`, `aba⁻¹b⁻¹ = K^{c₀(a,b)}` | `CentralExtension.c0`, `c0_self`, `c0_add_left`, `c0_add_right` | DEFINED |
| (7.1.10)--(7.1.13) the section `e`, `e₀ = 1`, the 2-cocycle `ε₀`, its cocycle identity | `CentralExtension` (`pi`, `kappa`, its cocycle field), `eps_cocycle` | DEFINED |
| (7.1.14)--(7.1.17) the primitive `s`-th root `ω`, the faithful character `χ`, `F_ω` | `Realization` (`omega`, `omega_ne_zero`), `chi`, `chi_ne_zero`, `pairing` | DEFINED |
| (7.1.18)--(7.1.23) the induced module `F{L} = F_ω ⊗_{F⟨K⟩} F[L̂]` and `F[L] ≅ F{L}` | `iota`, `eps` | DEFINED |
| (7.1.24)/(7.1.27)/(7.1.28) `ε(a,b) = ω^{ε₀(a,b)}`, `ε(0,a) = ε(a,0) = 1`, `e_α e_β = ε(α,β) e_{α+β}` | `eps`, `eps_zero_left`, `eps_zero_right`, `eps_ne_zero` | DEFINED |
| (7.1.29)/(7.1.30) the action of `𝔥̂` on `F[L]`: `h·e_α = (h,α)e_α`, `K·e_β = ω e_β` | `secAction`, `kappaAction`, `kappaAction_iota` | DEFINED |
| (7.1.31) `V_L = M(1) ⊗ F{L} = S(𝔥̂₋) ⊗ F{L}` | `VL R F`, `iotaVL`, `kappaActionVL`, `secActionVL` | DEFINED |
| (7.1.32)--(7.1.36) the `ê`-action on `V_L`, `h(0)`, `z^h` | `modeVL` and onward | PARTIAL |

WHAT THE MAP SAYS: the FIRST THREE ITEMS --- (7.1.1)'s abelian reading, (7.1.2)'s affinization and
(7.1.3)'s Heisenberg subalgebra --- are the whole of the §7.1 material that §1.6/§1.7 supply, and they
are now named here (`heisAb`, `hhat`, `IsInHeis0`); everything from (7.1.4) on is this file's own,
already landed.  The bridge between the two halves is ONE theorem, (7.1.6)/(7.1.7): the bracket of two
elements of `𝔥̂₀` is the central element `Σ_m m (x_m, y_{-m}) c`, i.e. the Heisenberg commutation
relations at the Lie-algebra level --- the bridge from `Affine F 𝔥` to `heisMinus`/`M1`. -/

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 {E : CentralExtension R} (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 {E : CentralExtension R} (Rc : Realization E F) (a : R.L) :
    kappaAction Rc (iota a) = Rc.omega • iota a := by
  simp [kappaAction]

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 {E : CentralExtension R} (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 {E : CentralExtension R} (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

/-! ## §7.1: the remaining DEFINITIONS, with the hard proofs marked `sorry`

Owner's directive (batch 366-A): finish the DEFINITIONS of §7.1; the proofs that are genuinely hard
(the CCR of (7.1.5) on `M(1)`, the degree-operator commutator, the `F^×`-cocycle identity (7.1.24), the
bilinearity of `c₀`, the decomposition of `L̂` used by (7.1.29)/(7.1.30)) are marked `sorry` for now.
Each such declaration cites its book number here, so the remaining work is a list, not a search. -/

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

/-- **(7.1.4)/(7.1.5)**: the DEGREE endomorphism `(n, a) → -n • (n, a)` of `𝔥̂_-`,
whose induced derivation is the degree operator `d`.  The SIGN is the book's: `heisMinus` is indexed by
`n ≥ 1` for `a ⊗ t^{-n}`, and FLM's (7.1.5) `[d, a(m)] = m a(m)` forces
`deg(a ⊗ t^{-n}) = -n` (so `M(1)` is graded in degrees ≤ 0, the convention under which the
weight `wt u = n₁ + ⋯ + n_k + ½(a,a)` of (8.5.21) is nonnegative).  With the
opposite sign one gets `[d, mode m a] = -m • mode m a`, contradicting (7.1.5). -/
noncomputable def degreeEnd : heisMinus R F →ₗ[F] heisMinus R F :=
  Finsupp.lsum F fun n => -((n : F)) • (Finsupp.lsingle n)

/-- (7.1.5): the lift of a GENERATOR map `e` of `𝔥̂_-` to the dual numbers `F[ε]/ε²`, i.e. the algebra map
`S(𝔥̂_-) → M(1)[ε]/ε²` that sends a generator `v` to `v + ε (e v)`; its `ε`-coefficient is the derivation
of `derivationOf` below.  (Same shape as `dualNumberLift`, with `φ v • 1` replaced by `e v`.) -/
noncomputable def derivationLift (e : heisMinus R F →ₗ[F] heisMinus R 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 (SymmetricAlgebra.ι F (heisMinus R F) (e v))
      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]
          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 }

/-- (7.1.5): the derivation of `S(𝔥̂_-)` induced by an endomorphism `e` of `𝔥̂_-` --- the `ε`-coefficient
of `derivationLift e`, i.e. the derivation with `D(v) = e v` on the generators `v`. -/
noncomputable def derivationOf (e : heisMinus R F →ₗ[F] heisMinus R F) : M1 R F →ₗ[F] M1 R F :=
  ((TrivSqZeroExt.sndHom (M1 R F) (M1 R F)).restrictScalars F).comp (derivationLift (R := R) (F := F) e)

/-- **(7.1.4)**: `d` acting as the degree operator on `M(1) = S(𝔥̂_-)` --- `d(v) = n • v` for
`v = a ⊗ t^{-n}`. -/
noncomputable def d : M1 R F →ₗ[F] M1 R F := derivationOf (R := R) (F := F) degreeEnd

/-- **(7.1.5)**: `[d, a(m)] = m a(m)` on `M(1) = S(𝔥̂_-)`. -/
theorem d_commutator_mode {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    (m : ℤ) (a : F ⊗[ℤ] R.L) :
    d (R := R) (F := F) ∘ₗ mode (R := R) (F := F) bL m a
        - mode (R := R) (F := F) bL m a ∘ₗ d (R := R) (F := F)
      = (m : F) • mode (R := R) (F := F) bL m a := by
  sorry

/-- **(7.1.5)**: `[a(m), β(n)] = (a,β) m δ_{m+n,0}` on `M(1) = S(𝔥̂_-)` --- the CCR of the Heisenberg
subalgebra, in the first factor of `V_L`. -/
theorem mode_commutator {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    (m n : ℤ) (a b : F ⊗[ℤ] R.L) :
    mode (R := R) (F := F) bL m a ∘ₗ mode (R := R) (F := F) bL n b
        - mode (R := R) (F := F) bL n b ∘ₗ mode (R := R) (F := F) bL m a
      = (if m + n = 0 then (m : F) * formH (R := R) (F := F) bL a b else 0)
          • (1 : M1 R F →ₗ[F] M1 R F) := by
  sorry

/-- **(7.1.24)**: the `F^×`-valued 2-cocycle identity of the section,
`ε(α,β) ε(α+β,γ) = ε(β,γ) ε(α,β+γ)`. -/
theorem eps_cocycle {E : CentralExtension R} {Rc : Realization E F} (a b c : R.L) :
    CentralExtension.eps E Rc a b * CentralExtension.eps E Rc (a + b) c
      = CentralExtension.eps E Rc b c * CentralExtension.eps E Rc a (b + c) := by
  sorry

/-- **(7.1.6)/(7.1.10)**: every element of `L̂` is `κ^m · e_α` --- the decomposition that turns the two
formulas (7.1.29)/(7.1.30) into an action of the whole of `L̂` on `F{L}`. -/
theorem exists_kappa_pow_mul_e (E : CentralExtension R) (x : E.Lhat) :
    ∃ m : ℕ, ∃ a : R.L, x = E.kappa ^ m * E.e a := by
  sorry

namespace CentralExtension

/-- **(7.1.13)**: the commutator map is alternating, `c₀(α,α) = 0`. -/
theorem c0_self (E : CentralExtension R) (a : R.L) : E.c0 a a = 0 := by
  sorry

/-- **(7.1.9)**: `c₀` is ℤ-additive in the first argument --- the commutator map of a central extension
is bilinear. -/
theorem c0_add_left (E : CentralExtension R) (a b c : R.L) :
    E.c0 (a + b) c = E.c0 a c + E.c0 b c := by
  sorry

/-- **(7.1.9)**: `c₀` is ℤ-additive in the second argument. -/
theorem c0_add_right (E : CentralExtension R) (a b c : R.L) :
    E.c0 a (b + c) = E.c0 a b + E.c0 a c := by
  sorry

end CentralExtension

/-- (7.1.5) on `V_L = M(1) ⊗ F{L}`: the Heisenberg modes act on the FIRST factor (the `𝔥̂`-action on
`M(1)`), and the `L̂`-action of (7.1.29)/(7.1.30) acts on the SECOND. -/
noncomputable def modeVL {κ : Type w} [Fintype κ] [DecidableEq κ] (bL : Module.Basis κ ℤ R.L)
    (m : ℤ) (a : F ⊗[ℤ] R.L) : VL R F →ₗ[F] VL R F :=
  TensorProduct.map (mode (R := R) (F := F) bL m a) LinearMap.id


/-! ### §7.1 (7.1.1)--(7.1.3): `𝔥`, the affine algebra `𝔥̂`, its Heisenberg subalgebra `𝔥̂₀` -/

/-- **(7.1.1) with §4.1**: "we view `𝔥` as an ABELIAN Lie algebra" --- the bundle that carries that
reading of `𝔥 = L ⊗_ℤ F` as a Lie structure (`AbelianLieAlg.ofModule`, §1.6/§1.7).  Use it as
`letI := (heisAb R F).instLieRing` and `letI := (heisAb R F).instLieAlgebra`. -/
noncomputable def heisAb (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F] :
    MM.FLM1.AbelianLieAlg F :=
  MM.FLM1.AbelianLieAlg.ofModule F (h R F)

/-- **(7.1.2)**: the ℤ-graded untwisted AFFINE LIE ALGEBRA
`𝔥̂ = ⊕_{n∈ℤ} 𝔥 ⊗ tⁿ ⊕ Fc ⊕ Fd` --- §1.6's `AffineExt` at `𝔤 = 𝔥`, whose bracket is `affineBracket`
(§1.6, (1.6.4)/(1.6.5)) and whose Lie laws are §1.6's `affine_isLieAlgebra`.  The `ℤ`-grading is §1.6's
`IsHomogeneousOfDeg` (the `d`-degree, (1.6.10)--(1.6.14)). -/
abbrev hhat (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] : Type (max u v) :=
  MM.FLM1.AffineExt F (h R F)

/-- **(7.1.3)**: the HEISENBERG SUBALGEBRA `𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc` of `𝔥̂` --- an element of
the `𝔥̂`-part of `𝔥̂` lies in `𝔥̂₀` exactly when its `t⁰`-component vanishes (the central `c` and the
derivation `d` are the other two components). -/
def IsInHeis0 (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (x : MM.FLM1.Affine F (h R F)) : Prop :=
  x.1 0 = 0


/-! ### §7.1 (7.1.3): `𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc` AS A HEISENBERG ALGEBRA

The Heisenberg commutation relations of (7.1.6)/(7.1.7) at the Lie-algebra level are
`[a⊗t^m, b⊗t^n] = m(a,b) δ_{m+n,0} c`, i.e. in coefficients `Σ_m m (x_m, y_{-m}) c` --- the same central
term as §1.6's `affineBracket`, but with the modes restricted to `n ≠ 0` (the degree-zero part `𝔥 ⊗ t⁰` of
`𝔥̂` is central in the abelian case and is exactly what `𝔥̂₀ = 𝔥̂'` EXCLUDES, which is why the carrier below
is indexed by `{n : ℤ // n ≠ 0}` and not by `ℤ`). -/

/-- **(7.1.3)**: the carrier of the Heisenberg subalgebra `𝔥̂₀ = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc`. -/
abbrev heis0 (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] : Type (max u v) :=
  ({n : ℤ // n ≠ 0} →₀ h R F) × F

/-- The reflection `m ↦ -m` on the nonzero modes (used by the central term). -/
def negMode (m : {n : ℤ // n ≠ 0}) : {n : ℤ // n ≠ 0} :=
  ⟨-m.1, by simpa using m.2⟩

/-- **(7.1.6)/(7.1.7) with (1.6.4)**: the Heisenberg bracket on `𝔥̂₀`,
`[x⊗t^m, y⊗t^n] = m (x,y) δ_{m+n,0} c`, i.e. the `c`-component `Σ_m m (x_m, y_{-m})`. -/
noncomputable def heis0Bracket (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F]
    [CharZero F] (B : h R F →ₗ[F] h R F →ₗ[F] F) (x y : heis0 R F) : heis0 R F :=
  (0, x.1.sum fun m u => (m.1 : F) * B u (y.1 (negMode m)))

/-- (7.1.6): the Heisenberg bracket is additive in its first variable. -/
theorem heis0Bracket_add_left (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F]
    [CharZero F] (B : h R F →ₗ[F] h R F →ₗ[F] F) (x y z : heis0 R F) :
    heis0Bracket R F B (x + y) z = heis0Bracket R F B x z + heis0Bracket R F B y z := by
  sorry

/-- (7.1.6): the Heisenberg bracket is additive in its second variable. -/
theorem heis0Bracket_add_right (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F]
    [CharZero F] (B : h R F →ₗ[F] h R F →ₗ[F] F) (x y z : heis0 R F) :
    heis0Bracket R F B x (y + z) = heis0Bracket R F B x y + heis0Bracket R F B x z := by
  sorry

/-- (7.1.6): the Heisenberg bracket is `F`-homogeneous in its second variable. -/
theorem heis0Bracket_smul_right (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F]
    [CharZero F] (B : h R F →ₗ[F] h R F →ₗ[F] F) (c : F) (x y : heis0 R F) :
    heis0Bracket R F B x (c • y) = c • heis0Bracket R F B x y := by
  sorry

/-- **(1.7.6)**: the bracket is ALTERNATING, `[u,u] = 0` --- the central term `Σ_m m (u_m, u_{-m})`
cancels pairwise by the SYMMETRY of the form `(x,y)`, exactly as for §1.6's `affineBracket`. -/
theorem heis0Bracket_self (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (hSymm : ∀ x y : h R F, B x y = B y x) (x : heis0 R F) :
    heis0Bracket R F B x x = 0 := by
  sorry

/-- **(7.1.6)/(7.1.7) with (1.6.4)**: `𝔥̂₀` IS A LIE RING under the Heisenberg bracket --- bilinearity,
alternation (from the symmetry of the form) and Jacobi (trivial, the bracket being central-valued). -/
noncomputable def heis0LieRing (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (hSymm : ∀ x y : h R F, B x y = B y x) :
    LieRing (heis0 R F) where
  bracket := heis0Bracket R F B
  add_lie := heis0Bracket_add_left R F B
  lie_add := heis0Bracket_add_right R F B
  lie_self := heis0Bracket_self R F B hSymm
  leibniz_lie := by sorry

/-- **(7.1.3) with (1.7.1)**: `𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc` AS A HEISENBERG ALGEBRA --- the bundle:
the carrier, the Lie structure of `heis0LieRing`, its `F`-linearity, and the evidence
`Cent 𝔥̂₀ = 𝔥̂₀' = Fc`, `dim Cent 𝔥̂₀ = 1`.  (The last field is where the NONSINGULARITY of the form of
(7.1.1) and `𝔥 ≠ 0` enter: with `B` nonsingular and some `x ≠ 0`, `[x⊗t^m, y⊗t^{-m}] = m B(x,y) c` is
nonzero for suitable `y`, so `c` spans the centre and the derived algebra.) -/
noncomputable def hhat0 (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (hSymm : ∀ x y : h R F, B x y = B y x)
    (hNondeg : ∀ x : h R F, (∀ y : h R F, B x y = 0) → x = 0) :
    MM.FLM1.Heisenberg F :=
  let lie : LieRing (heis0 R F) := heis0LieRing R F B hSymm
  letI : LieRing (heis0 R F) := lie
  { carrier := heis0 R F
    instLieRing := lie
    instLieAlgebra :=
      { (inferInstance : Module F (heis0 R F)) with
          lie_smul := fun c x y => by
            rw [show (⁅x, c • y⁆ : heis0 R F) = heis0Bracket R F B x (c • y) from rfl,
              show (⁅x, y⁆ : heis0 R F) = heis0Bracket R F B x y from rfl]
            exact heis0Bracket_smul_right R F B c x y }
    isHeisenberg := by sorry }


/-! ### §7.1 (7.1.4)/(7.1.5): the MODULE `M(1) = S(𝔥̂₋)` FOR `𝔥̂₀` --- the operators `a(n)`

(7.1.4), verbatim: "Consider the usual ℚ-graded `𝔥̂₀`-irreducible `𝔥̂`-module `M(1) = S(𝔥̂₋)`, with `c`
acting as 1, `d` acting as the degree operator and `𝔥̂₊` acting trivially."  (7.1.5), verbatim: "we use the
notation `a(n)` for the action of `a ⊗ tⁿ` on `S(𝔥̂₋)`, for `a ∈ 𝔥, n ∈ ℤ`.  The three clauses and the
operators:

* `c` acting as 1 ---------------------------- `centralAction` (the identity of `M1 R F`);
* `d` acting as the degree operator ---------- the landed `d` (`derivationOf degreeEnd`) and
  `d_commutator_mode`;
* `𝔥̂₊` acting trivially --------------------- `modeOf_pos_vacuum` (below): `a(m) · 1 = 0` for `m > 0`;
* `a(n)` for all `n ∈ ℤ` --------------------- `modeOf` (below): creation for `n < 0`, annihilation for
  `n > 0` (using the form `(·,·)` of (7.1.1) to identify `𝔥` with its dual), `0` for `n = 0`. -/

/-- **(7.1.4)**: "`c` acting as 1" --- the action of the central element on `M(1) = S(𝔥̂₋)`. -/
noncomputable def centralAction (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] :
    M1 R F →ₗ[F] M1 R F :=
  1

/-- **(7.1.5) with (7.1.4)**: THE OPERATOR `a(n)` --- the action of `a ⊗ tⁿ` on `M(1) = S(𝔥̂₋)`:
for `n < 0` it multiplies by `a ⊗ tⁿ` (creation), for `n > 0` it is the annihilation `y ↦ n (a,y) ∂_y`
--- the form `(·,·)` of (7.1.1) identifying `𝔥` with its dual --- and for `n = 0` it acts trivially
(`a ⊗ t⁰` is central and acts by `0` on the ℚ-graded picture consistent with `c ↦ 1`). -/
noncomputable def modeOf (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (n : ℤ) (a : h R F) : M1 R F →ₗ[F] M1 R F :=
  if h : n < 0 then creation (R := R) (F := F) ⟨(-n).toNat, by omega⟩ a
  else if h0 : n = 0 then 0
  else annihilation (R := R) (F := F) ⟨n.toNat, by omega⟩ (B a)

/-- **(7.1.4)**: "`𝔥̂₊` acting trivially" --- the positive modes kill the vacuum: `a(m) · 1 = 0` for
`m > 0`. -/
theorem modeOf_pos_vacuum (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (m : ℤ) (hm : 0 < m) (a : h R F) :
    modeOf R F B m a 1 = 0 := by
  sorry

/-- **(7.1.5)**: the negative modes create: `a(m) · 1 = a ⊗ t^m` for `m < 0`. -/
theorem modeOf_neg_vacuum (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (m : ℤ) (hm : m < 0) (a : h R F) :
    modeOf R F B m a 1
      = creation (R := R) (F := F) ⟨(-m).toNat, by omega⟩ a 1 := by
  sorry

/-- **(7.1.5)**: the zero mode acts trivially, `a(0) = 0` --- `𝔥 ⊗ t⁰` is central. -/
theorem modeOf_zero (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (a : h R F) :
    modeOf R F B 0 a = 0 := by
  sorry


/-! ### §7.1 (7.1.5): the COMMUTATION RELATIONS on `M(1)`, and the DEGREE operator

(7.1.5), verbatim (quoted in this file above): "we use the notation `a(n)` for the action of `a ⊗ t^n` on
`S(𝔥̂_-)` ... so that `[a(m), β(n)] = (a,β) m δ_{m+n,0}`, `[d, a(m)] = m a(m)`".  `modeOf` is that `a(n)`
for all `n ∈ ℤ` (creation for `n < 0`, annihilation for `n > 0` through the form `(·,·)` of (7.1.1), zero
for `n = 0`); the two relations are `modeOf_commutator` and `modeOf_commutator_d`.  The grading of
(7.1.4) ("the usual ℚ-graded `𝔥̂`-module") is `IsHomogeneousDeg`: the `d`-eigenspaces. -/

/-- **(7.1.4)**: the `d`-GRADING of `M(1) = S(𝔥̂_-)` --- "the usual `ℚ`-graded ... module", read as the
eigen-decomposition of the degree operator. -/
def IsHomogeneousDeg (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F] (n : ℤ)
    (v : M1 R F) : Prop :=
  d (R := R) (F := F) v = n • v

/-- **(7.1.5)**: THE COMMUTATION RELATIONS ON `M(1)`: `[a(m), β(n)] = (a,β) m δ_{m+n,0}` --- with `c`
acting as `1` by (7.1.4) --- i.e. `[a(m), b(n)] = m (a,b) δ_{m+n,0}` for `modeOf`. -/
theorem modeOf_commutator (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (hSymm : ∀ x y : h R F, B x y = B y x) (m n : ℤ)
    (a b : h R F) :
    (modeOf R F B m a).comp (modeOf R F B n b) - (modeOf R F B n b).comp (modeOf R F B m a)
      = (if m + n = 0 then (m : F) * B a b else 0) • (1 : M1 R F →ₗ[F] M1 R F) := by
  sorry

/-- **(7.1.5)**: `[d, a(m)] = m a(m)` --- the degree operator shifts the mode `a(m)` by `m`; the
basis-free form of the landed `d_commutator_mode` (and, with the sign of `degreeEnd`, non-vacuous). -/
theorem modeOf_commutator_d (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (B : h R F →ₗ[F] h R F →ₗ[F] F) (m : ℤ) (a : h R F) :
    (d (R := R) (F := F)).comp (modeOf R F B m a) - (modeOf R F B m a).comp (d (R := R) (F := F))
      = (m : F) • modeOf R F B m a := by
  sorry

/-- **(7.1.4)**: the vacuum is homogeneous of degree `0` --- `d` is a derivation and derivations kill
`1`. -/
theorem d_vacuum (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F] :
    d (R := R) (F := F) (1 : M1 R F) = 0 := by
  simp [d, derivationOf, derivationLift]

/-- **(7.1.4)**: `d` is a DERIVATION of `S(𝔥̂_-)`: `d (v * w) = d v * w + v * d w`. -/
theorem d_leibniz (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    (v w : M1 R F) :
    d (R := R) (F := F) (v * w) = d (R := R) (F := F) v * w + v * d (R := R) (F := F) w := by
  sorry

/-- **(7.1.4)**: products of homogeneous vectors are homogeneous of the sum of the degrees --- the
`ℚ`-grading of `M(1) = S(𝔥̂_-)` is multiplicative. -/
theorem IsHomogeneousDeg.mul (R : MM.FLM61.RationalLattice.{v}) (F : Type u) [Field F] [CharZero F]
    {k l : ℤ} {v w : M1 R F} (hv : IsHomogeneousDeg R F k v) (hw : IsHomogeneousDeg R F l w) :
    IsHomogeneousDeg R F (k + l) (v * w) := by
  rw [IsHomogeneousDeg] at hv hw ⊢
  rw [d_leibniz, hv, hw, smul_mul_assoc, mul_smul_comm, ← add_smul]


end MM.FLM71
