Exists_disc_sections_locality_of_henselSections_of_weierstrassPreparation.lean

theorem evalAt_zero (P : Place K F) : P.evalAt (0 : F) = 0

theorem evalAt_add (P : Place K F) (hP : P.IsRational) {f g : F} (hf : f ∈ P.toValuationSubring)
    (hg : g ∈ P.toValuationSubring) : P.evalAt (f + g) = P.evalAt f + P.evalAt g

theorem evalAt_eq_zero_iff (P : Place K F) (hP : P.IsRational) {f : F} (hf : f ∈
  P.toValuationSubring) :
    P.evalAt f = 0 ↔ (⟨f, hf⟩ : P.toValuationSubring) ∈ maximalIdeal P.toValuationSubring

theorem isUnit_iff_inv_mem (O : Subring F) (g : ↥O) :
    IsUnit g ↔ (g : F) ≠ 0 ∧ (g : F)⁻¹ ∈ O

theorem ord_nonneg_of_mem (P : Place K F) {f : F} (hf : f ∈ P.toValuationSubring) : 0 ≤ P.ord f

theorem ord_pos_iff_evalAt_eq_zero (P : Place K F) (hP : P.IsRational) {f : F} (hf : f ∈
  P.toValuationSubring)
    (hf0 : f ≠ 0) : 0 < P.ord f ↔ P.evalAt f = 0

theorem ord_eq_zero_of_isUnit (P : Place K F) {f : F} (hf : f ∈ P.toValuationSubring)
    (hu : IsUnit (⟨f, hf⟩ : P.toValuationSubring)) : P.ord f = 0

theorem exists_place_of_section
    (S : Subring F) (ι : ↥A →+* ↥S) (hι : ∀ a : ↥A, ((ι a : ↥S) : F) = algebraMap L F (a : L))
    (t : ↥S)
    (hfrac : ∀ f : F, ∃ g h : ↥S, (h : F) ≠ 0 ∧ f * (h : F) = (g : F))
    (B : ValuationSubring F) (hBA : ∀ c : L, algebraMap L F c ∈ B ↔ c ∈ A) (hSB : ∀ f : ↥S, (f : F)
      ∈ B)
    (hunitB : ∀ f : ↥S, f ∉ (maximalIdeal ↥A).map ι → (f : F) ≠ 0 ∧ (f : F)⁻¹ ∈ B)
    (hB : ∀ f : F, f ∈ B → ∃ g h : ↥S, h ∉ (maximalIdeal ↥A).map ι ∧ f * (h : F) = (g : F))
    (h𝔮B : ∀ g : ↥S, g ∈ (maximalIdeal ↥A).map ι → (g : F)⁻¹ ∉ B ∨ (g : F) = 0)
    (htq : t ∉ (maximalIdeal ↥A).map ι)
    (he1 : ∀ f : F, f ≠ 0 → ∃ c : L, c ≠ 0 ∧ algebraMap L F c * f ∈ B ∧ (algebraMap L F c * f)⁻¹ ∈
      B)
    (hprep : ∀ h : ↥S, h ∉ (maximalIdeal ↥A).map ι →
      ∃ (n : ℕ) (u : (↥S)ˣ) (r : Fin n → ↥A), (∀ i, r i ∈ maximalIdeal ↥A) ∧
        h = (u : ↥S) * ∏ i, (t - ι (r i)))
    (χ : ↥S →+* ↥A) (hχι : ∀ a : ↥A, χ (ι a) = a) (hc : χ t ∈ maximalIdeal ↥A)
    (hkerχ : RingHom.ker χ = Ideal.span {t - ι (χ t)}) :
    ∃ P : Place L F, P.IsRational ∧
      (∀ f : F, f ∈ P.toValuationSubring ↔ ∃ g h : ↥S, χ h ≠ 0 ∧ f * (h : F) = (g : F)) ∧
      (∀ f : ↥S, P.evalAt (f : F) = ((χ f : ↥A) : L)) ∧
      (∀ P' : Place L F, P'.IsRational →
        (∀ f : ↥S, (f : F) ∈ P'.toValuationSubring ∧ P'.evalAt (f : F) = ((χ f : ↥A) : L)) → P' =
          P)

