GradedRelation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The exact leading relation for the negative-degree presentation

These lemmas check the elementary input to Section 3 of the source: Hstar has integer weighted degree one for weights (-1,0,0,1,1), is not divisible by p, and none of the five generator classes vanishes in its principal quotient. The source polynomial H has degree-one component exactly Hstar. No associated-graded identification is assumed.

theorem OAI.StableCoordinate.Obstruction.p_not_dvd_Hstar line 23
Source documentation
Reduction at p=s=u=F=0, J=1 shows p ∤ Hstar.
```
theorem p_not_dvd_Hstar : ¬ (X 0 : P k 5) ∣ Hstar k := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.P, OAI.StableCoordinate.Obstruction.Hstar
theorem OAI.StableCoordinate.Obstruction.Hstar_not_dvd_X line 29
Source documentation
Each coordinate has a point on Hstar=0 where it is one.
```
theorem Hstar_not_dvd_X (i : Fin 5) : ¬ Hstar k ∣ (X i : P k 5) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.Hstar, OAI.StableCoordinate.Obstruction.P
theorem OAI.StableCoordinate.Obstruction.gX_ne_zero line 48
Source documentation
The five named generators in the graded presentation remain nonzero.
```
theorem gX_ne_zero (i : Fin 5) : gX k i ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.gX

theorem OAI.StableCoordinate.Obstruction.weighted_sub line 60

Source documentation

Homogeneity is preserved by subtraction over a ring.

theorem weighted_sub {σ : Type*} {w : σ → ℤ} {f g : MvPolynomial σ k} {n : ℤ}
    (hf : f.IsWeightedHomogeneous w n) (hg : g.IsWeightedHomogeneous w n) :
    (f - g).IsWeightedHomogeneous w n :=
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.Obstruction.xP_homogeneous line 66
Source documentation
The determinant invariant has presentation weight zero.
```
theorem xP_homogeneous : (xP k).IsWeightedHomogeneous presentationWeight 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.xP, OAI.StableCoordinate.Obstruction.presentationWeight
theorem OAI.StableCoordinate.Obstruction.Hstar_homogeneous line 80
Source documentation
The highest relation is homogeneous of presentation weight one.
```
theorem Hstar_homogeneous : (Hstar k).IsWeightedHomogeneous presentationWeight 1 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.Hstar, OAI.StableCoordinate.Obstruction.presentationWeight
theorem OAI.StableCoordinate.Obstruction.Hstar_degree line 98
Source documentation
The weight-one relation is nonzero, hence its weighted degree is one.
```
theorem Hstar_degree [Nontrivial k] :
    weightedTotalDegree' presentationWeight (Hstar k) = (1 : WithBot ℤ) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.presentationWeight, OAI.StableCoordinate.Obstruction.Hstar
theorem OAI.StableCoordinate.Obstruction.H_degree_one_component line 105
Source documentation
The degree-one component of the original relation is exactly Hstar.
```
theorem H_degree_one_component :
    weightedHomogeneousComponent presentationWeight 1 (H k) = Hstar k := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.presentationWeight, OAI.StableCoordinate.Obstruction.H, OAI.StableCoordinate.Obstruction.Hstar
theorem OAI.StableCoordinate.Obstruction.idealG_homogeneous line 124
Source documentation
The principal ideal of the highest relation is homogeneous for the source's actual integer grading, including its negative weight.
```
theorem idealG_homogeneous :
    (idealG k).IsHomogeneous (weightedHomogeneousSubmodule k presentationWeight) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.idealG, OAI.StableCoordinate.Obstruction.presentationWeight