Place_exists_uniformizing_separating_form.lean

theorem mwALGN_ord_algebraMap (v : Place k F) {c : k} (hc : c ≠ 0) :
    v.ord (algebraMap k F c) = 0

def mwALGN_ordGe (v : Place k F) (m : ℤ) : Submodule k F where
  carrier := {x | x = 0 ∨ m ≤ v.ord x}
  zero_mem' := Or.inl rfl
  add_mem' := by
    intro x y hx hy
    simp only [Set.mem_ofPred_eq] at hx hy ⊢
    by_cases hx0 : x = 0
    · subst hx0
      simpa using hy
    by_cases hy0 : y = 0
    · subst hy0
      simpa using hx
    by_cases hxy : x + y = 0
    · exact Or.inl hxy
    right
    have hx' : m ≤ v.ord x := hx.resolve_left hx0
    have hy' : m ≤ v.ord y := hy.resolve_left hy0
    have h := v.min_ord_le_ord_add hx0 hy0 hxy
    omega
  smul_mem' := by
    intro c x hx
    simp only [Set.mem_ofPred_eq] at hx ⊢
    by_cases hc : c = 0
    · subst hc
      simp
    by_cases hx0 : x = 0
    · subst hx0
      simp
    right
    rw [Algebra.smul_def, v.ord_mul ((_root_.map_ne_zero _).mpr hc) hx0,
      mwALGN_ord_algebraMap v hc, zero_add]
    exact hx.resolve_left hx0

theorem mwALGN_mem_ordGe_iff (v : Place k F) (m : ℤ) (x : F) :
    x ∈ mwALGN_ordGe v m ↔ x = 0 ∨ m ≤ v.ord x

theorem mwALGN_mem_of_forall_sum_pow_smul_mem (W : Submodule k F) {m : ℕ}
    (z : Fin (m + 1) → F) (θ : Fin (m + 1) → k) (hθ : Function.Injective θ)
    (h : ∀ l, (∑ i : Fin (m + 1), θ l ^ (i : ℕ) • z i) ∈ W) (i : Fin (m + 1)) : z i ∈ W

theorem _root_.AlgebraicCurve.Place.exists_uniformizing_separating_form
    {k F : Type*} [Field k] [Field F] [Algebra k F]
    (v : Place k F) {j : F} {n : ℕ} (β : Fin n → F)
    (cv : k) (hcv : 0 < v.ord (j - algebraMap k F cv))
    (βv : Fin n → k)
    (hβv : ∀ i, β i = algebraMap k F (βv i) ∨ 0 < v.ord (β i - algebraMap k F (βv i)))
    (hU1 : v.ord (j - algebraMap k F cv) = 1 ∨ ∃ i, v.ord (β i - algebraMap k F (βv i)) = 1)
    {r : ℕ} (pt : Fin r → Place k F) (cpt : Fin r → k) (βpt : Fin r → Fin n → k)
    (hS1 : ∀ t, pt t ≠ v → cpt t ≠ cv ∨ βpt t ≠ βv)
    {a : ℕ} (θ : Fin a → k) (hθ : Function.Injective θ) (ha : n * (r + 1) < a) :
    ∃ s : Fin a,
      v.ord ((j + ∑ i : Fin n, algebraMap k F (θ s ^ (i.val + 1)) * β i)
          - algebraMap k F (cv + ∑ i : Fin n, θ s ^ (i.val + 1) * βv i)) = 1 ∧
      ∀ t, pt t ≠ v →
        cpt t + ∑ i : Fin n, θ s ^ (i.val + 1) * βpt t i
          ≠ cv + ∑ i : Fin n, θ s ^ (i.val + 1) * βv i