theorem
  _root_.AlgebraicCurve.exists_disc_sections_locality_of_henselSections_of_weierstrassPreparation
    {L : Type} [Field L] (A : ValuationSubring L)
    {F : Type} [Field F] [Algebra L F]
    (S : Subring F) (_hS : IsLocalRing ↥S)
    (ι : ↥A →+* ↥S) (hι : ∀ a : ↥A, ((ι a : ↥S) : F) = algebraMap L F (a : L))
    (χ₀ : ↥S →+* ResidueField ↥A)
    (hχ₀C : ∀ a : ↥A, χ₀ (ι a) = IsLocalRing.residue ↥A a)
    (_hmax : ∀ f : ↥S, f ∈ maximalIdeal ↥S ↔ χ₀ f = 0)
    (t : ↥S)
    (hfrac : ∀ f : F, ∃ g h : ↥S, (h : F) ≠ 0 ∧ f * (h : F) = (g : F))
    (B : ValuationSubring F) (hBA : ∀ c : L, algebraMap L F c ∈ B ↔ c ∈ A) (hSB : ∀ f : ↥S, (f : F)
      ∈ B)
    (hunitB : ∀ f : ↥S, f ∉ (maximalIdeal ↥A).map ι → (f : F) ≠ 0 ∧ (f : F)⁻¹ ∈ B)
    (hB : ∀ f : F, f ∈ B → ∃ g h : ↥S, h ∉ (maximalIdeal ↥A).map ι ∧ f * (h : F) = (g : F))
    (_hprime : ((maximalIdeal ↥A).map ι).IsPrime) (htq : t ∉ (maximalIdeal ↥A).map ι)
    (he1 : ∀ f : F, f ≠ 0 → ∃ c : L, c ≠ 0 ∧ algebraMap L F c * f ∈ B ∧ (algebraMap L F c * f)⁻¹ ∈
      B)
    (hhensel : ∀ c : ↥A, IsLocalRing.residue ↥A c = 0 →
      ∃! χ : ↥S →+* ↥A, (∀ a : ↥A, χ (ι a) = a) ∧ (∀ f : ↥S, IsLocalRing.residue ↥A (χ f) = χ₀ f) ∧
        χ t = c)
    (hker : ∀ χ : ↥S →+* ↥A, (∀ a : ↥A, χ (ι a) = a) → (∀ f : ↥S, IsLocalRing.residue ↥A (χ f) = χ₀
      f) →
      RingHom.ker χ = Ideal.span {t - ι (χ t)})
    (hprep : ∀ h : ↥S, h ∉ (maximalIdeal ↥A).map ι →
      ∃ (n : ℕ) (u : (↥S)ˣ) (r : Fin n → ↥A), (∀ i, r i ∈ maximalIdeal ↥A) ∧
        h = (u : ↥S) * ∏ i, (t - ι (r i))) :
    ∃ D : Set (Place L F),
      (∀ P, P ∈ D ↔ (P.IsRational ∧ (∀ f : ↥S, (f : F) ∈ P.toValuationSubring ∧ P.evalAt (f : F) ∈
        A) ∧
        (∀ f : ↥S, A.valuation (P.evalAt (f : F)) < 1 ↔ χ₀ f = 0))) ∧
      (∀ χ : ↥S →+* ↥A, (∀ a : ↥A, χ (ι a) = a) → (∀ f : ↥S, IsLocalRing.residue ↥A (χ f) = χ₀ f) →
        ∃! P, P ∈ D ∧ ∀ f : ↥S, P.evalAt (f : F) = ((χ f : ↥A) : L)) ∧
      (∀ P ∈ D, ∀ f : F, f ∈ P.toValuationSubring ↔
        ∃ g h : ↥S, P.evalAt (h : F) ≠ 0 ∧ f * (h : F) = (g : F)) ∧
      (∀ f : F, f ≠ 0 → (∀ P ∈ D, P.ord f = 0) →
        ∃ (c : L) (u : (↥S)ˣ), c ≠ 0 ∧ algebraMap L F c * f = ((u : ↥S) : F)) ∧
      (∀ f : F, f ∈ B → (∀ P ∈ D, f ∈ P.toValuationSubring) → f ∈ S)