Poisson algebras and Poisson ideals

StructurePoisson bracket#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra. A Poisson bracket on \(A\) is a map assigning to \(x, y \in A\) an element \(\lbrace x, y \rbrace \in A\) such that for all \(x, y, z \in A\) and \(c \in \mathbb{C}\): \(\lbrace x + y, z \rbrace = \lbrace x, z \rbrace + \lbrace y, z \rbrace\) and \(\lbrace x, y + z \rbrace = \lbrace x, y \rbrace + \lbrace x, z \rbrace\); \(\lbrace x, y \rbrace = -\lbrace y, x \rbrace\); the Leibniz rule \(\lbrace x, yz \rbrace = y \lbrace x, z \rbrace + \lbrace x, y \rbrace z\) holds; the Jacobi identity \(\lbrace x, \lbrace y, z \rbrace \rbrace + \lbrace y, \lbrace z, x \rbrace \rbrace + \lbrace z, \lbrace x, y \rbrace \rbrace = 0\) holds; and \(\lbrace c x, y \rbrace = c \lbrace x, y \rbrace\) and \(\lbrace x, c y \rbrace = c \lbrace x, y \rbrace\).

structure PoissonBracket (A : Type) [CommRing A] [Algebra ℂ A] where
  bracket : A → A → A
  add_left : ∀ x y z, bracket (x + y) z = bracket x z + bracket y z
  add_right : ∀ x y z, bracket x (y + z) = bracket x y + bracket x z
  skew : ∀ x y, bracket x y = -bracket y x
  leibniz : ∀ x y z, bracket x (y * z) = y * bracket x z + bracket x y * z
  jacobi : ∀ x y z,
    bracket x (bracket y z) + bracket y (bracket z x) +
      bracket z (bracket x y) = 0
  smul_left : ∀ (c : ℂ) (x y : A),
    bracket (c • x) y = c • bracket x y
  smul_right : ∀ (c : ℂ) (x y : A),
    bracket x (c • y) = c • bracket x y

Used by 10

Used byThe zero ideal is a Poisson ideal · Bracket with zero · Poisson ideal · Poisson prime ideal · Poisson ideals inside an ideal lie in its Poisson core · Poisson core · Universal property of the Poisson core · The Poisson core is contained in the ideal · The Poisson core is a Poisson ideal · The sum of two Poisson ideals inside an ideal

DefinitionPoisson ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket \(\lbrace \cdot, \cdot \rbrace\). An ideal \(P\) of \(A\) is a Poisson ideal when \(\lbrace a, p \rbrace \in P\) for all \(a \in A\) and all \(p \in P\).

