/-
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 367-A, owner's directive)

# FLM Chapter 1, §1.6 and §1.7: AFFINE LIE ALGEBRAS and HEISENBERG ALGEBRAS, transcribed

**STANDING CONVENTION (printed 2, verbatim)**: "Throughout this work, `F` will denote a field of
characteristic 0.  All vector spaces and algebras will be over `F` unless another field is specified."
So the field of this file is of characteristic zero THROUGHOUT: `[CharZero F]` is carried by the file's
field variable and by every declaration that binds `F` explicitly.  (The repository's `FLM861Datum`
carries the same hypothesis.)

Owner's directive: the chain `vector space → affine Lie algebra → Heisenberg subalgebra → induced
`M(k) ≅ S(𝔩⁻)`` of Chapter 1 must exist as DEFINITIONS, and §7.1's `𝔤`, `𝔥̂`, `M(1) = S(𝔥̂_-)` are one
INSTANCE of it.  This file is that chain, in the book's numbering (printed 17--26); the instance follows
in `FLM71CentralExtension.lean`.  Hard laws are `sorry` (owner's directive).

The book, verbatim, in order:

* **(1.6.1)** "Let `𝔤` be a Lie algebra and let `(·,·)` be a bilinear form on `𝔤` ... `(·,·)` is said to be
  INVARIANT or `𝔤`-invariant if `([x,y],z) + (y,[x,z]) = 0`, equivalently `([x,y],z) = (x,[y,z])`."
* **(1.6.2)** `F[t,t^{-1}]`, the Laurent polynomials, with `f₀ = a₀` for `f = Σ aₙtⁿ`, and `d = t d/dt`.
* **(1.6.3)** "`𝔩̂ = 𝔤 ⊗_F F[t,t^{-1}] ⊕ Fc`, where `Fc` is a one-dimensional space."
* **(1.6.4)/(1.6.5)** "There is an (alternating) bilinear map `[·,·] : 𝔩̂ × 𝔩̂ → 𝔩̂` determined by
  `[x⊗t^m, y⊗t^n] = [x,y]⊗t^{m+n} + (x,y)m δ_{m+n,0}c`" and `[c, 𝔩̂] = 0`.
* **(1.6.6)** the loop algebra `𝔤 ⊗ F[t,t^{-1}]` with `[x⊗t^m, y⊗t^n] = [x,y]⊗t^{m+n}`.
* **(1.6.7)** the exact sequence `0 → Fc → 𝔩̂ → 𝔤 ⊗ F[t,t^{-1}] → 0`.
* **(1.6.8)** `d(c) = 0`, `d(x ⊗ f) = x ⊗ df`.
* **(1.6.9)** the extended affine algebra `𝔩 = 𝔩̂ ⋊ Fd` (semidirect product).
* **(1.6.10)/(1.6.11)** `𝔩 = ∐_{n∈ℤ} 𝔩_n` with `𝔩_n = {x | [d,x] = nx}` --- "`d` is the degree
  derivation"; **(1.6.12)--(1.6.14)** `𝔩_n = 𝔤̂_n ⊕ Fc` for `n = 0` and `𝔩_n = 𝔤̂_n` for `n ≠ 0`.
* **(1.7.1)** "We call a Lie algebra `𝔩` a HEISENBERG (Lie) algebra if `Cent 𝔩 = 𝔩'` and
  `dim Cent 𝔩 = 1`"; **(1.7.2)/(1.7.3)** `𝔩` is `ℤ`-graded with `dim 𝔩_n < ∞` and `Cent 𝔩 = 𝔩_0`.
* **(1.7.4)--(1.7.6)** "Let `z ∈ Cent 𝔩`, `z ≠ 0` ... Define a bilinear form `(·,·)` on `𝔩` by
  `[x,y] = (x,y)z`.  Then `(·,·)` is an alternating form, `(x,x) = 0`, equivalently `(x,y) = -(y,x)`."
