PrincipalInitialRelation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact initial relation of the source hypersurface

For the five independent variables p,s,u,F,J, with integer weights (-1,0,0,1,1), this file proves that the initial ideal of (H) is exactly (Hstar). It also gives the actual homogeneous kernel criterion in terms of the quotient rings A and G, without assuming an associated-graded isomorphism.

theorem OAI.StableCoordinate.PrincipalInitialRelation.H_bounded line 24
Source documentation
The original relation has no monomials above weight one.
```
theorem H_bounded : Bounded presentationWeight (H k) 1 := by
…
```
theorem OAI.StableCoordinate.PrincipalInitialRelation.H_isTopDegree line 32
Source documentation
The original relation has actual highest integer weight one.
```
theorem H_isTopDegree [Nontrivial k] : IsTopDegree presentationWeight (H k) 1 := by
…
```

theorem OAI.StableCoordinate.PrincipalInitialRelation.component_mul_H line 40

Source documentation

The leading weight of a product by the exact relation is obtained by multiplying the leading component by the exact polynomial Hstar.

theorem component_mul_H (q : P k 5) (d : ℤ)
    (hq : Bounded presentationWeight q d) :
    weightedHomogeneousComponent presentationWeight (d + 1) (q * H k) =
      weightedHomogeneousComponent presentationWeight d q * Hstar k := by
…

theorem OAI.StableCoordinate.PrincipalInitialRelation.initialIdeal_idealA line 49
Source documentation
The principal initial-ideal identity for the exact source relation.
```
theorem initialIdeal_idealA :
    initialIdeal presentationWeight (idealA k) = idealG k := by
…
```

theorem OAI.StableCoordinate.PrincipalInitialRelation.homogeneous_lower_iff line 56

Source documentation

A homogeneous polynomial has a lower-weight representative modulo H if and only if it belongs to (Hstar).

theorem homogeneous_lower_iff (p : P k 5) (d : ℤ)
    (hp : p.IsWeightedHomogeneous presentationWeight d) :
    (∃ r : P k 5, Bounded presentationWeight r (d - 1) ∧ p - r ∈ idealA k) ↔
      p ∈ idealG k := by
…

theorem OAI.StableCoordinate.PrincipalInitialRelation.quotient_homogeneous_lower_iff line 66

Source documentation

The same exact kernel criterion, stated directly in the two quotient rings. This is the degreewise algebraic interface used to identify G with gr A.

theorem quotient_homogeneous_lower_iff (p : P k 5) (d : ℤ)
    (hp : p.IsWeightedHomogeneous presentationWeight d) :
    (∃ r : P k 5, Bounded presentationWeight r (d - 1) ∧
      Ideal.Quotient.mk (idealA k) p = Ideal.Quotient.mk (idealA k) r) ↔
      Ideal.Quotient.mk (idealG k) p = 0 := by
…