GradedDegeneration.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

The actual integer grading of the degeneration ring

The quotient G = k[p,s,u,F,J]/(Hstar) carries the grading with weights (-1,0,0,1,1). This file constructs that grading, rather than assuming it, and records the degree-zero quadric coordinates used in the Laurent picture. It does not identify G with the associated graded ring of A.

def OAI.StableCoordinate.Obstruction.gPiece line 27
Source documentation
The degree-n submodule in the actual principal quotient G.
```
def gPiece (n : ℤ) : Submodule k (G k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.G
instance OAI.StableCoordinate.Obstruction.gGradedAlgebra line 31
Source documentation
Quotient homogeneity gives a genuine integer-graded algebra structure.
```
instance gGradedAlgebra : GradedAlgebra (gPiece k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.mk_mem_gPiece line 36
Source documentation
Images of weighted-homogeneous polynomials lie in the specified quotient piece.
```
theorem mk_mem_gPiece {n : ℤ} {q : P k 5}
    (hq : q.IsWeightedHomogeneous presentationWeight n) :
    Ideal.Quotient.mk (idealG k) q ∈ gPiece k n :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.P, OAI.StableCoordinate.Obstruction.presentationWeight, OAI.StableCoordinate.Obstruction.idealG, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.gX_mem_piece line 42
Source documentation
Each presentation generator retains its assigned (possibly negative) weight.
```
theorem gX_mem_piece (i : Fin 5) : gX k i ∈ gPiece k (presentationWeight i) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.gX, OAI.StableCoordinate.Obstruction.gPiece, OAI.StableCoordinate.Obstruction.presentationWeight
def OAI.StableCoordinate.Obstruction.xG line 46
Source documentation
The weight-zero invariant x in the degeneration ring.
```
def xG : G k := gX k 1 ^ 2 - gX k 2 ^ 2 + gX k 0 * gX k 3
```
Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.Obstruction.gX
def OAI.StableCoordinate.Obstruction.yG line 49
Source documentation
The weight-zero invariant y in the degeneration ring.
```
def yG : G k := gX k 1 + xG k * (xG k + gX k 2 ^ 2)
```
Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.Obstruction.gX, OAI.StableCoordinate.Obstruction.xG
def OAI.StableCoordinate.Obstruction.zG line 52
Source documentation
The weight-zero invariant z in the degeneration ring.
```
def zG : G k := gX k 1 * xG k + gX k 0 * gX k 4
```
Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.Obstruction.gX, OAI.StableCoordinate.Obstruction.xG
theorem OAI.StableCoordinate.Obstruction.mk_xP line 54
theorem OAI.StableCoordinate.Obstruction.xG_mem_piece line 58
Source documentation
The distinguished determinant invariant is homogeneous of degree zero.
```
theorem xG_mem_piece : xG k ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.xG, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.mul_mem_gPiece_zero line 62
Source documentation
Products of two degree-zero elements again have degree zero.
```
theorem mul_mem_gPiece_zero {a b : G k} (ha : a ∈ gPiece k 0) (hb : b ∈ gPiece k 0) :
    a * b ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.yG_mem_piece line 67
Source documentation
The second quadric coordinate has degree zero.
```
theorem yG_mem_piece : yG k ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.yG, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.zG_mem_piece line 76
Source documentation
The third quadric coordinate has degree zero.
```
theorem zG_mem_piece : zG k ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.zG, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.uG_mem_piece line 84
Source documentation
The variable u on the quadric is the original weight-zero generator.
```
theorem uG_mem_piece : gX k 2 ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.gX, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.g_relation line 88
Source documentation
The defining equation of G in its named generators.
```
theorem g_relation :
    xG k ^ 2 * gX k 3 - (1 + 2 * gX k 1 * xG k) * gX k 4 -
      gX k 0 * gX k 4 ^ 2 = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.xG, OAI.StableCoordinate.Obstruction.gX
theorem OAI.StableCoordinate.Obstruction.g_quadric_relation line 94
Source documentation
The quadric equation follows from the actual defining relation of G.
```
theorem g_quadric_relation : xG k * yG k - zG k * (zG k + 1) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.xG, OAI.StableCoordinate.Obstruction.yG, OAI.StableCoordinate.Obstruction.zG
def OAI.StableCoordinate.Obstruction.baseToDegenerationPre line 105
Source documentation
Polynomial map implementing the quadric coordinates in G.
```
def baseToDegenerationPre : P k 4 →ₐ[k] G k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.P, OAI.StableCoordinate.Obstruction.G
theorem OAI.StableCoordinate.Obstruction.baseToDegenerationPre_relation line 109
Source documentation
The quadric relation vanishes under the polynomial substitution.
```
theorem baseToDegenerationPre_relation :
    baseToDegenerationPre k (quadricRelation k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.baseToDegenerationPre, OAI.StableCoordinate.Obstruction.quadricRelation
def OAI.StableCoordinate.Obstruction.baseToDegeneration line 114
Source documentation
The canonical algebra homomorphism from the quadric ring into G.
```
def baseToDegeneration : B k →ₐ[k] G k :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.G
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_mk line 121
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_bX line 125
theorem OAI.StableCoordinate.Obstruction.baseToDegenerationPre_X_mem_piece line 130
Source documentation
All four polynomial substitution values lie in degree zero.
```
theorem baseToDegenerationPre_X_mem_piece (i : Fin 4) :
    baseToDegenerationPre k (X i) ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.baseToDegenerationPre, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_mem_piece line 140
Source documentation
The complete quadric coordinate ring lands in weight zero.
```
theorem baseToDegeneration_mem_piece (q : B k) :
    baseToDegeneration k q ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.baseToDegeneration, OAI.StableCoordinate.Obstruction.gPiece
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_sB line 158
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_f0 line 165
theorem OAI.StableCoordinate.Obstruction.baseToDegeneration_g0 line 171