ModificationEmbedding.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The degeneration embeds into the affine-modification Laurent model

This file uses the canonical source map from LaurentPresentation and identifies its image with the extended Rees algebra. Injectivity is supplied by the separate localization/domain argument; it is not assumed here.

abbrev OAI.StableCoordinate.ModificationEmbedding.LP.C line 22
abbrev OAI.StableCoordinate.ModificationEmbedding.LP.T line 23
abbrev OAI.StableCoordinate.ModificationEmbedding.values line 31
Source documentation
Alias for the canonical source-ordered Laurent coordinate values.
```
abbrev values := LaurentPresentation.laurentValues k
```
Mentions: OAI.StableCoordinate.LaurentPresentation.laurentValues
def OAI.StableCoordinate.ModificationEmbedding.polynomialMap line 34
Source documentation
Polynomial evaluation before taking the degeneration quotient.
```
def polynomialMap : P k 5 →ₐ[k] LaurentPolynomial (B k) :=
…
```
theorem OAI.StableCoordinate.ModificationEmbedding.polynomialMap_X line 38
abbrev OAI.StableCoordinate.ModificationEmbedding.toLaurent line 43
Source documentation
Alias for the canonical map from G to B[τ,τ⁻¹].
```
abbrev toLaurent := LaurentPresentation.toLaurentBase k
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.toLaurentBase
theorem OAI.StableCoordinate.ModificationEmbedding.toLaurent_mk line 46
theorem OAI.StableCoordinate.ModificationEmbedding.toLaurent_gX line 51
theorem OAI.StableCoordinate.ModificationEmbedding.values_mem line 55
theorem OAI.StableCoordinate.ModificationEmbedding.polynomialMap_mem line 66
theorem OAI.StableCoordinate.ModificationEmbedding.toLaurent_mem line 80
Source documentation
Every element of the actual source degeneration lands in the affine modification.
```
theorem toLaurent_mem (a : G k) :
    toLaurent k a ∈ ModificationPieces.modification (I k) := by
…
```
Mentions: OAI.StableCoordinate.ModificationEmbedding.toLaurent, OAI.StableCoordinate.ModificationPieces.modification
theorem OAI.StableCoordinate.ModificationEmbedding.values_homogeneous line 86
Source documentation
The source generator weights are exactly opposite their Laurent exponents.
```
theorem values_homogeneous (i : Fin 5) :
    ModificationPieces.Homogeneous (presentationWeight i) (values k i) := by
…
```
Mentions: OAI.StableCoordinate.ModificationPieces.Homogeneous, OAI.StableCoordinate.ModificationEmbedding.values
theorem OAI.StableCoordinate.ModificationEmbedding.polynomialMap_homogeneous line 101
Source documentation
An actual weighted homogeneous representative maps to the corresponding single Laurent degree; no grading of a quotient is postulated.
```
theorem polynomialMap_homogeneous {p : P k 5} {d : ℤ}
    (hp : p.IsWeightedHomogeneous presentationWeight d) :
    ModificationPieces.Homogeneous d (polynomialMap k p) :=
…
```
Mentions: OAI.StableCoordinate.ModificationPieces.Homogeneous, OAI.StableCoordinate.ModificationEmbedding.polynomialMap
theorem OAI.StableCoordinate.ModificationEmbedding.polynomialMap_positive_piece line 109
Source documentation
Positive-degree homogeneous representatives have numerators in the appropriate power of the exact source ideal.
```
theorem polynomialMap_positive_piece {p : P k 5} {ℓ : ℕ}
    (hp : p.IsWeightedHomogeneous presentationWeight (ℓ : ℤ)) :
    ∃ h ∈ I k ^ ℓ, polynomialMap k p = LP.C h * LP.T (-(ℓ : ℤ)) :=
…
```
Mentions: OAI.StableCoordinate.ModificationEmbedding.polynomialMap, OAI.StableCoordinate.ModificationEmbedding.LP.C, OAI.StableCoordinate.ModificationEmbedding.LP.T
theorem OAI.StableCoordinate.ModificationEmbedding.polynomialMap_positive_nonzero_numerator line 117
Source documentation
The extraction needed for the noncoordinate obstruction, stated directly for nonzero Laurent images of homogeneous representatives.
```
theorem polynomialMap_positive_nonzero_numerator {p : P k 5} {ℓ : ℕ}
    (hℓ : 0 < ℓ) (hp : p.IsWeightedHomogeneous presentationWeight (ℓ : ℤ))
    (hne : polynomialMap k p ≠ 0) :
    ∃ h ∈ I k, h ≠ 0 ∧ polynomialMap k p = LP.C h * LP.T (-(ℓ : ℤ)) :=
…
```
Mentions: OAI.StableCoordinate.ModificationEmbedding.polynomialMap, OAI.StableCoordinate.ModificationEmbedding.LP.C, OAI.StableCoordinate.ModificationEmbedding.LP.T
def OAI.StableCoordinate.ModificationEmbedding.imageSubalgebra line 126
Source documentation
The canonical map's image is a B-subalgebra, since the base map is a section on constant Laurent polynomials.
```
def imageSubalgebra : Subalgebra (B k) (LaurentPolynomial (B k)) where
…
```
theorem OAI.StableCoordinate.ModificationEmbedding.image_eq_modification line 140
Source documentation
Exact affine-modification image, with the actual source's two-generator center.
```
theorem image_eq_modification :
    imageSubalgebra k = ModificationPieces.modification (I k) := by
…
```
Mentions: OAI.StableCoordinate.ModificationEmbedding.imageSubalgebra, OAI.StableCoordinate.ModificationPieces.modification
theorem OAI.StableCoordinate.ModificationEmbedding.range_toLaurent line 152