IntegerFiltrationDegree.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Integer filtration degree and initial forms

Section 3 uses an exhaustive separated increasing filtration indexed by all integers, including negative integers. These generic lemmas prove that every nonzero element has a least layer and that its image modulo the preceding layer is nonzero. They do not assume any coordinate obstruction or associated-graded presentation.

def OAI.StableCoordinate.IntegerFiltration.degree line 25
Source documentation
The integer degree is the infimum of the layers containing an element. The lemmas below show that for a nonzero element this infimum is attained.
```
noncomputable def degree {A : Type*} (F : ℤ → Set A) (x : A) : ℤ :=
…
```
theorem OAI.StableCoordinate.IntegerFiltration.degree_eq_of_least line 29
Source documentation
A least layer computes the filtration degree.
```
theorem degree_eq_of_least {A : Type*} (F : ℤ → Set A) {x : A} {d : ℤ}
    (hd : x ∈ F d) (hleast : ∀ e : ℤ, x ∈ F e → d ≤ e) :
    degree F x = d := by
…
```
Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.exists_least_index line 40

Source documentation

An exhaustive separated increasing integer filtration gives every nonzero object a genuine least degree, not merely an infimum or a natural-number degree.

theorem exists_least_index (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) :
    ∃ d : ℤ, x ∈ F d ∧ ∀ e : ℤ, x ∈ F e → d ≤ e := by
…

theorem OAI.StableCoordinate.IntegerFiltration.exists_initial_index line 57

Source documentation

In particular the initial form of a nonzero element is represented in one layer but not the preceding layer.

theorem exists_initial_index (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) :
    ∃ d : ℤ, x ∈ F d ∧ x ∉ F (d - 1) := by
…

theorem OAI.StableCoordinate.IntegerFiltration.initial_index_unique line 69

Source documentation

Such an initial index is unique.

theorem initial_index_unique (F : ℤ → Set A) (hmono : Monotone F)
    {x : A} {d e : ℤ} (hd : x ∈ F d) (hd' : x ∉ F (d - 1))
    (he : x ∈ F e) (he' : x ∉ F (e - 1)) : d = e := by
…

theorem OAI.StableCoordinate.IntegerFiltration.degree_spec line 81

Source documentation

The degree of a nonzero element is an attained least index.

theorem degree_spec (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) :
    x ∈ F (degree F x) ∧ ∀ e : ℤ, x ∈ F e → degree F x ≤ e := by
…

Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.mem_iff_degree_le line 91

Source documentation

Membership in a filtration layer is equivalent to the integer degree bound.

theorem mem_iff_degree_le (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) (e : ℤ) :
    x ∈ F e ↔ degree F x ≤ e := by
…

Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.not_mem_degree_sub_one line 100

Source documentation

The preceding layer misses every nonzero element.

theorem not_mem_degree_sub_one (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) : x ∉ F (degree F x - 1) := by
…

Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.degree_eq_iff_initial line 110

Source documentation

The degree is characterized by membership in a layer and failure of membership in the immediately preceding layer.

theorem degree_eq_iff_initial (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) (d : ℤ) :
    degree F x = d ↔ x ∈ F d ∧ x ∉ F (d - 1) := by
…

Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.degree_pos_iff line 125

Source documentation

Being outside the zeroth layer is exactly positivity of filtration degree.

theorem degree_pos_iff (F : ℤ → Set A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d)
    (hseparated : ∀ x : A, (∀ d : ℤ, x ∈ F d) → x = 0)
    {x : A} (hx : x ≠ 0) :
    0 < degree F x ↔ x ∉ F 0 := by
…

Mentions: OAI.StableCoordinate.IntegerFiltration.degree

theorem OAI.StableCoordinate.IntegerFiltration.initial_form_ne_zero line 141
Source documentation
A representative in the first possible layer is nonzero in the quotient by its preceding layer. This is the nonvanishing needed for an initial form.
```
theorem initial_form_ne_zero (F : ℤ → Submodule K A) {d : ℤ} {x : A}
    (hx : x ∈ F d) (hxprev : x ∉ F (d - 1)) :
    (Submodule.Quotient.mk ⟨x, hx⟩ :
      (F d) ⧸ (F (d - 1)).comap (F d).subtype) ≠ 0 := by
…
```
theorem OAI.StableCoordinate.IntegerFiltration.separated_of_iInf_eq_bot line 151
Source documentation
Separation phrased as a lattice intersection implies elementwise separation.
```
theorem separated_of_iInf_eq_bot (F : ℤ → Submodule K A) (hF : ⨅ d, F d = ⊥)
    (x : A) (hx : ∀ d : ℤ, x ∈ F d) : x = 0 := by
…
```

theorem OAI.StableCoordinate.IntegerFiltration.exists_nonzero_initial_form line 159

Source documentation

The source's exhaustive separated filtration has a nonzero initial form for every nonzero element, as a genuine quotient-module element.

theorem exists_nonzero_initial_form (F : ℤ → Submodule K A) (hmono : Monotone F)
    (hexhaustive : ∀ x : A, ∃ d : ℤ, x ∈ F d) (hF : ⨅ d, F d = ⊥)
    {x : A} (hx : x ≠ 0) :
    ∃ (d : ℤ) (hd : x ∈ F d),
      (Submodule.Quotient.mk ⟨x, hd⟩ :
        (F d) ⧸ (F (d - 1)).comap (F d).subtype) ≠ 0 := by
…