/-
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 Lie structure is a `def` and deliberately NOT a global instance: it depends on the DATA `B`, and an
`instance` with data arguments is what makes typeclass search explode (the batch-368-A lesson).  Use it as
`letI : LieRing (Affine F 𝔤) := affineLieRing (F := F) B hSymm hInv`. -/

/-- **(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)**: `𝔤̂ = 𝔤 ⊗ F[t,t⁻¹] ⊕ Fc` IS A LIE RING under the affine bracket ---
"(alternating) bilinear map ... determined by `[x⊗t^m, y⊗t^n] = [x,y]⊗t^{m+n} + (x,y)m δ_{m+n,0}c`".
A `def` rather than an `instance` because it depends on the data `B` (with `hSymm`, `hInv`); use
`letI : LieRing (Affine F 𝔤) := affineLieRing (F := F) B hSymm hInv`. -/
noncomputable def affineLieRing {𝔤 : Type v} [AddCommGroup 𝔤] [Module F 𝔤] [LieRing 𝔤]
    [LieAlgebra F 𝔤] (B : 𝔤 →ₗ[F] 𝔤 →ₗ[F] F) (hSymm : IsSymmForm F B)
    (hInv : IsInvariantSym F B) : LieRing (Affine F 𝔤) where
  bracket := affineBracket F B
  add_lie := affineBracket_add_left (F := F) B
  lie_add := affineBracket_add_right (F := F) B
  lie_self := affineBracket_self (F := F) B hSymm
  leibniz_lie := by
    -- the leibniz form of Jacobi; equivalent to affineBracket_jacobi (1.6.4) modulo antisymmetry
    sorry

/-! ### §1.6 (continued): `LieAlgebra` PACKAGING OF `affineLieRing` --- OPEN, WITH THE DIAGNOSIS

What is LANDED above is (1.6.4)/(1.6.5) at the level of the bracket axioms: `affineLieRing` (a `def`,
because it depends on the data `B`) makes `𝔤̂ = 𝔤 ⊗ F[t,t⁻¹] ⊕ Fc` a LIE RING --- bilinearity
(`affineBracket_add_left/_add_right`), alternation (`affineBracket_self`, from the SYMMETRY of the form)
and Jacobi (`affineBracket_jacobi`, from the INVARIANCE of the form through the cyclicity
`invariant_trilinear_cyclic`) --- and the `F`-linearity that `LieAlgebra` adds is the landed pair
`affineBracket_smul_left`/`_smul_right`.

The remaining packaging, `LieAlgebra F (Affine F 𝔤)`, is blocked by an instance DIAMOND, not by
mathematics: in this Mathlib `class LieAlgebra (R) (L) [CommRing R] [LieRing L] extends Module R L`, so
the `LieAlgebra` instance must sit on the SAME `AddCommGroup (Affine F 𝔤)` as the `LieRing` one.  But the
ambient binders `[AddCommGroup 𝔤]` and `[LieRing 𝔤]` each supply `Zero 𝔤`/`Add 𝔤` (the
`Overlapping instance parameters` warnings above), so the `Module F (Affine F 𝔤)` of the expected type is
not the one `inferInstance`/`{ · with }` produces --- every attempt fails with
`Fields missing: smul_zero, smul_add, add_smul, zero_smul` on the `Module` parent.  Two landed repairs to
build on: (i) `AbelianLieAlg.ofModule` shows the pattern that DOES work (a structure carrying BOTH
instances, built with a `letI` that fixes the underlying `AddCommGroup` --- it works there because the
carrier is an opaque `V` with a single `AddCommGroup V` in scope); (ii) the minimal-binder shape
`[LieAlgebra F 𝔤]` alone (which supplies `LieRing 𝔤` and `Module F 𝔤` from one path) is the shape to
(MEASURED TOO: the minimal-binder attempt `[LieRing 𝔤] [LieAlgebra F 𝔤]` --- binder duplication removed --- fails in exactly the same way, with `DistribMulAction.smul_zero` mismatching on `Zero (Affine F 𝔤)`: the obstruction is inside the product/Finsupp instance path, so the repair must pin the underlying `AddCommGroup (Affine F 𝔤)` explicitly, not merely trim the binders.)
retry here, together with rebuilding `affineLieRing` on those same binders. -/



/-! ## §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" --- `IsHeisPresentation`;
* (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

/-- **(1.7.7)/(1.7.8)**: THE HEISENBERG COMMUTATION RELATIONS as data: a central `z ≠ 0` and two families
`(x_i)`, `(y_i)` with `[x_i,x_j] = [y_i,y_j] = 0`, `[x_i,y_i] = z`, `[x_i,y_j] = 0` for `i ≠ j`.  This is
the *presentation* (the book stresses "we do not assume any connection between the subscript `i` and
`deg x_i` or `deg y_j`"), not the definition; §7.1 realizes it for `𝔥̂₀`. -/
structure IsHeisPresentation (F : Type u) (𝔩 : Type v) [Field F] [CharZero 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
