DeterminantGradedObstruction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Final weight obstruction in the constructed determinant grading

This module connects the actual quotient grading to the Laurent proof of negative-weight vanishing. The two independently defined quotient-ring interfaces are definitionally equal; no extra grading or injectivity hypothesis is imposed here.

theorem OAI.StableCoordinate.DeterminantGradedObstruction.mem_fiberPiece_iff_fiberCoaction line 25
Source documentation
A fiber-weight identity for the actual Laurent coaction is equivalent to membership in the constructed graded piece. This also gives the converse needed after differentiating an equivariant additive action.
```
theorem mem_fiberPiece_iff_fiberCoaction {q : C k} (n : ℤ) :
    q ∈ Obstruction.fiberPiece k n ↔
      DeterminantWeights.fiberCoaction k q = AddMonoidAlgebra.single n q :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.DeterminantWeights.fiberCoaction
theorem OAI.StableCoordinate.DeterminantGradedObstruction.eq_zero_of_mem_baseRange_of_mem_fiberPiece line 33
Source documentation
An element of the actual fiber-weight piece of negative degree cannot lie nontrivially in the polynomial subalgebra k[a,d,u].
```
theorem eq_zero_of_mem_baseRange_of_mem_fiberPiece {q : C k}
    (hq : q ∈ (baseMap (k := k)).range) {n : ℤ} (hn : n < 0)
…
```
theorem OAI.StableCoordinate.DeterminantGradedObstruction.coefficient_mem_fiberPiece_neg_two line 40
Source documentation
A source-style weight-preserving derivation has coefficient c*D(b)-b*D(c) in fiber degree -2.
```
theorem coefficient_mem_fiberPiece_neg_two {r s : C k}
    (hr : r ∈ Obstruction.fiberPiece k (-1))
    (hs : s ∈ Obstruction.fiberPiece k (-1)) :
    c k * r - b k * s ∈ Obstruction.fiberPiece k (-2) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.fiberPiece
theorem OAI.StableCoordinate.DeterminantGradedObstruction.coefficient_eq_zero_of_mem_baseRange line 58
Source documentation
The precise contradiction endpoint for the rigidity coefficient, without introducing a homogeneous-polynomial representative premise.
```
theorem coefficient_eq_zero_of_mem_baseRange
    {r s : C k} (hr : r ∈ Obstruction.fiberPiece k (-1))
    (hs : s ∈ Obstruction.fiberPiece k (-1))
    (hq : c k * r - b k * s ∈ (baseMap (k := k)).range) :
…
```
Mentions: OAI.StableCoordinate.Obstruction.fiberPiece