DeterminantGradings.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

The two actual integer gradings on the determinant hypersurface

The degrees are exactly the two rows in source equation rig:gradings. Both gradings are constructed on C = k[a,d,b,c,u]/(ac-bd-1) by quotienting weighted polynomial gradings. In particular, negative auxiliary and fiber degrees are retained.

abbrev OAI.StableCoordinate.Obstruction.polynomialPiece line 25
Source documentation
The weighted pieces on the five-variable polynomial presentation.
```
abbrev polynomialPiece (w : Fin 5 → ℤ) : ℤ → Submodule k (P k 5) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.P
instance OAI.StableCoordinate.Obstruction.polynomialGrading line 28
theorem OAI.StableCoordinate.Obstruction.determinantRelation_homogeneous line 33
Source documentation
The determinant relation is homogeneous whenever the products ac and bd both have degree zero.
```
theorem determinantRelation_homogeneous (w : Fin 5 → ℤ)
    (hac : w 0 + w 3 = 0) (hbd : w 2 + w 1 = 0) :
    determinantRelation k ∈ polynomialPiece k w 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.determinantRelation, OAI.StableCoordinate.Obstruction.polynomialPiece
theorem OAI.StableCoordinate.Obstruction.idealC_homogeneous line 50
Source documentation
Thus the whole defining ideal is homogeneous, not just its displayed generator.
```
theorem idealC_homogeneous (w : Fin 5 → ℤ)
    (hac : w 0 + w 3 = 0) (hbd : w 2 + w 1 = 0) :
    (idealC k).IsHomogeneous (polynomialPiece k w) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.idealC, OAI.StableCoordinate.Obstruction.polynomialPiece
abbrev OAI.StableCoordinate.Obstruction.determinantPiece line 59
Source documentation
The induced weighted pieces in the determinant quotient.
```
abbrev determinantPiece (w : Fin 5 → ℤ) : ℤ → Submodule k (C k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.C
def OAI.StableCoordinate.Obstruction.determinantGrading line 64
Source documentation
The quotient grading for any weight vector satisfying the two determinant constraints.
```
def determinantGrading (w : Fin 5 → ℤ)
    (hac : w 0 + w 3 = 0) (hbd : w 2 + w 1 = 0) :
    GradedAlgebra (determinantPiece k w) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.determinantPiece
abbrev OAI.StableCoordinate.Obstruction.auxiliaryPiece line 71
Source documentation
Actual auxiliary homogeneous pieces: deg(a,d,b,c,u) = (0,1,-1,0,1).
```
abbrev auxiliaryPiece : ℤ → Submodule k (C k) := determinantPiece k auxiliaryWeight
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.determinantPiece, OAI.StableCoordinate.Obstruction.auxiliaryWeight
abbrev OAI.StableCoordinate.Obstruction.fiberPiece line 73
Source documentation
Actual fiber-weight pieces: wt(a,d,b,c,u) = (1,1,-1,-1,0).
```
abbrev fiberPiece : ℤ → Submodule k (C k) := determinantPiece k fiberWeight
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.determinantPiece, OAI.StableCoordinate.Obstruction.fiberWeight
instance OAI.StableCoordinate.Obstruction.auxiliaryGrading line 75
instance OAI.StableCoordinate.Obstruction.fiberGrading line 78
theorem OAI.StableCoordinate.Obstruction.cX_mem_auxiliaryPiece line 82
Source documentation
Every generator has its assigned auxiliary degree.
```
theorem cX_mem_auxiliaryPiece (i : Fin 5) : cX k i ∈ auxiliaryPiece k (auxiliaryWeight i) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX, OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.auxiliaryWeight
theorem OAI.StableCoordinate.Obstruction.cX_mem_fiberPiece line 87
Source documentation
Every generator has its assigned fiber weight.
```
theorem cX_mem_fiberPiece (i : Fin 5) : cX k i ∈ fiberPiece k (fiberWeight i) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.cX, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.fiberWeight
def OAI.StableCoordinate.Obstruction.vLow line 92
Source documentation
The degree-minus-one part of the obstruction polynomial.
```
def vLow : C k := cX k 0 ^ 3 * cX k 2
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.cX
def OAI.StableCoordinate.Obstruction.vHigh line 94
Source documentation
The degree-two part of the obstruction polynomial.
```
def vHigh : C k := cX k 0 ^ 2 * cX k 4 ^ 2 - cX k 1 ^ 2
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.cX
theorem OAI.StableCoordinate.Obstruction.v_eq_low_add_high line 96
theorem OAI.StableCoordinate.Obstruction.vLow_mem_auxiliaryPiece line 100
Source documentation
The lower term of v has auxiliary degree minus one.
```
theorem vLow_mem_auxiliaryPiece : vLow k ∈ auxiliaryPiece k (-1) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.vLow, OAI.StableCoordinate.Obstruction.auxiliaryPiece
theorem OAI.StableCoordinate.Obstruction.vHigh_mem_auxiliaryPiece line 106
Source documentation
The difference of squares in v has auxiliary degree two.
```
theorem vHigh_mem_auxiliaryPiece : vHigh k ∈ auxiliaryPiece k 2 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.vHigh, OAI.StableCoordinate.Obstruction.auxiliaryPiece
theorem OAI.StableCoordinate.Obstruction.vLow_mem_fiberPiece line 116
Source documentation
Both auxiliary parts have fiber weight two.
```
theorem vLow_mem_fiberPiece : vLow k ∈ fiberPiece k 2 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.vLow, OAI.StableCoordinate.Obstruction.fiberPiece
theorem OAI.StableCoordinate.Obstruction.vHigh_mem_fiberPiece line 121
theorem OAI.StableCoordinate.Obstruction.v_mem_fiberPiece line 131
Source documentation
The full obstruction polynomial is homogeneous of fiber weight two.
```
theorem v_mem_fiberPiece : v k ∈ fiberPiece k 2 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.v, OAI.StableCoordinate.Obstruction.fiberPiece
theorem OAI.StableCoordinate.Obstruction.auxiliary_proj_v_two line 137
Source documentation
Its auxiliary degree-two projection is exactly the source's difference of squares.
```
theorem auxiliary_proj_v_two :
    GradedAlgebra.proj (auxiliaryPiece k) 2 (v k) = vHigh k := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.v, OAI.StableCoordinate.Obstruction.vHigh
theorem OAI.StableCoordinate.Obstruction.auxiliary_proj_v_eq_zero line 147
Source documentation
No other auxiliary degrees occur beyond the two explicitly listed parts.
```
theorem auxiliary_proj_v_eq_zero (n : ℤ) (hnlow : (-1 : ℤ) ≠ n) (hnhigh : (2 : ℤ) ≠ n) :
    GradedAlgebra.proj (auxiliaryPiece k) n (v k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.v
theorem OAI.StableCoordinate.Obstruction.auxiliary_proj_mk line 158
Source documentation
Auxiliary projections commute with passage to the quotient.
```
theorem auxiliary_proj_mk (n : ℤ) (p : P k 5) :
    GradedAlgebra.proj (auxiliaryPiece k) n (Ideal.Quotient.mk (idealC k) p) =
      Ideal.Quotient.mk (idealC k) (weightedHomogeneousComponent auxiliaryWeight n p) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.P, OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.idealC, OAI.StableCoordinate.Obstruction.auxiliaryWeight
theorem OAI.StableCoordinate.Obstruction.fiber_proj_mk line 166
Source documentation
Fiber projections commute with passage to the quotient.
```
theorem fiber_proj_mk (n : ℤ) (p : P k 5) :
    GradedAlgebra.proj (fiberPiece k) n (Ideal.Quotient.mk (idealC k) p) =
      Ideal.Quotient.mk (idealC k) (weightedHomogeneousComponent fiberWeight n p) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.P, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.idealC, OAI.StableCoordinate.Obstruction.fiberWeight

theorem OAI.StableCoordinate.Obstruction.weightedHomogeneousComponent_commute line 173

Source documentation

Coefficientwise weighted projections for arbitrary weight vectors commute.

theorem weightedHomogeneousComponent_commute (w w' : Fin 5 → ℤ)
    (m n : ℤ) (p : P k 5) :
    weightedHomogeneousComponent w m (weightedHomogeneousComponent w' n p) =
      weightedHomogeneousComponent w' n (weightedHomogeneousComponent w m p) := by
…

Mentions: OAI.StableCoordinate.Obstruction.P

theorem OAI.StableCoordinate.Obstruction.auxiliary_fiber_proj_commute line 184
Source documentation
The fiber and auxiliary gradings are compatible on the actual quotient: their homogeneous projection maps commute.
```
theorem auxiliary_fiber_proj_commute (m n : ℤ) (z : C k) :
    GradedAlgebra.proj (auxiliaryPiece k) m (GradedAlgebra.proj (fiberPiece k) n z) =
      GradedAlgebra.proj (fiberPiece k) n (GradedAlgebra.proj (auxiliaryPiece k) m z) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.auxiliaryPiece, OAI.StableCoordinate.Obstruction.fiberPiece