OAI/AlgebraicGeometry/StableCoordinate/FiltrationDerivationShift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Bounded derivation shifts for the integer source filtration

This proves the generator-bound step in equation gr:shift of the source. It uses the actual five-variable integer filtration, including negative indices. Bounds on derivatives of the five generators imply one common bound on the derivative of every filtration piece.

  1. theorem OAI.StableCoordinate.Filtration.image_monomial_mem line 24

    Source documentation

    The image of each monomial lies in its assigned integer filtration layer.

    theorem image_monomial_mem (φ : MvPolynomial (Fin 5) K →ₐ[K] A)
    (s : Fin 5 →₀ ℕ) (c : K) :
    φ (monomial s c) ∈ imagePiece φ (monomialWeight s) :=
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight

  2. theorem OAI.StableCoordinate.Filtration.monomialWeight_single line 30

    Source documentation

    The weight of a pure power is its exponent times the variable weight.

    theorem monomialWeight_single (i : Fin 5) (n : ℕ) :
    monomialWeight (Finsupp.single i n) =
      n • monomialWeight (Finsupp.single i 1) := by
…

    Mentions: OAI.StableCoordinate.Filtration.monomialWeight

  3. theorem OAI.StableCoordinate.Filtration.derivation_mul_mem_imagePiece line 36

    Source documentation

    The product rule propagates a common filtration shift through multiplication.

    theorem derivation_mul_mem_imagePiece
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (D : Derivation K A A)
    {a b : A} {d e m : ℤ}
    (ha : a ∈ imagePiece φ d) (hb : b ∈ imagePiece φ e)
    (hDa : D a ∈ imagePiece φ (d + m))
    (hDb : D b ∈ imagePiece φ (e + m)) :
    D (a * b) ∈ imagePiece φ (d + e + m) := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece

  4. theorem OAI.StableCoordinate.Filtration.derivation_pow_mem_imagePiece line 51

    Source documentation

    The product rule propagates a common filtration shift through every power.

    theorem derivation_pow_mem_imagePiece
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (D : Derivation K A A)
    {a : A} {d m : ℤ}
    (ha : a ∈ imagePiece φ d) (hDa : D a ∈ imagePiece φ (d + m))
    (n : ℕ) : D (a ^ n) ∈ imagePiece φ (n • d + m) := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece

  5. theorem OAI.StableCoordinate.Filtration.derivation_monomial_mem_imagePiece line 65

    Source documentation

    A bound on generator derivatives gives the exact monomial-weight bound.

    theorem derivation_monomial_mem_imagePiece
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (D : Derivation K A A) (m : ℤ)
    (hD : ∀ i : Fin 5, D (φ (X i)) ∈
      imagePiece φ (monomialWeight (Finsupp.single i 1) + m))
    (s : Fin 5 →₀ ℕ) (c : K) :
    D (φ (monomial s c)) ∈ imagePiece φ (monomialWeight s + m) := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight

  6. theorem OAI.StableCoordinate.Filtration.derivation_source_piece_mem_imagePiece line 94

    Source documentation

    Generator bounds extend to every element of a source filtration piece.

    theorem derivation_source_piece_mem_imagePiece
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (D : Derivation K A A) (m : ℤ)
    (hD : ∀ i : Fin 5, D (φ (X i)) ∈
      imagePiece φ (monomialWeight (Finsupp.single i 1) + m))
    {q : MvPolynomial (Fin 5) K} {d : ℤ} (hq : q ∈ piece K d) :
    D (φ q) ∈ imagePiece φ (d + m) := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight, OAI.StableCoordinate.Filtration.piece

  7. theorem OAI.StableCoordinate.Filtration.derivation_imagePiece_le line 113

    Source documentation

    The source's bounded-shift assertion, for every integer filtration degree.

    theorem derivation_imagePiece_le
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (D : Derivation K A A) (m : ℤ)
    (hD : ∀ i : Fin 5, D (φ (X i)) ∈
      imagePiece φ (monomialWeight (Finsupp.single i 1) + m))
    (d : ℤ) :
    imagePiece φ d ≤ (imagePiece φ (d + m)).comap D.toLinearMap := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight

  8. theorem OAI.StableCoordinate.Filtration.derivation_eq_zero_of_generator_values line 123

    Source documentation

    A derivation vanishing on all presentation generators is zero.

    theorem derivation_eq_zero_of_generator_values
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (D : Derivation K A A) (hD : ∀ i : Fin 5, D (φ (X i)) = 0) : D = 0 := by
…
  9. theorem OAI.StableCoordinate.Filtration.exists_ne_zero_generator_value line 135

    Source documentation

    A nonzero derivation has a nonzero value on a presentation generator.

    theorem exists_ne_zero_generator_value
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (D : Derivation K A A) (hD : D ≠ 0) :
    ∃ i : Fin 5, D (φ (X i)) ≠ 0 := by