* **(1.7.7)** `𝔩⁺ = ⊕_{n>0} 𝔩_n`, `𝔩⁻ = ⊕_{n<0} 𝔩_n`, abelian with `(𝔩⁺,𝔩⁺) = (𝔩⁻,𝔩⁻) = 0`.
* **(1.7.8)** with bases `(xᵢ)` of `𝔩⁺` and `(yⱼ)` of `𝔩⁻`: "`[xᵢ,yⱼ] = δ_{ij}z` ... The relations (1.7.8)
  are called the HEISENBERG COMMUTATION RELATIONS."
* **(1.7.9)/(1.7.10)** `F_k` the one-dimensional graded `𝔩⁺ ⊕ Fz`-module with `z·1 = k`, `𝔩⁺·1 = 0`,
  `deg 1 = 0`; `M(k)` the induced `𝔩`-module, with `M(k) ≅ S(𝔩⁻)` as graded vector spaces, `z` acting as
  `k`, `yᵢ` as multiplication and `xᵢ` as the partial derivative `k ∂/∂yᵢ`.
-/

import Mathlib

namespace MM.FLM1

universe u v

variable (F : Type u) [Field F] [CharZero F]

/-! ## §1.6: invariant forms, the loop algebra, the affine algebra, its extension by `d` -/

/-- **(1.6.1)**: the bilinear form `(·,·)` is INVARIANT (associative) --- `([x,y],z) = (x,[y,z])`. -/
def IsInvariantSym {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤] [LieAlgebra F 𝔤]
    (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) : Prop :=
  ∀ x y z : 𝔤, B ⁅x, y⁆ z = B x ⁅y, z⁆

/-- **(1.6.3)/(1.6.5)**, linearly: the affine algebra `𝔩̂ = 𝔤 ⊗_F F[t,t^{-1}] ⊕ Fc`, carried as
`(ℤ →₀ 𝔤) ⊕ F·c` (the `ℤ`-index of `F[t,t^{-1}]` is the exponent of `t`). -/
abbrev Affine (𝔤 : Type v) [Zero 𝔤] : Type (max u v) := (ℤ →₀ 𝔤) × F

/-- **(1.6.9)**: the extended affine algebra `𝔩 = 𝔩̂ ⋊ Fd`, carried as `𝔩̂ ⊕ F·d`. -/
abbrev AffineExt (𝔤 : Type v) [Zero 𝔤] : Type (max u v) := Affine F 𝔤 × F

