LeadingComponent.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Leading components of locally nilpotent derivations

This module supplies the graded-algebra mechanism used in §5 of the source. Integer degrees are allowed, including negative degrees.

abbrev OAI.StableCoordinate.LeadingComponent.proj line 25
Source documentation
Projection to one homogeneous component, regarded as an endomorphism.
```
abbrev proj (i : ℤ) : A →ₗ[k] A := GradedAlgebra.proj 𝒜 i
```
theorem OAI.StableCoordinate.LeadingComponent.proj_mem line 27
theorem OAI.StableCoordinate.LeadingComponent.proj_of_mem line 30
theorem OAI.StableCoordinate.LeadingComponent.proj_of_mem_ne line 33
theorem OAI.StableCoordinate.LeadingComponent.proj_mul_left line 37
def OAI.StableCoordinate.LeadingComponent.componentLinear line 42
Source documentation
The part of a linear map that raises homogeneous degree by exactly m.
```
def componentLinear (D : A →ₗ[k] A) (m : ℤ) : A →ₗ[k] A :=
…
```
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_of_mem line 47
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_mem line 57
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_one line 63
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_mul line 69
def OAI.StableCoordinate.LeadingComponent.component line 99
Source documentation
Every homogeneous degree-shift component of a derivation is itself a derivation.
```
def component (D : Derivation k A A) (m : ℤ) : Derivation k A A where
…
```
theorem OAI.StableCoordinate.LeadingComponent.component_apply line 105
theorem OAI.StableCoordinate.LeadingComponent.component_of_mem line 108
theorem OAI.StableCoordinate.LeadingComponent.component_mem line 113
def OAI.StableCoordinate.LeadingComponent.DegreeLE line 119
Source documentation
Every homogeneous component above degree d vanishes.
```
def DegreeLE (d : ℤ) (x : A) : Prop :=
…
```
theorem OAI.StableCoordinate.LeadingComponent.degreeLE_of_mem line 122
theorem OAI.StableCoordinate.LeadingComponent.degreeLE_zero line 127
theorem OAI.StableCoordinate.LeadingComponent.le_of_proj_ne_zero_of_degreeLE line 131
def OAI.StableCoordinate.LeadingComponent.HasShiftLE line 139
Source documentation
A map's degree shift is bounded above by m. This does not require lower bounds and therefore applies to the source's integer gradings.
```
def HasShiftLE (D : A →ₗ[k] A) (m : ℤ) : Prop :=
…
```
theorem OAI.StableCoordinate.LeadingComponent.degreeLE_map line 142
theorem OAI.StableCoordinate.LeadingComponent.top_projection_map line 157
Source documentation
At the degree bound, only the top input component can contribute to the top output component.
```
theorem top_projection_map (D : A →ₗ[k] A) {m d : ℤ}
    (hD : HasShiftLE 𝒜 D m) {x : A} (hx : DegreeLE 𝒜 d x) :
    proj 𝒜 (d + m) (D x) = componentLinear 𝒜 D m (proj 𝒜 d x) := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.HasShiftLE, OAI.StableCoordinate.LeadingComponent.DegreeLE, OAI.StableCoordinate.LeadingComponent.proj, OAI.StableCoordinate.LeadingComponent.componentLinear
theorem OAI.StableCoordinate.LeadingComponent.degreeLE_iterate line 175
theorem OAI.StableCoordinate.LeadingComponent.top_projection_iterate line 188
Source documentation
The highest possible homogeneous component of every iterate equals the corresponding iterate of the leading component.
```
theorem top_projection_iterate (D : A →ₗ[k] A) {m i : ℤ}
    (hD : HasShiftLE 𝒜 D m) {x : A} (hx : x ∈ 𝒜 i) (n : ℕ) :
    proj 𝒜 (i + (n : ℤ) * m) ((D : A → A)^[n] x) =
      ((componentLinear 𝒜 D m : A → A)^[n] x) := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.HasShiftLE, OAI.StableCoordinate.LeadingComponent.proj, OAI.StableCoordinate.LeadingComponent.componentLinear
