OAI/AlgebraicGeometry/StableCoordinate/GradedPresentationKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StableCoordinate.GradedPresentationKernel.mem_boundedImage_iff line 28

   Source documentation

   Membership in the actual image of the weighted filtration is precisely the existence of a bounded polynomial representative.

   theorem mem_boundedImage_iff (w : σ → ℤ)
       (φ : MvPolynomial σ k →ₐ[k] A) (p : MvPolynomial σ k) (d : ℤ) :
       φ p ∈ (boundedSubmodule w d).map φ.toLinearMap ↔
         ∃ r : MvPolynomial σ k, Bounded w r d ∧ φ r = φ p := Iff.rfl

2. theorem OAI.StableCoordinate.GradedPresentationKernel.homogeneous_image_mem_lower_iff line 35

   Source documentation

   A homogeneous polynomial maps one filtration step lower exactly when it belongs to the ideal generated by the top component of the defining relation.

   theorem homogeneous_image_mem_lower_iff [IsDomain k]
       (w : σ → ℤ) (φ : MvPolynomial σ k →ₐ[k] A)
       (F : ℤ → Submodule k A)
       (hF : ∀ (p : MvPolynomial σ k) (d : ℤ),
         φ p ∈ F d ↔ ∃ r : MvPolynomial σ k, Bounded w r d ∧ φ r = φ p)
       (H : MvPolynomial σ k) (e : ℤ)
       (hH : Bounded w H e) (hHt : weightedHomogeneousComponent w e H ≠ 0)
       (hker : RingHom.ker φ.toRingHom = Ideal.span ({H} : Set (MvPolynomial σ k)))
       {p : MvPolynomial σ k} {d : ℤ} (hp : IsWeightedHomogeneous w p d) :
       φ p ∈ F (d - 1) ↔
         p ∈ Ideal.span ({weightedHomogeneousComponent w e H} : Set (MvPolynomial σ k)) := by
   …

3. theorem OAI.StableCoordinate.GradedPresentationKernel.top_principal_mem_iff line 62

   Source documentation

   Top components generate a homogeneous principal ideal, including for arbitrary integer weights.

   theorem top_principal_mem_iff (w : σ → ℤ) (H p : MvPolynomial σ k) (e : ℤ) :
       p ∈ Ideal.span ({weightedHomogeneousComponent w e H} : Set (MvPolynomial σ k)) ↔
         ∀ d : ℤ, weightedHomogeneousComponent w d p ∈
           Ideal.span ({weightedHomogeneousComponent w e H} : Set (MvPolynomial σ k)) := by
   …

4. theorem OAI.StableCoordinate.GradedPresentationKernel.kernel_eq_top_principal line 78

   Source documentation

   Exact kernel theorem for a polynomial-to-Rees construction whose coefficients are the images of weighted homogeneous components. The hF and hcoeff arguments are compatibility identities for the constructed maps, not assumptions about the principal theorem.

   theorem kernel_eq_top_principal [IsDomain k]
       (w : σ → ℤ) (φ : MvPolynomial σ k →ₐ[k] A)
       (F : ℤ → Submodule k A) [SetLike.GradedMonoid F] (hmono : Monotone F)
       (hF : ∀ (p : MvPolynomial σ k) (d : ℤ),
         φ p ∈ F d ↔ ∃ r : MvPolynomial σ k, Bounded w r d ∧ φ r = φ p)
       (H : MvPolynomial σ k) (e : ℤ)
       (hH : Bounded w H e) (hHt : weightedHomogeneousComponent w e H ≠ 0)
       (hker : RingHom.ker φ.toRingHom = Ideal.span ({H} : Set (MvPolynomial σ k)))
       (ψ : MvPolynomial σ k →ₐ[k] FilteredRees.rees F)
       (hcoeff : ∀ (p : MvPolynomial σ k) (d : ℤ),
         ((ψ p : FilteredRees.rees F) : LaurentPolynomial A).coeff d =
           φ (weightedHomogeneousComponent w d p)) :
   …

   Mentions: OAI.StableCoordinate.FilteredRees.rees