…
  10. theorem OAI.StableCoordinate.Filtration.exists_derivation_imagePiece_shift line 145

    Source documentation

    Exhaustiveness and the finite set of presentation generators supply a uniform integer shift for every derivation.

    theorem exists_derivation_imagePiece_shift
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (D : Derivation K A A) :
    ∃ m : ℤ, ∀ d : ℤ,
      imagePiece φ d ≤ (imagePiece φ (d + m)).comap D.toLinearMap := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece

  11. theorem OAI.StableCoordinate.Filtration.exists_attained_derivation_imagePiece_shift line 166

    Source documentation

    Separation makes the maximal generator shift sharp. Some nonzero generator image lands in degree weight + m, but not the preceding layer. This is exactly the nonvanishing criterion for the source's leading derivation.

    theorem exists_attained_derivation_imagePiece_shift
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (hsep : (⨅ d : ℤ, imagePiece φ d) = ⊥)
    (D : Derivation K A A) (hD : D ≠ 0) :
    ∃ (m : ℤ) (i : Fin 5),
      D (φ (X i)) ≠ 0 ∧
      D (φ (X i)) ∈ imagePiece φ (monomialWeight (Finsupp.single i 1) + m) ∧
      D (φ (X i)) ∉ imagePiece φ (monomialWeight (Finsupp.single i 1) + m - 1) ∧
      ∀ d : ℤ, imagePiece φ d ≤ (imagePiece φ (d + m)).comap D.toLinearMap := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight

  12. theorem OAI.StableCoordinate.Filtration.exists_attained_derivation_shift_with_initial_generator line 213

    Source documentation

    For the attained maximal shift, both the source generator and its derivative have nonzero initial classes. No separate exact-degree theorem for the source generators is needed to obtain this conclusion.

    theorem exists_attained_derivation_shift_with_initial_generator
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (hsep : (⨅ d : ℤ, imagePiece φ d) = ⊥)
    (D : Derivation K A A) (hD : D ≠ 0) :
    ∃ (m : ℤ) (i : Fin 5),
      φ (X i) ∈ imagePiece φ (monomialWeight (Finsupp.single i 1)) ∧
      φ (X i) ∉ imagePiece φ (monomialWeight (Finsupp.single i 1) - 1) ∧
      D (φ (X i)) ∈ imagePiece φ (monomialWeight (Finsupp.single i 1) + m) ∧
      D (φ (X i)) ∉ imagePiece φ (monomialWeight (Finsupp.single i 1) + m - 1) ∧
      ∀ d : ℤ, imagePiece φ d ≤ (imagePiece φ (d + m)).comap D.toLinearMap := by
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight

  13. theorem OAI.StableCoordinate.Filtration.exists_attained_derivation_shift_of_nonunit line 237

    Source documentation

    Specialization of the attained-shift theorem to the noetherian-domain source setting, where the image of the negative-weight variable is a nonunit.

    theorem exists_attained_derivation_shift_of_nonunit
    [IsNoetherianRing A] [IsDomain A]
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hφ : Function.Surjective φ)
    (hp : ¬ IsUnit (φ (X 0))) (D : Derivation K A A) (hD : D ≠ 0) :
    ∃ (m : ℤ) (i : Fin 5),
      φ (X i) ∈ imagePiece φ (monomialWeight (Finsupp.single i 1)) ∧
      φ (X i) ∉ imagePiece φ (monomialWeight (Finsupp.single i 1) - 1) ∧
      D (φ (X i)) ∈ imagePiece φ (monomialWeight (Finsupp.single i 1) + m) ∧
      D (φ (X i)) ∉ imagePiece φ (monomialWeight (Finsupp.single i 1) + m - 1) ∧
      ∀ d : ℤ, imagePiece φ d ≤ (imagePiece φ (d + m)).comap D.toLinearMap :=
…

    Mentions: OAI.StableCoordinate.Filtration.imagePiece, OAI.StableCoordinate.Filtration.monomialWeight