GradedPresentationMap.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The polynomial map onto the actual associated graded algebra

For the source's exact integer weight and the quotient/image filtration, this file constructs the algebra map from the five-variable polynomial ring to the Rees special fiber and proves surjectivity. No identification of the associated graded ring is assumed.

abbrev OAI.StableCoordinate.GradedPresentationMap.imageGr line 27
def OAI.StableCoordinate.GradedPresentationMap.variableElement line 30
Source documentation
A variable as a member of its assigned image-filtration piece.
```
def variableElement (i : Fin 5) :
    imagePiece φ (monomialWeight (Finsupp.single i 1)) :=
…
```
def OAI.StableCoordinate.GradedPresentationMap.reesMap line 35
Source documentation
The homogeneous polynomial map into the extended Rees algebra.
```
def reesMap : MvPolynomial (Fin 5) k →ₐ[k] rees (imagePiece φ) :=
…
```
def OAI.StableCoordinate.GradedPresentationMap.gradedMap line 41
Source documentation
The natural ring map from the source polynomial ring into the actual associated graded algebra.
```
def gradedMap : MvPolynomial (Fin 5) k →ₐ[k] imageGr φ :=
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.imageGr
theorem OAI.StableCoordinate.GradedPresentationMap.gradedMap_X line 44
theorem OAI.StableCoordinate.GradedPresentationMap.monomialWeight_single line 49
theorem OAI.StableCoordinate.GradedPresentationMap.monomialWeight_eq_weight line 56
Source documentation
Compatibility of the source's explicit exponent formula with mathlib's general weighted-polynomial API.
```
theorem monomialWeight_eq_weight (w : Fin 5 → ℤ)
    (hw : ∀ i, w i = monomialWeight (Finsupp.single i 1)) :
    monomialWeight = Finsupp.weight w := by
…
```
def OAI.StableCoordinate.GradedPresentationMap.monomialElement line 65
Source documentation
A monomial as a member of its assigned image-filtration piece.
```
def monomialElement (e : Fin 5 →₀ ℕ) (c : k) :
    imagePiece φ (monomialWeight e) :=
…
```
theorem OAI.StableCoordinate.GradedPresentationMap.reesMap_monomial_coe line 70
Source documentation
The Rees map preserves each monomial with its exact integer weight.
```
theorem reesMap_monomial_coe (e : Fin 5 →₀ ℕ) (c : k) :
    (reesMap φ (monomial e c) : LaurentPolynomial A) =
      AddMonoidAlgebra.single (monomialWeight e) (φ (monomial e c)) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.reesMap
theorem OAI.StableCoordinate.GradedPresentationMap.gradedMap_monomial line 91
Source documentation
Exact formula for the homogeneous symbol of every source monomial.
```
theorem gradedMap_monomial (e : Fin 5 →₀ ℕ) (c : k) :
    gradedMap φ (monomial e c) =
      initial (imagePiece φ) (imagePiece_mono φ) (monomialWeight e)
        (monomialElement φ e c) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.gradedMap, OAI.StableCoordinate.GradedPresentationMap.monomialElement
theorem OAI.StableCoordinate.GradedPresentationMap.reesMap_coeff line 103
Source documentation
The exact coefficient formula, useful for identifying the kernel of the polynomial map degree by degree.
```
theorem reesMap_coeff (p : MvPolynomial (Fin 5) k) (d : ℤ) :
    (reesMap φ p : LaurentPolynomial A).coeff d =
      φ (∑ e ∈ p.support, if monomialWeight e = d then monomial e (p.coeff e) else 0) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.reesMap
theorem OAI.StableCoordinate.GradedPresentationMap.reesMap_coeff_weightedComponent line 125
Source documentation
The Rees representative's degree-d coefficient is the image of the mathlib weighted homogeneous component.
```
theorem reesMap_coeff_weightedComponent (w : Fin 5 → ℤ)
    (hw : ∀ i, w i = monomialWeight (Finsupp.single i 1))
    (p : MvPolynomial (Fin 5) k) (d : ℤ) :
    (reesMap φ p : LaurentPolynomial A).coeff d =
      φ (weightedHomogeneousComponent w d p) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.reesMap
theorem OAI.StableCoordinate.GradedPresentationMap.reesMap_coe_of_homogeneous line 135
Source documentation
A homogeneous source polynomial has precisely its expected Rees symbol.
```
theorem reesMap_coe_of_homogeneous (p : MvPolynomial (Fin 5) k) (d : ℤ)
    (hp : ∀ e ∈ p.support, monomialWeight e = d) :
    (reesMap φ p : LaurentPolynomial A) = AddMonoidAlgebra.single d (φ p) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.reesMap
