/-
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: NEXT (draft held, batch 367-A)

The §1.7 transcription (printed 21--26) is DRAFTED and its content fixed --- the structure of
(1.7.1)--(1.7.3) with the dual bases of (1.7.8), the bracket [x_i,y_j] = d_ij z of (1.7.8), the form
(x,y) of (1.7.4) with its alternation (1.7.6), and M(k) = S(l-) with the three actions of (1.7.10)
(z by k, y_i by multiplication, x_i by k d/dy_i).  What blocks it is purely the Lean universe
annotation of the carrier l = l+ (+) l- (+) Fz (the Type (max u v) ascription produces a stuck
universe constraint) followed by three type mismatches that all cascade from it.  Landed next batch by
giving the carrier its correct universe (the index type i : Type v makes HeisenbergAlg F a live
universe parameter) and then the same declarations verbatim.

Nothing of this is a mathematical gap: it is an annotation. -/

end MM.FLM1
