CoordinateLeadingDerivation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A coordinate system produces a leading locally nilpotent derivation

This is the first half of the source's coordinate obstruction, through the construction of a nonzero homogeneous locally nilpotent derivation on the actual associated graded ring. Its distinguished invariant has negative degree; its second invariant has strictly positive degree and is nonzero. The derivation and its shift are constructed, not postulated.

def OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra line 25
Source documentation
The degree-at-most-zero part of a multiplicative integer filtration is a subalgebra.
```
def degreeZeroSubalgebra (F : ℤ → Submodule k A) [SetLike.GradedMonoid F] :
    Subalgebra k A where
…
```
theorem OAI.StableCoordinate.FilteredRees.mem_degreeZeroSubalgebra line 38
theorem OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra_ne_top_of_initial_ne_zero line 45
Source documentation
A nonzero positive-degree initial form witnesses that the degree-zero subalgebra is proper. This lets a presentation of the graded ring supply the properness input without a separate argument about coordinates.
```
theorem degreeZeroSubalgebra_ne_top_of_initial_ne_zero
    (F : ℤ → Submodule k A) [SetLike.GradedMonoid F] (hmono : Monotone F)
    {d : ℤ} (hd : 0 < d) (a : F d)
    (ha : initial F hmono d a ≠ 0) : degreeZeroSubalgebra F ≠ ⊤ := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.initial, OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra

theorem OAI.StableCoordinate.FilteredRees.exists_leading_lnd line 60

Source documentation

A nonzero locally nilpotent derivation on a separated five-generator presentation has an actual nonzero homogeneous leading derivation. All invariant initial forms remain invariant.

theorem exists_leading_lnd
    (φ : MvPolynomial (Fin 5) k →ₐ[k] A) (hφ : Function.Surjective φ)
    (hsep : (⨅ d : ℤ, Filtration.imagePiece φ d) = ⊥)
    (D : Derivation k A A) (hD : D ≠ 0)
    (hln : ∀ a, ∃ n : ℕ, ((D : A → A)^[n]) a = 0) :
    ∃ (m : ℤ) (δ : Derivation k
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))),
      δ ≠ 0 ∧
      (∀ a, ∃ n : ℕ, ((δ : _ → _)^[n]) a = 0) ∧
      (∀ (d : ℤ) (a : Filtration.imagePiece φ d),
        ∃ b : Filtration.imagePiece φ (d + m),
…

Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.FilteredRees.Gr, OAI.StableCoordinate.Filtration.imagePiece_mono

theorem OAI.StableCoordinate.FilteredRees.exists_positive_initial line 92

Source documentation

A nonzero element outside the degree-zero part has a nonzero initial form of strictly positive integer degree.

theorem exists_positive_initial
    (F : ℤ → Submodule k A) [SetLike.GradedMonoid F] (hmono : Monotone F)
    (hext : ∀ a : A, ∃ d : ℤ, a ∈ F d) (hsep : (⨅ d : ℤ, F d) = ⊥)
    {a : A} (ha : a ∉ F 0) :
    ∃ (d : ℤ) (hd : a ∈ F d), 0 < d ∧
      initial F hmono d ⟨a, hd⟩ ≠ 0 := by
…

Mentions: OAI.StableCoordinate.FilteredRees.initial

theorem OAI.StableCoordinate.FilteredRees.coordinate_produces_leading_lnd line 114

Source documentation

The first obstruction step for a polynomial coordinate system containing the distinguished negative-weight generator. It supplies, on the actual Rees associated graded ring, a nonzero homogeneous locally nilpotent derivation annihilating that generator's initial form and a nonzero positive-degree initial form.

theorem coordinate_produces_leading_lnd
    [Nontrivial A]
    (φ : MvPolynomial (Fin 5) k →ₐ[k] A) (hφ : Function.Surjective φ)
    (hsep : (⨅ d : ℤ, Filtration.imagePiece φ d) = ⊥)
    (hproper : degreeZeroSubalgebra (Filtration.imagePiece φ) ≠ ⊤)
    (e : MvPolynomial (Fin 4) k ≃ₐ[k] A) (hp : e (X 0) = φ (X 0)) :
    ∃ (m : ℤ) (δ : Derivation k
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))),
      δ ≠ 0 ∧
      (∀ a, ∃ n : ℕ, ((δ : _ → _)^[n]) a = 0) ∧
      (∀ (d : ℤ) (a : Filtration.imagePiece φ d),
…

Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra, OAI.StableCoordinate.FilteredRees.Gr, OAI.StableCoordinate.Filtration.imagePiece_mono

theorem OAI.StableCoordinate.FilteredRees.coordinate_produces_leading_lnd_of_nonunit line 150

Source documentation

In the noetherian-domain source setting, separation is a proved consequence of the nonunit negative-weight generator, not an extra obstruction assumption.

theorem coordinate_produces_leading_lnd_of_nonunit
    [IsNoetherianRing A] [IsDomain A]
    (φ : MvPolynomial (Fin 5) k →ₐ[k] A) (hφ : Function.Surjective φ)
    (hpunit : ¬ IsUnit (φ (X 0)))
    (hproper : degreeZeroSubalgebra (Filtration.imagePiece φ) ≠ ⊤)
    (e : MvPolynomial (Fin 4) k ≃ₐ[k] A) (hp : e (X 0) = φ (X 0)) :
    ∃ (m : ℤ) (δ : Derivation k
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))),
      δ ≠ 0 ∧
      (∀ a, ∃ n : ℕ, ((δ : _ → _)^[n]) a = 0) ∧
      (∀ (d : ℤ) (a : Filtration.imagePiece φ d),
…

Mentions: OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra, OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.FilteredRees.Gr, OAI.StableCoordinate.Filtration.imagePiece_mono

theorem OAI.StableCoordinate.FilteredRees.coordinate_produces_leading_lnd_of_noetherian_domain line 175

Source documentation

When coordinates are supplied, the noetherian-domain and nonunit facts required for separation follow from that coordinate equivalence. Thus the only filtration input still needed is properness of its degree-zero part, which the graded-presentation theorem supplies.

theorem coordinate_produces_leading_lnd_of_noetherian_domain
    [IsNoetherianRing k] [IsDomain k]
    (φ : MvPolynomial (Fin 5) k →ₐ[k] A) (hφ : Function.Surjective φ)
    (hproper : degreeZeroSubalgebra (Filtration.imagePiece φ) ≠ ⊤)
    (e : MvPolynomial (Fin 4) k ≃ₐ[k] A) (hp : e (X 0) = φ (X 0)) :
    ∃ (m : ℤ) (δ : Derivation k
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))
      (Gr (Filtration.imagePiece φ) (Filtration.imagePiece_mono φ))),
      δ ≠ 0 ∧
      (∀ a, ∃ n : ℕ, ((δ : _ → _)^[n]) a = 0) ∧
      (∀ (d : ℤ) (a : Filtration.imagePiece φ d),
        ∃ b : Filtration.imagePiece φ (d + m),
…

Mentions: OAI.StableCoordinate.FilteredRees.degreeZeroSubalgebra, OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.FilteredRees.Gr, OAI.StableCoordinate.Filtration.imagePiece_mono