DeterminantWeights.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Fiber weights on the actual determinant quotient

The Laurent coaction is induced by the exact weights (1,1,-1,-1,0) on a,d,b,c,u. We establish the final weight contradiction in the actual quotient ring, not just in an abstract polynomial algebra: an element in the image of k[a,d,u] with negative fiber weight is zero.

theorem OAI.StableCoordinate.DeterminantWeights.relation_fiber_homogeneous line 28
Source documentation
The determinant relation is homogeneous of fiber weight zero.
```
theorem relation_fiber_homogeneous :
    (relation k).IsWeightedHomogeneous Obstruction.fiberWeight 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.fiberWeight
def OAI.StableCoordinate.DeterminantWeights.fiberCoaction line 43
Source documentation
The genuine fiber-weight coaction on k[a,d,b,c,u]/(ac-bd-1).
```
def fiberCoaction : C k →ₐ[k] LaurentPolynomial (C k) :=
…
```
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_generator line 48
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_a line 53
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_d line 56
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_b line 59
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_c line 62
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_u line 65
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_ab line 70
Source documentation
The first quadric coordinate x=ab is fixed by fiber scaling.
```
@[simp] theorem fiberCoaction_ab :
    fiberCoaction k (a k * b k) = AddMonoidAlgebra.single 0 (a k * b k) := by
…
```
Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_dc line 76
Source documentation
The second quadric coordinate y=dc is fixed by fiber scaling.
```
@[simp] theorem fiberCoaction_dc :
    fiberCoaction k (d k * c k) = AddMonoidAlgebra.single 0 (d k * c k) := by
…
```
Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_db line 82
Source documentation
The third quadric coordinate z=db is fixed by fiber scaling.
```
@[simp] theorem fiberCoaction_db :
    fiberCoaction k (d k * b k) = AddMonoidAlgebra.single 0 (d k * b k) := by
…
```
Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_of_mem_quadric_adjoin line 88
Source documentation
Every polynomial in the four base quadric coordinates is fiber-invariant.
```
theorem fiberCoaction_of_mem_quadric_adjoin {q : C k}
    (hq : q ∈ Algebra.adjoin k (Set.range ![a k * b k, d k * c k, d k * b k, u k])) :
    fiberCoaction k q = AddMonoidAlgebra.single 0 q := by
…
```
Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_mk_of_homogeneous line 102
Source documentation
Homogeneous images in the quotient satisfy the corresponding Laurent weight identity.
```
theorem fiberCoaction_mk_of_homogeneous {p : P k} {n : ℤ}
    (hp : p.IsWeightedHomogeneous Obstruction.fiberWeight n) :
    fiberCoaction k (mk k p) = AddMonoidAlgebra.single n (mk k p) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.fiberWeight, OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantWeights.fiberCoaction_mem_nonnegative_of_mem_baseRange line 109
Source documentation
Membership in the polynomial subalgebra generated by a,d,u gives only nonnegative fiber powers.
```
theorem fiberCoaction_mem_nonnegative_of_mem_baseRange {q : C k}
    (hq : q ∈ (baseMap (k := k)).range) :
…
```
theorem OAI.StableCoordinate.DeterminantWeights.eq_zero_of_mem_baseRange_of_negative_weight line 127
Source documentation
The final rigidity obstruction in the actual determinant quotient, stated directly using its fiber coaction.
```
theorem eq_zero_of_mem_baseRange_of_negative_weight {q : C k}
    (hq : q ∈ (baseMap (k := k)).range) {n : ℤ} (hn : n < 0)
…
```
theorem OAI.StableCoordinate.DeterminantWeights.eq_zero_of_mem_baseRange_of_homogeneous_representative line 136
Source documentation
The same obstruction for the image definition of a homogeneous quotient piece. This is the interface consumed by a quotient grading.
```
theorem eq_zero_of_mem_baseRange_of_homogeneous_representative {q : C k}
    (hq : q ∈ (baseMap (k := k)).range) {n : ℤ} (hn : n < 0)
…
```
theorem OAI.StableCoordinate.DeterminantWeights.no_nonzero_baseRange_weight_neg_two line 146
Source documentation
In particular, the nonzero coefficient of fiber weight -2 required by the source's final step cannot lie in k[a,d,u].
```
theorem no_nonzero_baseRange_weight_neg_two {q : C k} (hq0 : q ≠ 0)
    (hq : q ∈ (baseMap (k := k)).range) :
…
```
theorem OAI.StableCoordinate.DeterminantWeights.eq_zero_of_mem_baseRange_of_mem_homogeneous_piece line 154
Source documentation
Image-submodule form of the final obstruction; this matches the standard grading on a quotient by a homogeneous relation.
```
theorem eq_zero_of_mem_baseRange_of_mem_homogeneous_piece {q : C k}
    (hq : q ∈ (baseMap (k := k)).range) {n : ℤ} (hn : n < 0)
…
```

theorem OAI.StableCoordinate.DeterminantWeights.coefficient_weight_neg_two line 163

Source documentation

Both terms of the source coefficient c*D(b)-b*D(c) have fiber weight -2 whenever D preserves the fiber weights of b and c.

theorem coefficient_weight_neg_two {r s : C k}
    (hr : fiberCoaction k r = AddMonoidAlgebra.single (-1) r)
    (hs : fiberCoaction k s = AddMonoidAlgebra.single (-1) s) :
    fiberCoaction k (c k * r - b k * s) =
      AddMonoidAlgebra.single (-2) (c k * r - b k * s) := by
…

Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction

theorem OAI.StableCoordinate.DeterminantWeights.coefficient_eq_zero_of_mem_baseRange line 175
Source documentation
Final coefficient vanishing, ready to combine with the determinant coefficient's nonvanishing for a nonzero derivation.
```
theorem coefficient_eq_zero_of_mem_baseRange {r s : C k}
    (hr : fiberCoaction k r = AddMonoidAlgebra.single (-1) r)
    (hs : fiberCoaction k s = AddMonoidAlgebra.single (-1) s)
    (hq : c k * r - b k * s ∈ (baseMap (k := k)).range) :
…
```
Mentions: OAI.StableCoordinate.DeterminantWeights.fiberCoaction