Transcendental_and_finiteDimensional_adjoin_of_valuations.lean

def lSpace (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (m : Multiset (Valuation F ℤᵐ⁰)) : Submodule K F where
  carrier := {g | ∀ v ∈ V, v g ≤ WithZero.exp ((m.count v : ℕ) : ℤ)}
  add_mem' {a b} ha hb := fun v hv => (Valuation.map_add v a b).trans (max_le (ha v hv) (hb v hv))
  zero_mem' := fun v _ => by simp
  smul_mem' c {g} hg := fun v hv => by
    rw [Algebra.smul_def, map_mul]
    by_cases hc : c = 0
    · simp [hc]
    · rw [hK v hv c hc, one_mul]; exact hg v hv

theorem mem_lSpace_iff (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (m : Multiset (Valuation F ℤᵐ⁰)) (g : F) :
    g ∈ lSpace V hK m ↔ ∀ v ∈ V, v g ≤ WithZero.exp ((m.count v : ℕ) : ℤ)

theorem lSpace_zero_le (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hconst : ∀ f : F, (∀ v ∈ V, v f ≤ 1) → f ∈ Set.range (algebraMap K F)) :
    lSpace V hK 0 ≤ Submodule.span K {(1 : F)}

theorem lSpace_cons_le (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hres : ∀ v ∈ V, ∀ f : F, v f = 1 → ∃ c : K, v (f - algebraMap K F c) < 1)
    (m : Multiset (Valuation F ℤᵐ⁰)) (v₀ : Valuation F ℤᵐ⁰) :
    lSpace V hK (v₀ ::ₘ m) = lSpace V hK m ∨
      ∃ g₀ ∈ lSpace V hK (v₀ ::ₘ m), lSpace V hK (v₀ ::ₘ m) = lSpace V hK m ⊔ Submodule.span K {g₀}

theorem finite_and_finrank_lSpace_le (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hres : ∀ v ∈ V, ∀ f : F, v f = 1 → ∃ c : K, v (f - algebraMap K F c) < 1)
    (hconst : ∀ f : F, (∀ v ∈ V, v f ≤ 1) → f ∈ Set.range (algebraMap K F))
    (m : Multiset (Valuation F ℤᵐ⁰)) :
    Module.Finite K (lSpace V hK m) ∧ Module.finrank K (lSpace V hK m) ≤ Multiset.card m + 1

theorem lSpace_mono (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    {m m' : Multiset (Valuation F ℤᵐ⁰)} (h : m ≤ m') : lSpace V hK m ≤ lSpace V hK m'

theorem mul_mem_lSpace (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    {m m' : Multiset (Valuation F ℤᵐ⁰)} {g g' : F} (hg : g ∈ lSpace V hK m) (hg' : g' ∈ lSpace V hK
      m') :
    g * g' ∈ lSpace V hK (m + m')

theorem pow_mem_lSpace (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    {m : Multiset (Valuation F ℤᵐ⁰)} {g : F} (hg : g ∈ lSpace V hK m) (i : ℕ) :
    g ^ i ∈ lSpace V hK (i • m)

theorem exists_mem_lSpace (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hfin : ∀ f : F, f ≠ 0 → {v ∈ V | 1 < v f}.Finite) (g : F) :
    ∃ m : Multiset (Valuation F ℤᵐ⁰), g ∈ lSpace V hK m

theorem linearIndependent_pow_of_transcendental {f : F} (htr : Transcendental K f) (k : ℕ) :
    LinearIndependent K (fun i : Fin k => f ^ (i : ℕ)) := by
  rw [Fintype.linearIndependent_iff]
  intro g hg i
  have hp : Polynomial.aeval f (∑ j : Fin k, Polynomial.monomial (j : ℕ) (g j)) = 0 := by
    rw [map_sum]
    simpa [Polynomial.aeval_monomial, Algebra.smul_def] using hg
  have hp0 := (transcendental_iff.1 htr) _ hp
  have hcoeff := congrArg (fun p : Polynomial K => p.coeff (i : ℕ)) hp0
  simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_monomial, Polynomial.coeff_zero] at hcoeff
  rw [Finset.sum_eq_single i (fun j _ hji => ite_eq_right (fun h => hji (Fin.ext h))) (fun h =>
    absurd (Finset.mem_univ i) h),
    ite_eq_left rfl] at hcoeff
  exact hcoeff

theorem v_le_one_of_isIntegral (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    {v : Valuation F ℤᵐ⁰} (hv : v ∈ V) {f : F} (hf : IsIntegral K f) : v f ≤ 1

theorem transcendental_and_finiteDimensional (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hres : ∀ v ∈ V, ∀ f : F, v f = 1 → ∃ c : K, v (f - algebraMap K F c) < 1)
    (hfin : ∀ f : F, f ≠ 0 → {v ∈ V | 1 < v f}.Finite)
    (hconst : ∀ f : F, (∀ v ∈ V, v f ≤ 1) → f ∈ Set.range (algebraMap K F))
    (f : F) (hf : f ∉ Set.range (algebraMap K F)) :
    Transcendental K f ∧ FiniteDimensional ↥(IntermediateField.adjoin K ({f} : Set F)) F

theorem _root_.AlgebraicCurve.transcendental_and_finiteDimensional_adjoin_of_valuations
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (V : Set (Valuation F ℤᵐ⁰))
    (hK : ∀ v ∈ V, ∀ c : K, c ≠ 0 → v (algebraMap K F c) = 1)
    (hres : ∀ v ∈ V, ∀ f : F, v f = 1 → ∃ c : K, v (f - algebraMap K F c) < 1)
    (hfin : ∀ f : F, f ≠ 0 → {v ∈ V | 1 < v f}.Finite)
    (hconst : ∀ f : F, (∀ v ∈ V, v f ≤ 1) → f ∈ Set.range (algebraMap K F))
    (f : F) (hf : f ∉ Set.range (algebraMap K F)) :
    Transcendental K f ∧ FiniteDimensional ↥(IntermediateField.adjoin K ({f} : Set F)) F