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

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]

/-! ## §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.7: HEISENBERG ALGEBRAS (printed 21--26) --- THE DEFINITION, AND WHAT THE BOOK DERIVES FROM IT

(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: `IsHeisenberg` below.  In
particular there is no carrier `𝔩₊ ⊕ 𝔩₋ ⊕ Fz` in the definition; that carrier is a *presentation* of the
commutation relations, recorded here as (1.7.7)/(1.7.8) and realized in §7.1.

The rest of §1.7, in the book's order:

* **(1.7.2)/(1.7.3)** "Throughout this section `𝔩` shall be a ℤ-graded Heisenberg algebra
  `𝔩 = ⊕_{n∈ℤ} 𝔩_n` such that `dim 𝔩_n < ∞` ... and `Cent 𝔩 = 𝔩₀`" --- `IsHeisenbergGraded`.
* **(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)`"
  --- `isAlt_of_bracket_eq_smul`.
* **(1.7.7)/(1.7.8)** `𝔩₊ = ⊕_{n>0} 𝔩_n`, `𝔩₋ = ⊕_{n<0} 𝔩_n` are abelian, dual bases `(x_i)`, `(y_i)`
  with `(x_i,y_j) = δ_{ij}`, and "the relations (1.7.8) are called the HEISENBERG COMMUTATION RELATIONS"
  --- `IsHeisPresentation`.
* **(1.7.9)/(1.7.10)** `F_k` and `M(k) ≅ S(𝔩₋)`, with `z ↦ k`, `y_i ↦` multiplication and
  `x_i ↦ k ∂/∂y_i` --- landed with §7.1's `M(1) = S(𝔥̂₋)`.

WHERE THE HEISENBERG ALGEBRA ACTUALLY COMES FROM (this is §7.1's start, not §1.7's): 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; the definitions below are what it must satisfy. -/

/-- **(1.3.1) with (1.7.1)**: the centre `Cent 𝔩 = {x | ∀ y, [x,y] = 0}`. -/
def center (F : Type u) (𝔩 : Type v) [Field 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] [LieRing 𝔩] [LieAlgebra F 𝔩] : Submodule F 𝔩 :=
  Submodule.span F (Set.range fun p : 𝔩 × 𝔩 => ⁅p.1, p.2⁆)

/-- **(1.7.1)**: THE DEFINITION OF A HEISENBERG (LIE) ALGEBRA --- "`Cent 𝔩 = 𝔩'` and
`dim Cent 𝔩 = 1`". -/
def IsHeisenberg (F : Type u) (𝔩 : Type v) [Field F] [LieRing 𝔩] [LieAlgebra F 𝔩] : Prop :=
  center F 𝔩 = derived F 𝔩 ∧ Module.rank F (center F 𝔩) = 1

/-- **(1.7.2)/(1.7.3)**: the ℤ-graded shape of §1.7 --- a family of subspaces `𝔩_n` with
`𝔩 = ⊕_{n∈ℤ} 𝔩_n`, `[𝔩_m, 𝔩_n] ⊆ 𝔩_{m+n}`, `dim 𝔩_n < ∞`, and `Cent 𝔩 = 𝔩₀` (and (1.7.1) at the
top). -/
structure IsHeisenbergGraded (F : Type u) (𝔩 : Type v) [Field F] [LieRing 𝔩] [LieAlgebra F 𝔩]
    where
  /-- (1.7.1): the underlying Heisenberg property. -/
  isHeisenberg : IsHeisenberg F 𝔩
  /-- the graded pieces `𝔩_n`. -/
  piece : ℤ → Submodule F 𝔩
  /-- `𝔩 = ⊕_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 𝔩 = piece 0

/-- **(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] [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

/-- **(1.7.7)/(1.7.8)**: THE HEISENBERG COMMUTATION RELATIONS, as data: a central `z ≠ 0`, two families
`(x_i)`, `(y_i)` with `[x_i,x_j] = [y_i,y_j] = 0` and `[x_i,y_j] = δ_{ij} z`.  This is the *presentation*
--- "we do not assume any connection between the subscript `i` and `deg x_i` or `deg y_j`" --- not the
definition; (1.7.1)'s content is that the pieces `𝔩±` of (1.7.7) are what such data describes. -/
structure IsHeisPresentation (F : Type u) (𝔩 : Type v) [Field F] [LieRing 𝔩] [LieAlgebra F 𝔩]
    (ι : Type v) where
  /-- (1.7.8): `z`, spanning the centre. -/
  z : 𝔩
  /-- (1.7.8): `z ≠ 0`. -/
  z_ne_zero : z ≠ 0
  /-- (1.7.8): the basis `(x_i)` of `𝔩₊`. -/
  x : ι → 𝔩
  /-- (1.7.8): the basis `(y_i)` of `𝔩₋`. -/
  y : ι → 𝔩
  /-- `z` is central. -/
  z_central : ∀ w : 𝔩, ⁅z, w⁆ = 0
  /-- (1.7.8): `(x_i, x_j) = 0`, i.e. `[x_i, x_j] = 0`. -/
  hxx : ∀ i j : ι, ⁅x i, x j⁆ = 0
  /-- (1.7.8): `(y_i, y_j) = 0`, i.e. `[y_i, y_j] = 0`. -/
  hyy : ∀ i j : ι, ⁅y i, y j⁆ = 0
  /-- (1.7.8): `[x_i, y_i] = z`. -/
  hxy_self : ∀ i : ι, ⁅x i, y i⁆ = z
  /-- (1.7.8): `[x_i, y_j] = 0` for `i ≠ j`. -/
  hxy_ne : ∀ i j : ι, i ≠ j → ⁅x i, y j⁆ = 0


end MM.FLM1
