OAI/AlgebraicGeometry/StableCoordinate/WeightedInitialKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The homogeneous kernel criterion for a principal filtered quotient

A homogeneous polynomial disappears in the associated graded quotient by (H) exactly when it is divisible by the highest component of H. The statement is expressed in terms of representatives of lower weight; it thus supplies the kernel computation independently of a particular associated-graded construction.

  1. lemma OAI.StableCoordinate.WeightedInitial.bounded_of_homogeneous line 23
  2. lemma OAI.StableCoordinate.WeightedInitial.top_sub_lower line 28
  3. theorem OAI.StableCoordinate.WeightedInitial.homogeneous_quotient_kernel_iff line 36

    Source documentation

    The homogeneous representative criterion for the kernel of the associated -graded map from a weighted polynomial ring modulo one relation.

    theorem homogeneous_quotient_kernel_iff
    (w : σ → ℤ) (H : MvPolynomial σ K) (e : ℤ)
    (hH : Bounded w H e) (hHt : weightedHomogeneousComponent w e H ≠ 0)
    {p : MvPolynomial σ K} {d : ℤ} (hp : IsWeightedHomogeneous w p d) :
    (∃ r : MvPolynomial σ K, Bounded w r (d - 1) ∧
      p - r ∈ Ideal.span ({H} : Set (MvPolynomial σ K))) ↔
    p ∈ Ideal.span ({weightedHomogeneousComponent w e H} : Set (MvPolynomial σ K)) := by
…

    Mentions: OAI.StableCoordinate.WeightedInitial.Bounded