FiltrationSeparation.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Separation for the integer filtration

The variables are ordered (p,s,u,F,J). The integer weight is -exp(p) + exp(F) + exp(J). This file proves the negative-weight power-divisibility estimate, and separates every image filtration in a Noetherian domain whenever the image of p is a nonunit.

def OAI.StableCoordinate.Filtration.monomialWeight line 25
Source documentation
The source weight (-1,0,0,1,1) on exponent vectors.
```
def monomialWeight : (Fin 5 →₀ ℕ) →+ ℤ where
…
```
theorem OAI.StableCoordinate.Filtration.monomialWeight_apply line 30
theorem OAI.StableCoordinate.Filtration.exponent_zero_ge_of_weight_le_neg line 34
Source documentation
A monomial of weight at most -r has at least r factors of p.
```
theorem exponent_zero_ge_of_weight_le_neg {e : Fin 5 →₀ ℕ} {r : ℕ}
    (h : monomialWeight e ≤ -(r : ℤ)) : r ≤ e 0 := by
…
```
Mentions: OAI.StableCoordinate.Filtration.monomialWeight
def OAI.StableCoordinate.Filtration.piece line 42
Source documentation
The span of the monomials of integer source weight at most d.
```
def piece (d : ℤ) : Submodule K (MvPolynomial (Fin 5) K) :=
…
```
theorem OAI.StableCoordinate.Filtration.piece_mono line 46
Source documentation
The source filtration is increasing.
```
theorem piece_mono : Monotone (piece K) := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.pow_X_zero_dvd_monomial line 53
Source documentation
Every negative-weight monomial is divisible by the corresponding power of p.
```
theorem pow_X_zero_dvd_monomial {e : Fin 5 →₀ ℕ} {r : ℕ}
    (h : monomialWeight e ≤ -(r : ℤ)) (c : K) :
    (X (0 : Fin 5) : MvPolynomial (Fin 5) K) ^ r ∣ monomial e c := by
…
```
Mentions: OAI.StableCoordinate.Filtration.monomialWeight
theorem OAI.StableCoordinate.Filtration.piece_neg_le_span_pow line 61
Source documentation
The negative source piece is contained in the principal ideal (p^r).
```
theorem piece_neg_le_span_pow (r : ℕ) :
    piece K (-(r : ℤ)) ≤
      (Ideal.span {((X (0 : Fin 5) : MvPolynomial (Fin 5) K) ^ r)}).restrictScalars K := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.monomial_mem_piece line 69
Source documentation
A monomial belongs to its assigned filtration piece.
```
theorem monomial_mem_piece {e : Fin 5 →₀ ℕ} {d : ℤ}
    (h : monomialWeight e ≤ d) (c : K) : monomial e c ∈ piece K d := by
…
```
Mentions: OAI.StableCoordinate.Filtration.monomialWeight, OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.mem_piece_iff line 76
Source documentation
Membership can equivalently be tested on the support.
```
theorem mem_piece_iff {q : MvPolynomial (Fin 5) K} {d : ℤ} :
    q ∈ piece K d ↔ ∀ e ∈ q.support, monomialWeight e ≤ d := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece, OAI.StableCoordinate.Filtration.monomialWeight
theorem OAI.StableCoordinate.Filtration.exists_mem_piece line 103
Source documentation
Exhaustiveness of the filtration on the five-variable polynomial ring.
```
theorem exists_mem_piece (q : MvPolynomial (Fin 5) K) :
    ∃ d : ℤ, q ∈ piece K d := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.one_mem_piece line 113
Source documentation
The constant one has weight zero.
```
theorem one_mem_piece : (1 : MvPolynomial (Fin 5) K) ∈ piece K 0 := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.mul_mem_piece line 118
Source documentation
Multiplication adds filtration indices, including negative indices.
```
theorem mul_mem_piece {q r : MvPolynomial (Fin 5) K} {d e : ℤ}
    (hq : q ∈ piece K d) (hr : r ∈ piece K e) : q * r ∈ piece K (d + e) := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
