AssociatedGradedPresentation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The actual associated graded presentation for the source hypersurface

This identifies the Rees special fiber of the source quotient filtration with the exact degeneration ring Obstruction.G, with its independent generators.

theorem OAI.StableCoordinate.AssociatedGradedPresentation.monomialWeight_eq_weight line 21
Source documentation
The two source-weight APIs describe precisely the same integer weight.
```
theorem monomialWeight_eq_weight :
    Filtration.monomialWeight = Finsupp.weight presentationWeight := by
…
```
Mentions: OAI.StableCoordinate.Filtration.monomialWeight
theorem OAI.StableCoordinate.AssociatedGradedPresentation.piece_eq_boundedSubmodule line 32
Source documentation
The span-of-monomials source filtration agrees with the coefficientwise weighted filtration used to establish the leading-relation theorem.
```
theorem piece_eq_boundedSubmodule (d : ℤ) :
    Filtration.piece k d = boundedSubmodule presentationWeight d := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.AssociatedGradedPresentation.imagePiece_mem_iff line 42
Source documentation
Every bounded image representative criterion is now proved for the actual source filtration, rather than assumed for an abstract filtered algebra.
```
theorem imagePiece_mem_iff (φ : P k 5 →ₐ[k] A) (p : P k 5) (d : ℤ) :
    φ p ∈ imagePiece φ d ↔
      ∃ r : P k 5, Bounded presentationWeight r d ∧ φ r = φ p := by
…
```
theorem OAI.StableCoordinate.AssociatedGradedPresentation.reesMap_coeff_weighted line 51
Source documentation
The coefficient of the actual source Rees map is the image of the matching weighted homogeneous component.
```
theorem reesMap_coeff_weighted (φ : P k 5 →ₐ[k] A) (p : P k 5) (d : ℤ) :
    (reesMap φ p : LaurentPolynomial A).coeff d =
      φ (weightedHomogeneousComponent presentationWeight d p) := by
…
```
abbrev OAI.StableCoordinate.AssociatedGradedPresentation.quotientMap line 61
Source documentation
The actual polynomial presentation map of the source hypersurface.
```
abbrev quotientMap : P k 5 →ₐ[k] Obstruction.A k := Ideal.Quotient.mkₐ k (idealA k)
```
Mentions: OAI.StableCoordinate.Obstruction.A
abbrev OAI.StableCoordinate.AssociatedGradedPresentation.associatedGraded line 64
Source documentation
The actual Rees associated graded algebra of the source image filtration.
```
abbrev associatedGraded := imageGr (quotientMap k)
```
Mentions: OAI.StableCoordinate.AssociatedGradedPresentation.quotientMap
abbrev OAI.StableCoordinate.AssociatedGradedPresentation.gradedPresentationMap line 67
Source documentation
The actual polynomial map onto the source's associated graded algebra.
```
abbrev gradedPresentationMap : P k 5 →ₐ[k] associatedGraded k :=
…
```
Mentions: OAI.StableCoordinate.AssociatedGradedPresentation.associatedGraded
theorem OAI.StableCoordinate.AssociatedGradedPresentation.homogeneous_symbol_eq_zero_iff line 74
Source documentation
Vanishing of an actual homogeneous symbol is exactly vanishing modulo the exact relation Hstar.
```
theorem homogeneous_symbol_eq_zero_iff (p : P k 5) (d : ℤ)
    (hp : p.IsWeightedHomogeneous presentationWeight d) :
    quotientMap k p ∈ imagePiece (quotientMap k) (d - 1) ↔ p ∈ idealG k := by
…
```
Mentions: OAI.StableCoordinate.AssociatedGradedPresentation.quotientMap
theorem OAI.StableCoordinate.AssociatedGradedPresentation.gradedPresentation_ker line 86
Source documentation
The full kernel of the actual polynomial map is exactly (Hstar).
```
theorem gradedPresentation_ker :
    RingHom.ker (gradedPresentationMap k).toRingHom = idealG k := by
…
```
Mentions: OAI.StableCoordinate.AssociatedGradedPresentation.gradedPresentationMap
def OAI.StableCoordinate.AssociatedGradedPresentation.associatedGradedEquiv line 99
Source documentation
The complete concrete associated-graded presentation, with no graded-domain or source-presentation hypothesis added.
```
def associatedGradedEquiv : Obstruction.G k ≃ₐ[k] associatedGraded k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.AssociatedGradedPresentation.associatedGraded
theorem OAI.StableCoordinate.AssociatedGradedPresentation.associatedGradedEquiv_mk line 104
theorem OAI.StableCoordinate.AssociatedGradedPresentation.associatedGradedEquiv_gX line 111
Source documentation
The presentation equivalence preserves the designated generator symbols.
```
theorem associatedGradedEquiv_gX (i : Fin 5) :
    associatedGradedEquiv k (gX k i) =
      FilteredRees.initial (imagePiece (quotientMap k)) (imagePiece_mono (quotientMap k))
        (monomialWeight (Finsupp.single i 1)) (variableElement (quotientMap k) i) := by
…
```
Mentions: OAI.StableCoordinate.AssociatedGradedPresentation.associatedGradedEquiv, OAI.StableCoordinate.FilteredRees.initial, OAI.StableCoordinate.AssociatedGradedPresentation.quotientMap