theorem OAI.StableCoordinate.LeadingComponent.iterate_linear_zero line 201
theorem OAI.StableCoordinate.LeadingComponent.iterate_linear_add line 206
theorem OAI.StableCoordinate.LeadingComponent.eventually_zero_add line 210
theorem OAI.StableCoordinate.LeadingComponent.locallyNilpotent_componentLinear line 227
Source documentation
Taking the highest allowed shift preserves local nilpotence. No sign assumption on m, no field hypothesis, and no characteristic hypothesis are needed for this linear-algebra fact.
```
theorem locallyNilpotent_componentLinear (D : A →ₗ[k] A) {m : ℤ}
    (hD : HasShiftLE 𝒜 D m)
    (hln : ∀ x : A, ∃ n : ℕ, (D : A → A)^[n] x = 0) :
    ∀ x : A, ∃ n : ℕ, ((componentLinear 𝒜 D m : A → A)^[n] x) = 0 := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.HasShiftLE, OAI.StableCoordinate.LeadingComponent.componentLinear
theorem OAI.StableCoordinate.LeadingComponent.locallyNilpotent_component line 243
Source documentation
The leading homogeneous component of a locally nilpotent derivation is locally nilpotent, provided no component has larger degree shift.
```
theorem locallyNilpotent_component (D : Derivation k A A) {m : ℤ}
    (hD : HasShiftLE 𝒜 D.toLinearMap m)
    (hln : ∀ x : A, ∃ n : ℕ, (D : A → A)^[n] x = 0) :
    ∀ x : A, ∃ n : ℕ, ((component 𝒜 D m : A → A)^[n] x) = 0 :=
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.HasShiftLE, OAI.StableCoordinate.LeadingComponent.component
theorem OAI.StableCoordinate.LeadingComponent.component_ne_zero line 251
Source documentation
A component is nonzero as soon as its value is nonzero on one homogeneous element.
```
theorem component_ne_zero (D : Derivation k A A) (m : ℤ)
    {i : ℤ} {x : A} (hx : x ∈ 𝒜 i) (hDx : proj 𝒜 (i + m) (D x) ≠ 0) :
    component 𝒜 D m ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.proj, OAI.StableCoordinate.LeadingComponent.component
theorem OAI.StableCoordinate.LeadingComponent.component_eq_zero_of_eq_zero line 261
Source documentation
Every component annihilates any homogeneous element annihilated by the original derivation.
```
theorem component_eq_zero_of_eq_zero (D : Derivation k A A) (m : ℤ)
    {i : ℤ} {x : A} (hx : x ∈ 𝒜 i) (hDx : D x = 0) :
    component 𝒜 D m x = 0 := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.component
theorem OAI.StableCoordinate.LeadingComponent.component_high_term_eq_zero line 269
Source documentation
If a derivation kills a sum with two distinct homogeneous degrees, its leading component kills the higher-degree summand. This is used with a³*b of degree -1 and a²*u²-d² of degree 2.
```
theorem component_high_term_eq_zero (D : Derivation k A A) {m : ℤ}
    (hD : HasShiftLE 𝒜 D.toLinearMap m)
    {i j : ℤ} {x y : A} (hx : x ∈ 𝒜 i) (hy : y ∈ 𝒜 j)
    (hij : i < j) (hxy : D (x + y) = 0) : component 𝒜 D m y = 0 := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.HasShiftLE, OAI.StableCoordinate.LeadingComponent.component
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_eq_sum line 280
theorem OAI.StableCoordinate.LeadingComponent.componentLinear_preserves line 293
Source documentation
A homogeneous component preserves any submodule that is preserved by the original map and by all grading projections.
```
theorem componentLinear_preserves (D : A →ₗ[k] A) (m : ℤ) (S : Submodule k A)
    (hS : ∀ (i : ℤ) (x : A), x ∈ S → proj 𝒜 i x ∈ S)
    (hD : ∀ x : A, x ∈ S → D x ∈ S) {x : A} (hx : x ∈ S) :
    componentLinear 𝒜 D m x ∈ S := by
…
```
Mentions: OAI.StableCoordinate.LeadingComponent.proj, OAI.StableCoordinate.LeadingComponent.componentLinear

theorem OAI.StableCoordinate.LeadingComponent.projection_preserves_of_commute line 304

Source documentation

Commuting gradings preserve one another's homogeneous submodules.

theorem projection_preserves_of_commute
    (ℬ : ℤ → Submodule k A) [GradedAlgebra ℬ]
    (hcomm : ∀ (i j : ℤ) (x : A),
      proj 𝒜 i (proj ℬ j x) = proj ℬ j (proj 𝒜 i x))
    {i j : ℤ} {x : A} (hx : x ∈ ℬ j) : proj 𝒜 i x ∈ ℬ j := by
…

Mentions: OAI.StableCoordinate.LeadingComponent.proj

theorem OAI.StableCoordinate.LeadingComponent.component_preserves_compatible_grading line 314

Source documentation

Taking an auxiliary-degree component preserves a compatible second grading whenever the original derivation preserves that grading.

theorem component_preserves_compatible_grading
    (ℬ : ℤ → Submodule k A) [GradedAlgebra ℬ]
    (hcomm : ∀ (i j : ℤ) (x : A),
      proj 𝒜 i (proj ℬ j x) = proj ℬ j (proj 𝒜 i x))
    (D : Derivation k A A) (m : ℤ)
    (hD : ∀ (j : ℤ) (x : A), x ∈ ℬ j → D x ∈ ℬ j)
    {j : ℤ} {x : A} (hx : x ∈ ℬ j) : component 𝒜 D m x ∈ ℬ j := by
…

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