OAI/Algebra/AffineCancellation/GradedLND.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ComplexCancellation.GradedLND.proj line 12
2. lemma OAI.ComplexCancellation.GradedLND.proj_mem line 14
3. lemma OAI.ComplexCancellation.GradedLND.proj_of_mem line 17
4. lemma OAI.ComplexCancellation.GradedLND.proj_of_mem_ne line 20
5. lemma OAI.ComplexCancellation.GradedLND.proj_mul_left line 23
6. lemma OAI.ComplexCancellation.GradedLND.proj_mul_right line 27
7. def OAI.ComplexCancellation.GradedLND.componentLinear line 32

   Source documentation

   The shift-j component of a linear map, on an arbitrary ℤ-graded algebra.

   def componentLinear (D : R →ₗ[k] R) (j : ℤ) : R →ₗ[k] R :=
   …

8. lemma OAI.ComplexCancellation.GradedLND.componentLinear_of_mem line 37
9. lemma OAI.ComplexCancellation.GradedLND.componentLinear_leibniz line 47
10. def OAI.ComplexCancellation.GradedLND.component line 65
11. lemma OAI.ComplexCancellation.GradedLND.component_of_mem line 70
12. lemma OAI.ComplexCancellation.GradedLND.component_homogeneous line 74
13. def OAI.ComplexCancellation.GradedLND.filtration line 80

    Source documentation

    The increasing filtration associated to an integer grading.

    def filtration (d : ℤ) : Submodule k R := ⨆ i : {i : ℤ // i ≤ d}, G i
    …

14. lemma OAI.ComplexCancellation.GradedLND.mem_filtration line 83
15. lemma OAI.ComplexCancellation.GradedLND.filtration_mono line 87
16. lemma OAI.ComplexCancellation.GradedLND.proj_filtration line 92
17. lemma OAI.ComplexCancellation.GradedLND.exists_filtration line 102
18. def OAI.ComplexCancellation.GradedLND.ShiftBound line 112
19. lemma OAI.ComplexCancellation.GradedLND.map_filtration line 116
20. lemma OAI.ComplexCancellation.GradedLND.top_map line 126
21. lemma OAI.ComplexCancellation.GradedLND.iterate_top line 143
22. lemma OAI.ComplexCancellation.GradedLND.component_locallyNilpotent line 157

    Source documentation

    Local nilpotence survives passage to the highest homogeneous component, including for gradings with negative degrees.

    lemma component_locallyNilpotent {D : Derivation k R R} {j : ℤ}
        (hD : ShiftBound G D j) (hln : ∀ r : R, ∃ n : ℕ, (D : R → R)^[n] r = 0) :
        ∀ r : R, ∃ n : ℕ, (component G D j : R → R)^[n] r = 0 := by
    …

    Mentions: OAI.ComplexCancellation.GradedLND.ShiftBound, OAI.ComplexCancellation.GradedLND.component

23. lemma OAI.ComplexCancellation.GradedLND.eq_zero_of_projections line 186
24. lemma OAI.ComplexCancellation.GradedLND.mem_filtration_iff line 191
25. lemma OAI.ComplexCancellation.GradedLND.shiftBound_of_components line 207
26. lemma OAI.ComplexCancellation.GradedLND.component_exists line 216
27. lemma OAI.ComplexCancellation.GradedLND.homogeneous_generators line 234
28. lemma OAI.ComplexCancellation.GradedLND.component_bounded line 254
29. theorem OAI.ComplexCancellation.GradedLND.highest line 274

    Source documentation

    Every nonzero locally nilpotent derivation of a finite type graded algebra has a nonzero highest component, itself locally nilpotent.

    theorem highest [Algebra.FiniteType k R] (D : Derivation k R R) (hD : D ≠ 0)
        (hln : ∀ r : R, ∃ n : ℕ, (D : R → R)^[n] r = 0) :
        ∃ j, component G D j ≠ 0 ∧ ShiftBound G D j ∧
          ∀ r : R, ∃ n : ℕ, (component G D j : R → R)^[n] r = 0 := by
    …

    Mentions: OAI.ComplexCancellation.GradedLND.component, OAI.ComplexCancellation.GradedLND.ShiftBound