def IsPoissonIdeal (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (P : Ideal A) : Prop :=
  ∀ (a p : A), p ∈ P → br.bracket a p ∈ P

Uses 1 · Used by 8

Statement usesPoisson bracket

Used byThe zero ideal is a Poisson ideal · Poisson prime ideal · Poisson ideals inside an ideal lie in its Poisson core · Poisson core · Universal property of the Poisson core · The Poisson core is contained in the ideal · The Poisson core is a Poisson ideal · The sum of two Poisson ideals inside an ideal

DefinitionPoisson prime ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. An ideal \(P\) of \(A\) is a Poisson prime when it is both a prime ideal and a Poisson ideal.

def IsPoissonPrime (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (P : Ideal A) : Prop :=
  P.IsPrime ∧ IsPoissonIdeal A br P

Uses 2

Statement usesPoisson ideal · Poisson bracket

DefinitionPoisson core#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. For an ideal \(J\) of \(A\), the Poisson core of \(J\) is the supremum, in the lattice of ideals of \(A\), of the set of all Poisson ideals of \(A\) contained in \(J\).

It is the largest Poisson ideal contained in \(J\) (universal property of the Poisson core).

def poissonCore (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (J : Ideal A) : Ideal A :=
  sSup {P : Ideal A | P ≤ J ∧ IsPoissonIdeal A br P}

Uses 2 · Used by 4

Statement usesPoisson ideal · Poisson bracket

Used byPoisson ideals inside an ideal lie in its Poisson core · Universal property of the Poisson core · The Poisson core is contained in the ideal · The Poisson core is a Poisson ideal

TheoremBracket with zero#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket \(\lbrace \cdot, \cdot \rbrace\). For every \(a \in A\), \(\lbrace a, 0 \rbrace = 0\).

theorem bracket_zero (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (a : A) : br.bracket a 0 = 0

Uses 1 · Used by 1

Statement usesPoisson bracket

Used byThe zero ideal is a Poisson ideal

TheoremThe zero ideal is a Poisson ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. The zero ideal of \(A\) is a Poisson ideal.

theorem bot_poisson (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) : IsPoissonIdeal A br ⊥

Uses 3 · Used by 1

Statement usesPoisson ideal · Poisson bracket

Proof usesBracket with zero

Used byThe Poisson core is a Poisson ideal

TheoremThe sum of two Poisson ideals inside an ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket, and let \(I\), \(K\) and \(J\) be ideals of \(A\). If \(I\) and \(K\) are Poisson ideals contained in \(J\), then their sum \(I + K\) is a Poisson ideal contained in \(J\).

theorem sup_poisson {A : Type} [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A)
    {J I K : Ideal A} (hI : I ≤ J ∧ IsPoissonIdeal A br I)
    (hK : K ≤ J ∧ IsPoissonIdeal A br K) :
    I ⊔ K ≤ J ∧ IsPoissonIdeal A br (I ⊔ K)

Uses 2 · Used by 1

Statement usesPoisson ideal · Poisson bracket

Used byThe Poisson core is a Poisson ideal

TheoremThe Poisson core is a Poisson ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. For every ideal \(J\) of \(A\), the Poisson core of \(J\) is a Poisson ideal.

The family of Poisson ideals contained in \(J\) is nonempty and directed (the sum of two members is again a member), so every element of the core lies in some member of the family.

theorem poissonCore_poisson (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (J : Ideal A) :
    IsPoissonIdeal A br (poissonCore A br J)

Uses 5 · Used by 1

Statement usesPoisson ideal · Poisson bracket · Poisson core

Proof usesThe zero ideal is a Poisson ideal · The sum of two Poisson ideals inside an ideal

Used byUniversal property of the Poisson core

TheoremThe Poisson core is contained in the ideal#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. For every ideal \(J\) of \(A\), the Poisson core of \(J\) is contained in \(J\).

theorem poissonCore_le (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (J : Ideal A) :
    poissonCore A br J ≤ J

Uses 3 · Used by 1

Statement usesPoisson bracket · Poisson core

Proof usesPoisson ideal

Used byUniversal property of the Poisson core

TheoremPoisson ideals inside an ideal lie in its Poisson core#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket, and let \(J\) and \(P\) be ideals of \(A\). If \(P \subseteq J\) and \(P\) is a Poisson ideal, then \(P\) is contained in the Poisson core of \(J\).

theorem le_poissonCore (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) {J P : Ideal A}
    (hP : P ≤ J ∧ IsPoissonIdeal A br P) :
    P ≤ poissonCore A br J

Uses 3 · Used by 1

Statement usesPoisson ideal · Poisson bracket · Poisson core

Used byUniversal property of the Poisson core

TheoremUniversal property of the Poisson core#✓fully proved

Let \(A\) be a commutative \(\mathbb{C}\)-algebra with a Poisson bracket. For every ideal \(J\) of \(A\), the Poisson core of \(J\) is the greatest element of the set of Poisson ideals of \(A\) contained in \(J\): it is a Poisson ideal contained in \(J\), and it contains every Poisson ideal of \(A\) contained in \(J\).

theorem poissonCore_isGreatest (A : Type) [CommRing A] [Algebra ℂ A]
    (br : PoissonBracket A) (J : Ideal A) :
    IsGreatest {P : Ideal A | P ≤ J ∧ IsPoissonIdeal A br P}
      (poissonCore A br J)

Uses 6

Statement usesPoisson ideal · Poisson bracket · Poisson core

Proof usesPoisson ideals inside an ideal lie in its Poisson core · The Poisson core is contained in the ideal · The Poisson core is a Poisson ideal

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.