/-- **(1.6.6)**: the bracket of the LOOP algebra,
`[x ⊗ t^m, y ⊗ t^n] = [x,y] ⊗ t^{m+n}`, in coefficients. -/
noncomputable def loopBracket {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (x y : ℤ →₀ 𝔤) : ℤ →₀ 𝔤 :=
  x.sum fun m u => y.sum fun n w => Finsupp.single (m + n) ⁅u, w⁆

/-- **(1.6.4)/(1.6.5)**: the bracket of the AFFINE algebra --- the loop bracket plus the central term
`(x,y)m δ_{m+n,0}c`, i.e. the `c`-component `Σ_m m (u_m, y_{-m})`. -/
noncomputable def affineBracket {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (x y : Affine F 𝔤) : Affine F 𝔤 :=
  (loopBracket F x.1 y.1, x.1.sum fun m u => (m : F) * B u (y.1 (-m)))

/-- **(1.6.8)/(1.6.11)**: the action of `d` on `𝔩̂`, `d(x ⊗ t^m) = m (x ⊗ t^m)` and `d(c) = 0` --- the
degree derivation; its eigenspaces are the graded pieces `𝔩_n` of (1.6.10)--(1.6.14). -/
noncomputable def dAct {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] (x : Affine F 𝔤) : Affine F 𝔤 :=
  (x.1.sum fun m u => Finsupp.single m (m • u), 0)

/-- **(1.6.10)--(1.6.14)**: an element of `𝔩̂` is HOMOGENEOUS OF DEGREE `n` if it is concentrated in the
`t^n`-component, i.e. `d` acts on it by `n`.  This is the degree that (7.1.4)'s "`d` acting as the degree
operator" refers to. -/
def IsHomogeneousOfDeg {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] (n : ℤ) (x : Affine F 𝔤) : Prop :=
  x.1.support ⊆ {n}

/-! ### §1.6 (continued): THE AFFINIZATION IS A LIE ALGEBRA ((1.6.4)/(1.6.5))

`affineBracket` above is a *function*; what the book asserts in (1.6.4)/(1.6.5) is that it makes
`𝔤̂ = 𝔤 ⊗ F[t,t⁻¹] ⊕ Fc` a LIE ALGEBRA --- "(alternating) bilinear map ... determined by
`[x⊗t^m, y⊗t^n] = [x,y]⊗t^{m+n} + (x,y)m δ_{m+n,0}c`" and `[c, 𝔤̂] = 0`.  The two hypotheses needed are
exactly the two properties of the form in the book's own setting:

* **(1.6.1) SYMMETRY** `(x,y) = (y,x)` --- needed for ALTERNATION: the central part of `[u,u]` is
  `Σ_m m (u_m, u_{-m})`, and the pair `(m,-m)`, `(-m,m)` cancels precisely by symmetry;
* **(1.6.1) INVARIANCE** `([x,y],z) = (x,[y,z])` --- needed for JACOBI: the loop part is Jacobi in `𝔤`
  and the central part is `(x,[y,z])m + (y,[z,x])n + (z,[x,y])p` at `m+n+p = 0`, which vanishes because
  the trilinear form `(x,[y,z])` is CYCLIC --- a consequence of symmetry plus invariance
  (`(x,[y,z]) = ([x,y],z) = -([y,x],z) = -(y,[x,z]) = (y,[z,x])`).

**THE CONTENT IS THE THEOREM `affine_isLieAlgebra` BELOW**: the affine bracket is alternating and satisfies
Jacobi --- i.e. `𝔤̂` IS a Lie algebra --- exactly when `B` is symmetric and invariant.  An
`instance` packaging would be bookkeeping only, and it runs into Mathlib's `LieAlgebra extends Module`
diamond: `LieAlgebra` must sit on the SAME `AddCommGroup (Affine F 𝔤)` as the `LieRing`, which the
product/Finsupp instance path does not deliver (`DistribMulAction.smul_zero` mismatches on
`Zero (Affine F 𝔤)`) --- hence a theorem, not an instance. -/

/-- **(1.6.1)**: the form is SYMMETRIC --- "let `(·,·)` be a symmetric invariant bilinear form". -/
def IsSymmForm {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) : Prop :=
  ∀ x y : 𝔤, B x y = B y x

/-- **(1.6.1)**: the trilinear form `(x,[y,z])` is CYCLIC, `(x,[y,z]) = (y,[z,x])`, from symmetry and
invariance --- the identity that cancels the central term of Jacobi. -/
theorem invariant_trilinear_cyclic {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (hSymm : IsSymmForm F B)
    (hInv : IsInvariantSym F B) (x y z : 𝔤) : B x ⁅y, z⁆ = B y ⁅z, x⁆ := by
  sorry

/-- **(1.6.4)**: the affine bracket is additive in its first variable. -/
theorem affineBracket_add_left {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (x y z : Affine F 𝔤) :
    affineBracket F B (x + y) z = affineBracket F B x z + affineBracket F B y z := by
  sorry

/-- **(1.6.4)**: the affine bracket is additive in its second variable. -/
theorem affineBracket_add_right {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (x y z : Affine F 𝔤) :
    affineBracket F B x (y + z) = affineBracket F B x y + affineBracket F B x z := by
  sorry

/-- **(1.6.4)**: the affine bracket is `F`-homogeneous in its second variable --- the `F`-linearity that
`LieAlgebra.lie_smul` asks for. -/
theorem affineBracket_smul_right {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (c : F) (x y : Affine F 𝔤) :
    affineBracket F B x (c • y) = c • affineBracket F B x y := by
  sorry

/-- **(1.6.4)**: the affine bracket is `F`-homogeneous in its first variable. -/
theorem affineBracket_smul_left {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (c : F) (x y : Affine F 𝔤) :
    affineBracket F B (c • x) y = c • affineBracket F B x y := by
  sorry

/-- **(1.6.4)**: the affine bracket is ALTERNATING, `[u,u] = 0`.  The loop part dies by the
antisymmetry of `[·,·]` in `𝔤` (the pairs `(m,n)`, `(n,m)` cancel); the central part `Σ_m m (u_m,u_{-m})`
dies by the pair `(m,-m)`, `(-m,m)` and the SYMMETRY of the form. -/
theorem affineBracket_self {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (hSymm : IsSymmForm F B) (x : Affine F 𝔤) :
    affineBracket F B x x = 0 := by
  sorry

/-- **(1.6.4)/(1.6.5)**: JACOBI for the affine bracket --- the loop part is Jacobi in `𝔤`, and the central
term is `(x,[y,z])m + (y,[z,x])n + (z,[x,y])p` at `m + n + p = 0`, which vanishes by the cyclicity
`invariant_trilinear_cyclic` of the trilinear form. -/
theorem affineBracket_jacobi {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (hSymm : IsSymmForm F B)
    (hInv : IsInvariantSym F B) (u v w : Affine F 𝔤) :
    affineBracket F B (affineBracket F B u v) w + affineBracket F B (affineBracket F B v w) u
      + affineBracket F B (affineBracket F B w u) v = 0 := by
  sorry


/-- **(1.6.4)/(1.6.5)**: THE AFFINIZATION OF A LIE ALGEBRA IS A LIE ALGEBRA --- as a THEOREM, i.e. as
the list of laws satisfied by the affine bracket `[x⊗t^m, y⊗t^n] = [x,y]⊗t^{m+n} + (x,y)m δ_{m+n,0}c`,
`[c, ·] = 0`: bilinearity (four laws), alternation `[u,u] = 0`, Jacobi, and the `F`-linearity that
`LieAlgebra` adds.  The hypotheses are exactly the two properties the book's setting gives to the form
(1.6.1): SYMMETRY (for the alternation) and INVARIANCE (for Jacobi, through the cyclicity of
`(x,[y,z])`).  Nothing else is needed --- in particular no choice of an instance. -/
theorem affine_isLieAlgebra {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (hSymm : IsSymmForm F B)
    (hInv : IsInvariantSym F B) :
    (∀ x y z : Affine F 𝔤, affineBracket F B (x + y) z = affineBracket F B x z + affineBracket F B y z) ∧
    (∀ x y z : Affine F 𝔤, affineBracket F B x (y + z) = affineBracket F B x y + affineBracket F B x z) ∧
    (∀ x : Affine F 𝔤, affineBracket F B x x = 0) ∧
    (∀ u v w : Affine F 𝔤, affineBracket F B (affineBracket F B u v) w
      + affineBracket F B (affineBracket F B v w) u + affineBracket F B (affineBracket F B w u) v = 0) ∧
    (∀ (c : F) (x y : Affine F 𝔤), affineBracket F B (c • x) y = c • affineBracket F B x y) ∧
    (∀ (c : F) (x y : Affine F 𝔤), affineBracket F B x (c • y) = c • affineBracket F B x y) :=
  ⟨affineBracket_add_left (F := F) B, affineBracket_add_right (F := F) B,
    affineBracket_self (F := F) B hSymm, affineBracket_jacobi (F := F) B hSymm hInv,
    affineBracket_smul_left (F := F) B, affineBracket_smul_right (F := F) B⟩

/-! ## §1.7: HEISENBERG ALGEBRAS (printed 21--26) --- THE DEFINITION, BUNDLED

(1.7.1) verbatim: **"We call a Lie algebra `𝔩` a HEISENBERG (Lie) algebra if `Cent 𝔩 = 𝔩'` and
`dim Cent 𝔩 = 1`."**  This --- and nothing else --- is the definition.  It is provided in BOTH forms:

* `IsHeisenberg F 𝔩 : Prop` --- the property, for statements;
* `Heisenberg F` (and `HeisenbergGraded F`) --- the **bundled object**: carrier, Lie structure, and the
  property.  Bundling is what lets §7.1's Heisenberg subalgebra `𝔥̂₀ = 𝔥̂'` (7.1.3) be an element of
  `Heisenberg F` instead of a restatement of (1.7.1).

§4.1's reading of `𝔥 = L ⊗_ℤ F` (7.1.1) is likewise bundled: `AbelianLieAlg F` is an abelian Lie algebra
as an object, and `AbelianLieAlg.ofModule` is the canonical way to instantiate it on any `F`-module.

The rest of §1.7, in the book's order (all statements carry their numbers):

* (1.7.2)/(1.7.3) "`𝔩` shall be a ℤ-graded Heisenberg algebra `𝔩 = ⊕_{n∈ℤ} 𝔩_n` such that
  `dim 𝔩_n < ∞` ... and `Cent 𝔩 = 𝔩₀`" --- the extra fields of `HeisenbergGraded`;
* (1.7.4)--(1.7.6) "Define a bilinear form `(·,·)` ... `[x,y] = (x,y)z` ... `(x,x) = 0`, equivalently
  `(x,y) = -(y,x)`" --- `isAlt_of_bracket_eq_smul`;
* (1.7.7)/(1.7.8) `𝔩±` abelian, dual bases, `[x_i,y_j] = δ_{ij}z`, "the relations (1.7.8) are called the
  HEISENBERG COMMUTATION RELATIONS" --- realized for `ᵒ4̂₀` in `FLM71CentralExtension.lean`
  (`heisAb`, `hhat`, `IsInHeis0`), not as an abstract presentation here;
* (1.7.9)/(1.7.10) `F_k` and `M(k) ≅ S(𝔩₋)` with `z ↦ k`, `y_i ↦` multiplication, `x_i ↦ k ∂/∂y_i` ---
  landed with §7.1's `M(1) = S(𝔥̂₋)` (7.1.4).

WHERE THE HEISENBERG ALGEBRA OF THE BOOK COMES FROM (§7.1, not §1.7): from the lattice `L` with its
symmetric form one sets `𝔥 = L_ℂ = L ⊗_ℤ F` (7.1.1), a finite-dimensional `F`-space with a nonsingular
symmetric form, viewed --- as in Section 4.1 --- as an ABELIAN Lie algebra; then the ℤ-graded untwisted
affine Lie algebra `𝔥̂ = 𝔥 ⊗ F[t,t⁻¹] ⊕ Fc ⊕ Fd` (7.1.2) and its HEISENBERG SUBALGEBRA
`𝔥̂₀ = 𝔥̂' = ⊕_{n≠0} 𝔥 ⊗ tⁿ ⊕ Fc` (7.1.3) are formed, with `M(1) = S(𝔥̂₋)` (7.1.4).  That construction is
`FLM71CentralExtension.lean`'s; it must produce a `Heisenberg F` (and an `AbelianLieAlg F` for `𝔥`).

Hard laws are `sorry` (owner's directive). -/

/-- **(1.3.1) with (1.7.1)**: the centre `Cent 𝔩 = {x | ∀ y, [x,y] = 0}`. -/
def center (F : Type u) (𝔩 : Type v) [Field F] [CharZero F] [LieRing 𝔩] [LieAlgebra F 𝔩] : Submodule F 𝔩 where
  carrier := {x : 𝔩 | ∀ y : 𝔩, ⁅x, y⁆ = 0}
  zero_mem' := by intro y; simp
  add_mem' := by intro x y hx hy z; rw [add_lie, hx z, hy z, add_zero]
  smul_mem' := by intro c x hx y; rw [smul_lie, hx y, smul_zero]

/-- **(1.7.1)**: the derived subalgebra `𝔩' = [𝔩,𝔩]`, spanned by the brackets. -/
def derived (F : Type u) (𝔩 : Type v) [Field F] [CharZero F] [LieRing 𝔩] [LieAlgebra F 𝔩] : Submodule F 𝔩 :=
  Submodule.span F (Set.range fun p : 𝔩 × 𝔩 => ⁅p.1, p.2⁆)

/-- **(1.7.1)**: THE DEFINITION, as a property --- "`Cent 𝔩 = 𝔩'` and `dim Cent 𝔩 = 1`". -/
def IsHeisenberg (F : Type u) (𝔩 : Type v) [Field F] [CharZero F] [LieRing 𝔩] [LieAlgebra F 𝔩] : Prop :=
  center F 𝔩 = derived F 𝔩 ∧ Module.rank F (center F 𝔩) = 1

/-- **(1.7.1), BUNDLED**: a HEISENBERG (Lie) ALGEBRA as an object --- carrier, its Lie structure, and the
two defining properties.  Use `Heisenberg.mk` (or `⟨…⟩`) to instantiate one; `H.isHeisenberg` is the
property, `H.carrier` the carrier (its Lie instances come with it). -/
structure Heisenberg (F : Type u) [Field F] [CharZero F] where
  /-- the carrier `𝔩`. -/
  carrier : Type v
  /-- the Lie ring structure of `𝔩`. -/
  [instLieRing : LieRing carrier]
  /-- the `F`-Lie algebra structure of `𝔩`. -/
  [instLieAlgebra : LieAlgebra F carrier]
  /-- **(1.7.1)**: `Cent 𝔩 = 𝔩'` and `dim Cent 𝔩 = 1`. -/
  isHeisenberg : IsHeisenberg F carrier

attribute [instance] Heisenberg.instLieRing Heisenberg.instLieAlgebra

/-- **(1.7.2)/(1.7.3), BUNDLED**: a ℤ-GRADED Heisenberg algebra --- "`𝔩 = ⊕_{n∈ℤ} 𝔩_n` such that
`dim 𝔩_n < ∞` ... and `Cent 𝔩 = 𝔩₀`", with (1.7.1) on top. -/
structure HeisenbergGraded (F : Type u) [Field F] [CharZero F] where
  /-- the carrier `𝔩`. -/
  carrier : Type v
  /-- the Lie ring structure of `𝔩`. -/
  [instLieRing : LieRing carrier]
  /-- the `F`-Lie algebra structure of `𝔩`. -/
  [instLieAlgebra : LieAlgebra F carrier]
  /-- the graded pieces `𝔩_n`. -/
  piece : ℤ → Submodule F carrier
  /-- `𝔩 = ⊕_n 𝔩_n`. -/
  span_piece : ⨆ n, piece n = ⊤
  /-- (1.7.2): `[𝔩_m, 𝔩_n] ⊆ 𝔩_{m+n}`. -/
  lie_mem : ∀ m n : ℤ, ∀ x ∈ piece m, ∀ y ∈ piece n, ⁅x, y⁆ ∈ piece (m + n)
  /-- (1.7.3): `dim 𝔩_n < ∞`. -/
  finite_piece : ∀ n : ℤ, Module.Finite F (piece n)
  /-- (1.7.3): `Cent 𝔩 = 𝔩₀`. -/
  center_eq_piece_zero : center F carrier = piece 0
  /-- (1.7.1). -/
  isHeisenberg : IsHeisenberg F carrier

attribute [instance] HeisenbergGraded.instLieRing HeisenbergGraded.instLieAlgebra

/-- **(§4.1 with (1.6.1)), BUNDLED**: an ABELIAN (= trivial) Lie algebra --- this is §4.1's reading of
`𝔥`, the one §7.1's construction of `𝔥̂` (7.1.2) starts from.  The bundle carries its carrier, the module
structure, the Lie structure and the vanishing of the bracket; `ofModule` below builds one on any
`F`-module. -/
structure AbelianLieAlg (F : Type u) [Field F] [CharZero F] where
  /-- the carrier `𝔥`. -/
  carrier : Type v
  /-- the additive group structure of `𝔥`. -/
  [instAddCommGroup : AddCommGroup carrier]
  /-- the `F`-module structure of `𝔥`. -/
  [instModule : Module F carrier]
  /-- the (trivial) Lie ring structure of `𝔥`. -/
  [instLieRing : LieRing carrier]
  /-- the `F`-Lie algebra structure of `𝔥`. -/
  [instLieAlgebra : LieAlgebra F carrier]
  /-- the bracket vanishes identically. -/
  bracket_eq_zero : ∀ x y : carrier, ⁅x, y⁆ = 0

attribute [instance] AbelianLieAlg.instAddCommGroup AbelianLieAlg.instModule
  AbelianLieAlg.instLieRing AbelianLieAlg.instLieAlgebra

/-- **(§4.1)**: the canonical ABELIAN Lie algebra structure on an `F`-module --- the object of which
`𝔥 = L ⊗_ℤ F` (7.1.1) is an instance.  Deliberately NOT a global instance (an instance of `LieRing` on
every module would be a diamond against every other Lie structure); use it as
`AbelianLieAlg.ofModule F 𝔥` and read `.carrier` for the Lie structure. -/
def AbelianLieAlg.ofModule (F : Type u) (V : Type v) [Field F] [CharZero F] [AddCommGroup V] [Module F V] :
    AbelianLieAlg F :=
  let lie : LieRing V :=
    { bracket := fun _ _ => 0
      add_lie := by intros; simp
      lie_add := by intros; simp
      lie_self := by intros; simp
      leibniz_lie := by intros; simp }
  letI : LieRing V := lie
  { carrier := V
    instLieRing := lie
    instLieAlgebra :=
      { lie_smul := by intro t x y; exact (smul_zero t).symm }
    bracket_eq_zero := fun _ _ => rfl }

/-- **(§4.1)**: in an abelian Lie algebra the centre is the whole algebra --- the two properties of
(1.7.1) fail there exactly as they should (`Fz` with `z ≠ 0` cannot be the centre of an abelian
algebra unless the algebra is `0`). -/
theorem AbelianLieAlg.center_eq_top (F : Type u) [Field F] [CharZero F] (A : AbelianLieAlg F) : center F A.carrier = ⊤ := by
  sorry

/-- **(§4.1)**: in an abelian Lie algebra the derived subalgebra vanishes. -/
theorem AbelianLieAlg.derived_eq_bot (F : Type u) [Field F] [CharZero F] (A : AbelianLieAlg F) : derived F A.carrier = ⊥ := by
  sorry

/-- **(1.7.4)--(1.7.6)**: for `z ∈ Cent 𝔩`, `z ≠ 0`, and a bilinear form `(·,·)` with `[x,y] = (x,y)z`,
the form is ALTERNATING: `(x,x) = 0` and `(x,y) = -(y,x)`. -/
theorem isAlt_of_bracket_eq_smul (F : Type u) (𝔩 : Type v) [Field F] [CharZero F] [LieRing 𝔩] [LieAlgebra F 𝔩]
    (z : 𝔩) (hz : z ≠ 0) (B : 𝔩 →ₗ[F] 𝔩 →ₗ[F] F) (hB : ∀ x y : 𝔩, ⁅x, y⁆ = B x y • z) :
    (∀ x : 𝔩, B x x = 0) ∧ (∀ x y : 𝔩, B x y = -B y x) := by
  sorry

end MM.FLM1
