DerivationTopShift.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A maximal degree shift detected on finitely many algebra generators

For an integer-graded algebra, the values of a derivation on finitely many generators have only finitely many homogeneous components. Thus a nonzero derivation has a maximal degree shift which is attained on a generator. These lemmas supply the finite-support step in the leading-derivation construction of Sections 3 and 5 of the supplied manuscript.

theorem OAI.StableCoordinate.DerivationTopShift.exists_proj_ne_zero line 27
Source documentation
A nonzero element of an internally graded algebra has a nonzero homogeneous projection.
```
theorem exists_proj_ne_zero {a : A} (ha : a ≠ 0) :
    ∃ j : ℤ, proj 𝒜 j a ≠ 0 := by
…
```

theorem OAI.StableCoordinate.DerivationTopShift.exists_generator_ne_zero line 37

Source documentation

A nonzero derivation cannot vanish on all algebra generators.

theorem exists_generator_ne_zero (g : ι → A)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (D : Derivation k A A) (hD : D ≠ 0) :
    ∃ i, D (g i) ≠ 0 := by
…

theorem OAI.StableCoordinate.DerivationTopShift.exists_maximal_generator_shift line 53

Source documentation

Finitely many generator images admit a maximal degree shift, and for a nonzero derivation the maximum is attained. No sign restriction is imposed on generator degrees or on the resulting shift.

theorem exists_maximal_generator_shift (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (D : Derivation k A A) (hD : D ≠ 0) :
    ∃ m : ℤ,
      (∀ i j, d i + m < j → proj 𝒜 j (D (g i)) = 0) ∧
      (∃ i, proj 𝒜 (d i + m) (D (g i)) ≠ 0) := by
…

theorem OAI.StableCoordinate.DerivationTopShift.exists_maximal_component line 87

Source documentation

For a family of homogeneous component derivations, vanishing outside the finite shift support can be tested solely on algebra generators.

theorem exists_maximal_component (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (D : Derivation k A A) (hD : D ≠ 0)
    (E : ℤ → Derivation k A A)
    (hE : ∀ m i, E m (g i) = proj 𝒜 (d i + m) (D (g i))) :
    ∃ m : ℤ, E m ≠ 0 ∧ ∀ n, m < n → E n = 0 := by
…

theorem OAI.StableCoordinate.DerivationTopShift.exists_top_component_and_global_bound line 110

Source documentation

Once homogeneous components are constructed, finite algebra generation provides a single upper degree-shift bound on every homogeneous input, with an attained nonzero top derivation. This is the hypothesis needed for the leading-component local-nilpotence argument.

theorem exists_top_component_and_global_bound
    (g : ι → A) (d : ι → ℤ)
    (hg : Algebra.adjoin k (Set.range g) = ⊤)
    (hhom : ∀ i, g i ∈ 𝒜 (d i))
    (D : Derivation k A A) (hD : D ≠ 0)
    (E : ℤ → Derivation k A A)
    (hE : ∀ m i (x : A), x ∈ 𝒜 i →
      E m x = proj 𝒜 (i + m) (D x)) :
    ∃ m : ℤ, E m ≠ 0 ∧
      (∀ n, m < n → E n = 0) ∧
      (∀ i (x : A), x ∈ 𝒜 i → ∀ j, i + m < j → proj 𝒜 j (D x) = 0) := by
…