LeadingLocallyNilpotent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A nonzero leading locally nilpotent derivation

This module combines finite algebra generation with the actual homogeneous component construction. It establishes the auxiliary-grading passage in §5 of the source without assuming a global degree-shift bound.

theorem OAI.StableCoordinate.LeadingComponent.exists_nonzero_locallyNilpotent_component line 25

Source documentation

Every nonzero locally nilpotent derivation of a finitely generated integer-graded algebra with homogeneous generators has a nonzero leading homogeneous locally nilpotent component.

theorem exists_nonzero_locallyNilpotent_component
    (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (hhom : ∀ i, g i ∈ 𝒜 (d i))
    (D : Derivation k A A) (hD : D ≠ 0)
    (hln : ∀ x : A, ∃ n : ℕ, (D : A → A)^[n] x = 0) :
    ∃ m : ℤ, component 𝒜 D m ≠ 0 ∧
      HasShiftLE 𝒜 D.toLinearMap m ∧
      (∀ x : A, ∃ n : ℕ, ((component 𝒜 D m : A → A)^[n] x) = 0) := by
…

Mentions: OAI.StableCoordinate.LeadingComponent.component, OAI.StableCoordinate.LeadingComponent.HasShiftLE

theorem OAI.StableCoordinate.LeadingComponent.exists_nonzero_locallyNilpotent_component_annihilating_top line 42

Source documentation

The source's auxiliary-grading reduction: if a locally nilpotent derivation annihilates a sum of two distinct homogeneous degrees, its nonzero leading locally nilpotent component annihilates the higher part.

theorem exists_nonzero_locallyNilpotent_component_annihilating_top
    (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (hhom : ∀ i, g i ∈ 𝒜 (d i))
    (D : Derivation k A A) (hD : D ≠ 0)
    (hln : ∀ x : A, ∃ n : ℕ, (D : A → A)^[n] x = 0)
    {i j : ℤ} {x y : A} (hx : x ∈ 𝒜 i) (hy : y ∈ 𝒜 j)
    (hij : i < j) (hxy : D (x + y) = 0) :
    ∃ m : ℤ, component 𝒜 D m ≠ 0 ∧
      (∀ z : A, ∃ n : ℕ, ((component 𝒜 D m : A → A)^[n] z) = 0) ∧
      component 𝒜 D m y = 0 := by
…

Mentions: OAI.StableCoordinate.LeadingComponent.component

theorem OAI.StableCoordinate.LeadingComponent.exists_nonzero_locallyNilpotent_component_compatible line 60

Source documentation

The leading component also preserves a compatible second grading. This packages the full leading-component step of the source's rigidity proof, including preservation of the fiber weights.

theorem exists_nonzero_locallyNilpotent_component_compatible
    (ℬ : ℤ → Submodule k A) [GradedAlgebra ℬ]
    (hcomm : ∀ (i j : ℤ) (x : A),
      proj 𝒜 i (proj ℬ j x) = proj ℬ j (proj 𝒜 i x))
    (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (hhom : ∀ i, g i ∈ 𝒜 (d i))
    (D : Derivation k A A) (hD : D ≠ 0)
    (hln : ∀ x : A, ∃ n : ℕ, (D : A → A)^[n] x = 0)
    (hpres : ∀ (r : ℤ) (z : A), z ∈ ℬ r → D z ∈ ℬ r)
    {i j : ℤ} {x y : A} (hx : x ∈ 𝒜 i) (hy : y ∈ 𝒜 j)
    (hij : i < j) (hxy : D (x + y) = 0) :
…

Mentions: OAI.StableCoordinate.LeadingComponent.proj