Strict levels in one-point filtrations

This file separates the filtration-counting argument from any degree-one leading-coefficient cancellation. For a nested filtration whose successive finrank jumps are bounded by d, it bounds the final finrank by d times the number of strict levels. A matching lower bound therefore forces many strict levels.

For the one-point Riemann filtration, a section that first appears at level n + 1 automatically has exact pole order -(n + 1). Choosing one section at every strict level gives a pairwise-distinct family of exact pole orders, with no hypothesis on the degree of the distinguished place.

noncomputable def BGS.HasseWeil.strictFiltrationLevels {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) (N : ℕ) : Finset ℕ

Levels below N at which a nested filtration grows strictly.

Equations

• BGS.HasseWeil.strictFiltrationLevels R N = {n ∈ Finset.range N | R n < R (n + 1)}

@[simp]

theorem BGS.HasseWeil.strictFiltrationLevels_zero {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) : strictFiltrationLevels R 0 = ∅

theorem BGS.HasseWeil.strictFiltrationLevels_succ_card_of_lt {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) (n : ℕ) (h : R n < R (n + 1)) : (strictFiltrationLevels R (n + 1)).card = (strictFiltrationLevels R n).card + 1

theorem BGS.HasseWeil.strictFiltrationLevels_succ_card_of_not_lt {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) (n : ℕ) (h : ¬R n < R (n + 1)) : (strictFiltrationLevels R (n + 1)).card = (strictFiltrationLevels R n).card

theorem BGS.HasseWeil.finrank_le_initial_add_mul_card_strictFiltrationLevels {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) (d : ℕ) (hnested : ∀ (n : ℕ), R n ≤ R (n + 1)) (hjump : ∀ (n : ℕ), Module.finrank K ↥(R (n + 1)) ≤ Module.finrank K ↥(R n) + d) (N : ℕ) : Module.finrank K ↥(R N) ≤ Module.finrank K ↥(R 0) + d * (strictFiltrationLevels R N).card

If every nontrivial step of a nested filtration has dimension increase at most d, then the total dimension is bounded by d times the number of strict steps, plus the initial dimension.

theorem BGS.HasseWeil.le_card_strictFiltrationLevels_of_initial_add_mul_le_finrank {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) {d m N : ℕ} (hd : 0 < d) (hnested : ∀ (n : ℕ), R n ≤ R (n + 1)) (hjump : ∀ (n : ℕ), Module.finrank K ↥(R (n + 1)) ≤ Module.finrank K ↥(R n) + d) (hlower : Module.finrank K ↥(R 0) + d * m ≤ Module.finrank K ↥(R N)) : m ≤ (strictFiltrationLevels R N).card

A lower dimension bound forces many strict filtration levels.

@[instance_reducible]

noncomputable def BGS.HasseWeil.strictLevelsConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the one point strict levels construction.

Equations

• BGS.HasseWeil.strictLevelsConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.strictLevelsConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.onePointRiemannSpace_order_eq_neg_succ_of_mem_not_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) {x : L} (hxSucc : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (n + 1)) (hxNot : x ∉ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) : x ≠ 0 ∧ (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) P = -↑(n + 1)

A section appearing for the first time at level n + 1 has exact pole order -(n + 1) at the distinguished place. No residue-degree hypothesis is needed.

theorem BGS.HasseWeil.exists_onePointRiemannSpace_sections_indexed_by_strictLevels (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (N : ℕ) : ∃ (f : ↥(strictFiltrationLevels (fun (m : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) N) → L), (∀ (i : ↥(strictFiltrationLevels (fun (m : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) N)), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (↑i + 1) ∧ f i ∉ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ↑i ∧ (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P = -↑(↑i + 1)) ∧ Function.Injective f

Choose one section for every strict level below N. The chosen sections have pairwise distinct exact pole orders, hence are themselves pairwise distinct.