SourceFiltrationProper.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

A proper zeroth filtration layer in the actual source algebra

The two points (p,s,u,F,J) = (0,0,0,0,0) and (0,0,0,1,0) lie on H = 0. They agree on every polynomial of source weight at most zero, but not on F. Thus the zeroth layer of the actual quotient filtration is proper, without any associated-graded presentation assumption.

def OAI.StableCoordinate.SourceFiltration.presentation line 26
Source documentation
The actual quotient presentation homomorphism.
```
def presentation : P k 5 →ₐ[k] A k := Ideal.Quotient.mkₐ k (idealA k)
```
def OAI.StableCoordinate.SourceFiltration.testPoint line 29
Source documentation
A line of points on H = 0, varying only the coordinate F.
```
def testPoint (t : k) : Fin 5 → k := ![0, 0, 0, t, 0]
```
theorem OAI.StableCoordinate.SourceFiltration.aeval_H_testPoint line 31
def OAI.StableCoordinate.SourceFiltration.testEval line 35
Source documentation
Evaluation on the actual hypersurface algebra along the test line.
```
def testEval (t : k) : A k →ₐ[k] k :=
…
```
theorem OAI.StableCoordinate.SourceFiltration.testEval_presentation line 43
theorem OAI.StableCoordinate.SourceFiltration.testEval_aX line 46
theorem OAI.StableCoordinate.SourceFiltration.testPoint_monomial_eq line 52
Source documentation
Weight-zero bound removes dependence on F after setting p=0.
```
theorem testPoint_monomial_eq (t : k) (e : Fin 5 →₀ ℕ)
    (he : monomialWeight e ≤ 0) (c : k) :
    aeval (testPoint k t) (monomial e c) =
      aeval (testPoint k 0) (monomial e c) := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.testPoint
theorem OAI.StableCoordinate.SourceFiltration.testPoint_eq_of_mem_piece_zero line 69
Source documentation
All evaluations along the test line agree on the zeroth polynomial layer.
```
theorem testPoint_eq_of_mem_piece_zero (t : k) {q : P k 5} (hq : q ∈ piece k 0) :
    aeval (testPoint k t) q = aeval (testPoint k 0) q := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.testPoint
theorem OAI.StableCoordinate.SourceFiltration.testEval_eq_of_mem_zero_layer line 80
Source documentation
The same constancy holds on the zeroth layer of the quotient filtration.
```
theorem testEval_eq_of_mem_zero_layer (t : k) {a : A k}
    (ha : a ∈ imagePiece (presentation k) 0) : testEval k t a = testEval k 0 a := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.presentation, OAI.StableCoordinate.SourceFiltration.testEval
theorem OAI.StableCoordinate.SourceFiltration.F_not_mem_zero_layer line 86
Source documentation
The class F is genuinely not in the zeroth layer of the source algebra.
```
theorem F_not_mem_zero_layer [Nontrivial k] :
    aX k 3 ∉ imagePiece (presentation k) 0 := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.presentation
theorem OAI.StableCoordinate.SourceFiltration.F_mem_one_layer line 93
Source documentation
The class F belongs to the first layer of the source filtration.
```
theorem F_mem_one_layer : aX k 3 ∈ imagePiece (presentation k) 1 := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.presentation
theorem OAI.StableCoordinate.SourceFiltration.degree_F line 98
Source documentation
Its least integer filtration index is exactly one.
```
theorem degree_F [Nontrivial k] :
    IntegerFiltration.degree (fun d => (imagePiece (presentation k) d : Set (A k)))
      (aX k 3) = 1 := by
…
```
Mentions: OAI.StableCoordinate.IntegerFiltration.degree, OAI.StableCoordinate.SourceFiltration.presentation
def OAI.StableCoordinate.SourceFiltration.zeroLayerSubalgebra line 108
Source documentation
The zeroth layer, with its actual subalgebra structure.
```
def zeroLayerSubalgebra : Subalgebra k (A k) where
…
```
theorem OAI.StableCoordinate.SourceFiltration.mem_zeroLayerSubalgebra line 123
theorem OAI.StableCoordinate.SourceFiltration.p_mem_zeroLayerSubalgebra line 127
Source documentation
The distinguished element p is in the zeroth-layer subalgebra.
```
theorem p_mem_zeroLayerSubalgebra : aX k 0 ∈ zeroLayerSubalgebra k := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.zeroLayerSubalgebra
theorem OAI.StableCoordinate.SourceFiltration.zeroLayerSubalgebra_ne_top line 134
Source documentation
The proper-subalgebra premise in the coordinate-derivation argument is proved for the actual source filtration, not added as an external assumption.
```
theorem zeroLayerSubalgebra_ne_top [Nontrivial k] : zeroLayerSubalgebra k ≠ ⊤ := by
…
```
Mentions: OAI.StableCoordinate.SourceFiltration.zeroLayerSubalgebra