theorem OAI.StableCoordinate.GradedPresentationMap.gradedMap_of_homogeneous line 161
Source documentation
The natural map on any homogeneous polynomial equals the homogeneous initial form represented by its image under the presentation.
```
theorem gradedMap_of_homogeneous (p : MvPolynomial (Fin 5) k) (d : ℤ)
    (hp : ∀ e ∈ p.support, monomialWeight e = d) :
    gradedMap φ p = initial (imagePiece φ) (imagePiece_mono φ) d
      ⟨φ p, p, (mem_piece_iff k).mpr (fun e he => (hp e he).le), rfl⟩ := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.gradedMap
def OAI.StableCoordinate.GradedPresentationMap.initialLinear line 171
Source documentation
The homogeneous symbol is linear within a fixed filtration degree.
```
def initialLinear (d : ℤ) : imagePiece φ d →ₗ[k] imageGr φ where
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.imageGr
def OAI.StableCoordinate.GradedPresentationMap.imagePieceMap line 183
Source documentation
The presentation map restricted to one source filtration piece.
```
def imagePieceMap (d : ℤ) : piece k d →ₗ[k] imagePiece φ d where
…
```
def OAI.StableCoordinate.GradedPresentationMap.sourceInitial line 189
Source documentation
A source polynomial of weight at most d has a degree-d symbol.
```
def sourceInitial (d : ℤ) : piece k d →ₗ[k] imageGr φ :=
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.imageGr
theorem OAI.StableCoordinate.GradedPresentationMap.sourceInitial_apply line 192
theorem OAI.StableCoordinate.GradedPresentationMap.sourceInitial_monomial_mem_range line 198
Source documentation
Every source monomial symbol is in the range of the polynomial map; symbols placed in a strictly larger degree vanish.
```
theorem sourceInitial_monomial_mem_range (e : Fin 5 →₀ ℕ) (c : k)
    (d : ℤ) (h : monomialWeight e ≤ d) :
    sourceInitial φ d ⟨monomial e c, monomial_mem_piece k h c⟩ ∈
      (gradedMap φ).range := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.sourceInitial, OAI.StableCoordinate.GradedPresentationMap.gradedMap

theorem OAI.StableCoordinate.GradedPresentationMap.linear_span_range line 213

Source documentation

Linear maps out of a span can be tested on its specified generators.

private theorem linear_span_range
    {M N : Type*} [AddCommMonoid M] [AddCommMonoid N]
    [Module k M] [Module k N] (s : Set M) (L : Submodule.span k s →ₗ[k] N)
    (S : Submodule k N)
    (h : ∀ (p : M) (hp : p ∈ s), L ⟨p, Submodule.subset_span hp⟩ ∈ S)
    (p : Submodule.span k s) : L p ∈ S := by
…

theorem OAI.StableCoordinate.GradedPresentationMap.sourceInitial_mem_range line 236
Source documentation
Every symbol of a polynomial in a source filtration piece is in range.
```
theorem sourceInitial_mem_range (d : ℤ) (p : piece k d) :
    sourceInitial φ d p ∈ (gradedMap φ).range := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.sourceInitial, OAI.StableCoordinate.GradedPresentationMap.gradedMap
theorem OAI.StableCoordinate.GradedPresentationMap.initial_mem_range line 244
Source documentation
Every homogeneous class of the actual image filtration is in range.
```
theorem initial_mem_range (d : ℤ) (a : imagePiece φ d) :
    initial (imagePiece φ) (imagePiece_mono φ) d a ∈ (gradedMap φ).range := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.gradedMap
theorem OAI.StableCoordinate.GradedPresentationMap.gradedMap_surjective line 252
Source documentation
The source polynomial map onto the actual associated graded algebra is surjective. This uses only the image filtration, not a proposed presentation.
```
theorem gradedMap_surjective : Function.Surjective (gradedMap φ) := by
…
```
Mentions: OAI.StableCoordinate.GradedPresentationMap.gradedMap