instance OAI.StableCoordinate.Filtration.(instance at line 143) line 143
instance OAI.StableCoordinate.Filtration.(instance at line 147) line 147
def OAI.StableCoordinate.Filtration.imagePiece line 155
Source documentation
The image filtration under a polynomial presentation. In particular this is the quotient filtration when φ is an ideal quotient homomorphism.
```
def imagePiece (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (d : ℤ) : Submodule K A :=
…
```
theorem OAI.StableCoordinate.Filtration.imagePiece_mono line 159
Source documentation
The image filtration is increasing.
```
theorem imagePiece_mono (φ : MvPolynomial (Fin 5) K →ₐ[K] A) :
    Monotone (imagePiece φ) := by
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece
theorem OAI.StableCoordinate.Filtration.exists_mem_imagePiece line 165
Source documentation
A surjective polynomial presentation gives an exhaustive image filtration.
```
theorem exists_mem_imagePiece (φ : MvPolynomial (Fin 5) K →ₐ[K] A)
    (hφ : Function.Surjective φ) (a : A) : ∃ d : ℤ, a ∈ imagePiece φ d := by
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece
theorem OAI.StableCoordinate.Filtration.X_mem_piece line 172
Source documentation
A source generator belongs to the piece specified by its weight.
```
theorem X_mem_piece (i : Fin 5) :
    (X i : MvPolynomial (Fin 5) K) ∈ piece K (monomialWeight (Finsupp.single i 1)) := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece, OAI.StableCoordinate.Filtration.monomialWeight
theorem OAI.StableCoordinate.Filtration.X_zero_mem_piece_neg_one line 178
Source documentation
The negative degree of the distinguished variable is available before separation or identification of the associated graded ring.
```
theorem X_zero_mem_piece_neg_one :
    (X (0 : Fin 5) : MvPolynomial (Fin 5) K) ∈ piece K (-1) := by
…
```
Mentions: OAI.StableCoordinate.Filtration.piece
theorem OAI.StableCoordinate.Filtration.image_X_zero_mem_neg_one line 183
Source documentation
The image of the distinguished variable belongs to degree -1.
```
theorem image_X_zero_mem_neg_one (φ : MvPolynomial (Fin 5) K →ₐ[K] A) :
    φ (X 0) ∈ imagePiece φ (-1) :=
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece

theorem OAI.StableCoordinate.Filtration.mul_mem_imagePiece line 188

Source documentation

The image filtration is multiplicative.

theorem mul_mem_imagePiece (φ : MvPolynomial (Fin 5) K →ₐ[K] A)
    {a b : A} {d e : ℤ} (ha : a ∈ imagePiece φ d) (hb : b ∈ imagePiece φ e) :
    a * b ∈ imagePiece φ (d + e) := by
…

Mentions: OAI.StableCoordinate.Filtration.imagePiece

instance OAI.StableCoordinate.Filtration.(instance at line 195) line 195
instance OAI.StableCoordinate.Filtration.(instance at line 199) line 199
theorem OAI.StableCoordinate.Filtration.pow_dvd_of_mem_imagePiece_neg line 204
Source documentation
Divisibility survives the polynomial presentation.
```
theorem pow_dvd_of_mem_imagePiece_neg (φ : MvPolynomial (Fin 5) K →ₐ[K] A)
    {r : ℕ} {a : A} (ha : a ∈ imagePiece φ (-(r : ℤ))) :
    φ (X 0) ^ r ∣ a := by
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece
theorem OAI.StableCoordinate.Filtration.eq_zero_of_mem_all_imagePieces line 215
Source documentation
Krull intersection separates the image filtration. No claim that every image has this property is made: the noetherian-domain and nonunit hypotheses are explicit and must be supplied by a polynomial-presentation theorem.
```
theorem eq_zero_of_mem_all_imagePieces [IsNoetherianRing A] [IsDomain A]
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hp : ¬ IsUnit (φ (X 0)))
    {a : A} (ha : ∀ d : ℤ, a ∈ imagePiece φ d) : a = 0 := by
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece
theorem OAI.StableCoordinate.Filtration.iInf_imagePiece_eq_bot line 231
Source documentation
Equivalent submodule-valued statement of separation.
```
theorem iInf_imagePiece_eq_bot [IsNoetherianRing A] [IsDomain A]
    (φ : MvPolynomial (Fin 5) K →ₐ[K] A) (hp : ¬ IsUnit (φ (X 0))) :
    (⨅ d : ℤ, imagePiece φ d) = ⊥ := by
…
```
Mentions: OAI.StableCoordinate.Filtration.imagePiece