Place_forall_localSubring_iff_forall_localization.lean

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

theorem ord_eq_zero_of_evalAt_ne_zero (v : Place L F)
    {f : F} (hf : f ∈ v.toValuationSubring) (hne : v.evalAt f ≠ 0) : v.ord f = 0

theorem inv_mem_and_evalAt_inv (P : Place L F) (hP : P.IsRational) {f : F} (hf : f ∈
  P.toValuationSubring)
    (hne : P.evalAt f ≠ 0) : f⁻¹ ∈ P.toValuationSubring ∧ P.evalAt f⁻¹ = (P.evalAt f)⁻¹

theorem Ws33.Core.core_one
    {L F : Type*} [Field L] [Field F] [Algebra L F] (A : ValuationSubring L)
    (T : Subring F) (𝔭 : Ideal ↥T) (Lx : Subring F)
    (hLx : ∀ f : F, f ∈ Lx ↔ ∃ b c : ↥T, c ∉ 𝔭 ∧ f * (c : F) = (b : F))
    (P : Place L F) (hP : P.IsRational) :
    (∀ t : ↥T, (t : F) ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt (t : F) ∈ A, (IsUnit (⟨P.evalAt (t : F), h⟩ : ↥A) ↔ t ∉ 𝔭)) ↔
    (∀ f : F, f ∈ Lx → f ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt f ∈ A, (IsUnit (⟨P.evalAt f, h⟩ : ↥A) ↔ ∃ g ∈ Lx, f * g = 1))

theorem evalAt_add_of_mem (v : Place L F) (hv : v.IsRational) {f g : F}
    (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    v.evalAt (f + g) = v.evalAt f + v.evalAt g

theorem evalAt_neg_of_mem (v : Place L F) (hv : v.IsRational) {f : F} (hf : f ∈
  v.toValuationSubring) :
    v.evalAt (-f) = -v.evalAt f

theorem evalAt_sub_of_mem (v : Place L F) (hv : v.IsRational) {f g : F}
    (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    v.evalAt (f - g) = v.evalAt f - v.evalAt g

theorem Ws33.Core.core_two
    {L F : Type*} [Field L] [Field F] [Algebra L F] (A : ValuationSubring L)
    (N₀ : Subring F) [IsLocalRing ↥N₀] (C' : Subring L) (hC'A : ∀ c : L, c ∈ C' → c ∈ A)
    (hconst : ∀ g : ↥N₀, ∃ (o : ↥C') (h : algebraMap L F (o : L) ∈ N₀), ¬ IsUnit (g - ⟨_, h⟩))
    (T : Subring F) (hT : T = Subring.closure ((N₀ : Set F) ∪ Set.range (fun a : ↥A => algebraMap L
      F (a : L))))
    (𝔭 : Ideal ↥T)
    (h𝔭 : 𝔭 = Ideal.span ({t : ↥T | ∃ f : ↥N₀, ¬ IsUnit f ∧ (t : F) = (f : F)} ∪
      {t : ↥T | ∃ a : ↥A, a ∈ maximalIdeal ↥A ∧ (t : F) = algebraMap L F (a : L)}))
    (P : Place L F) (hP : P.IsRational) :
    ((∀ f : F, f ∈ N₀ → f ∈ P.toValuationSubring) ∧
      (∀ f : ↥N₀, ¬ IsUnit f → ∃ h : P.evalAt (f : F) ∈ A, (⟨P.evalAt (f : F), h⟩ : ↥A) ∈
        maximalIdeal ↥A)) ↔
    (∀ t : ↥T, (t : F) ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt (t : F) ∈ A, (IsUnit (⟨P.evalAt (t : F), h⟩ : ↥A) ↔ t ∉ 𝔭)) := by
  classical
  subst hT
  subst h𝔭
  set s : Set F := (N₀ : Set F) ∪ Set.range (fun a : ↥A => algebraMap L F (a : L)) with hs
  have hNT : ∀ f : F, f ∈ N₀ → f ∈ Subring.closure s := fun f hf => Subring.subset_closure (Or.inl
    hf)
  have hAT : ∀ a : ↥A, algebraMap L F (a : L) ∈ Subring.closure s := fun a =>
    Subring.subset_closure (Or.inr ⟨a, rfl⟩)
  set cT : ↥A → ↥(Subring.closure s) := fun a => ⟨algebraMap L F (a : L), hAT a⟩ with hcT
  set G : Set ↥(Subring.closure s) := {t | ∃ f : ↥N₀, ¬ IsUnit f ∧ (t : F) = (f : F)} ∪
      {t | ∃ a : ↥A, a ∈ maximalIdeal ↥A ∧ (t : F) = algebraMap L F (a : L)} with hG
  have hG1 : ∀ (f : ↥N₀), ¬ IsUnit f → (⟨(f : F), hNT f f.2⟩ : ↥(Subring.closure s)) ∈ Ideal.span G
    :=
    fun f hf => Ideal.subset_span (Or.inl ⟨f, hf, rfl⟩)
  have hG2 : ∀ a : ↥A, a ∈ maximalIdeal ↥A → cT a ∈ Ideal.span G :=
    fun a ha => Ideal.subset_span (Or.inr ⟨a, ha, rfl⟩)
  have hdec : ∀ t : ↥(Subring.closure s), ∃ a : ↥A, t - cT a ∈ Ideal.span G := by
    rintro ⟨x, hx⟩
    induction hx using Subring.closure_induction with
    | mem y hy =>
      rcases hy with hy | ⟨a, rfl⟩
      · obtain ⟨o, ho, hnu⟩ := hconst ⟨y, hy⟩
        refine ⟨⟨(o : L), hC'A _ o.2⟩, ?_⟩
        have : (⟨y, Subring.subset_closure (Or.inl hy)⟩ : ↥(Subring.closure s)) - cT ⟨(o : L), hC'A
          _ o.2⟩ =
            ⟨((⟨y, hy⟩ : ↥N₀) - ⟨algebraMap L F (o : L), ho⟩ : ↥N₀), hNT _ (Subring.sub_mem _ hy
              ho)⟩ := Subtype.ext rfl
        rw [this]
        exact hG1 _ hnu
      · exact ⟨a, by rw [show (⟨algebraMap L F (a : L), Subring.subset_closure (Or.inr ⟨a, rfl⟩)⟩ :
            ↥(Subring.closure s)) = cT a from rfl, sub_self]; exact (Ideal.span G).zero_mem⟩
    | zero =>
      refine ⟨0, ?_⟩
      have : (⟨0, Subring.zero_mem _⟩ : ↥(Subring.closure s)) - cT 0 = 0 := Subtype.ext
        (by simp [hcT])
      rw [this]; exact (Ideal.span G).zero_mem
    | one =>
      refine ⟨1, ?_⟩
      have : (⟨1, Subring.one_mem _⟩ : ↥(Subring.closure s)) - cT 1 = 0 := Subtype.ext
        (by simp [hcT])
      rw [this]; exact (Ideal.span G).zero_mem
    | add y z hy hz ihy ihz =>
      obtain ⟨a, ha⟩ := ihy
      obtain ⟨b, hb⟩ := ihz
      refine ⟨a + b, ?_⟩
      have : (⟨y + z, Subring.add_mem _ hy hz⟩ : ↥(Subring.closure s)) - cT (a + b) =
          (⟨y, hy⟩ - cT a) + (⟨z, hz⟩ - cT b) := Subtype.ext (by simp [hcT]; ring)
      rw [this]; exact (Ideal.span G).add_mem ha hb
    | neg y hy ih =>
      obtain ⟨a, ha⟩ := ih
      refine ⟨-a, ?_⟩
      have : (⟨-y, Subring.neg_mem _ hy⟩ : ↥(Subring.closure s)) - cT (-a) = -((⟨y, hy⟩ :
        ↥(Subring.closure s)) - cT a) :=
        Subtype.ext (by simp [hcT]; ring)
      rw [this]; exact (Ideal.span G).neg_mem_iff.mpr ha
    | mul y z hy hz ihy ihz =>
      obtain ⟨a, ha⟩ := ihy
      obtain ⟨b, hb⟩ := ihz
      refine ⟨a * b, ?_⟩
      have : (⟨y * z, Subring.mul_mem _ hy hz⟩ : ↥(Subring.closure s)) - cT (a * b) =
          (⟨y, hy⟩ - cT a) * ⟨z, hz⟩ + cT a * (⟨z, hz⟩ - cT b) := Subtype.ext (by simp [hcT]; ring)
      rw [this]
      exact (Ideal.span G).add_mem ((Ideal.span G).mul_mem_right _ ha) ((Ideal.span G).mul_mem_left
        _ hb)
  constructor
  · rintro ⟨hN, hNu⟩
    have hle : Subring.closure s ≤ P.toValuationSubring.toSubring := by
      rw [Subring.closure_le]
      rintro y (hy | ⟨a, rfl⟩)
      · exact hN y hy
      · exact P.algebraMap_mem' _
    have hTP : ∀ t : ↥(Subring.closure s), (t : F) ∈ P.toValuationSubring := fun t => hle t.2
    have hTA : ∀ t : ↥(Subring.closure s), P.evalAt (t : F) ∈ A := by
      rintro ⟨x, hx⟩
      change P.evalAt x ∈ A
      induction hx using Subring.closure_induction with
      | mem y hy =>
        rcases hy with hy | ⟨a, rfl⟩
        · obtain ⟨o, ho, hnu⟩ := hconst ⟨y, hy⟩
          obtain ⟨hmem, -⟩ := hNu _ hnu
          have hmem' : P.evalAt (y - algebraMap L F (o : L)) ∈ A := hmem
          have e : y = (y - algebraMap L F (o : L)) + algebraMap L F (o : L) := by ring
          rw [e, evalAt_add_of_mem P hP (hN _ (Subring.sub_mem _ hy ho)) (P.algebraMap_mem' _),
            Place.evalAt_algebraMap_eq]
          exact add_mem hmem' (hC'A _ o.2)
        · rw [Place.evalAt_algebraMap_eq]; exact a.2
      | zero => rw [evalAt_zero]; exact zero_mem _
      | one => rw [Place.evalAt_one]; exact one_mem _
      | add y z hy hz ihy ihz =>
        rw [evalAt_add_of_mem P hP (hle hy) (hle hz)]; exact add_mem ihy ihz
      | neg y hy ih => rw [evalAt_neg_of_mem P hP (hle hy)]; exact neg_mem ih
      | mul y z hy hz ihy ihz =>
        rw [P.evalAt_mul_of_mem hP (hle hy) (hle hz)]; exact mul_mem ihy ihz
    have h𝔭A : ∀ p : ↥(Subring.closure s), p ∈ Ideal.span G →
        (⟨P.evalAt (p : F), hTA p⟩ : ↥A) ∈ maximalIdeal ↥A := by
      intro p hp
      induction hp using Submodule.span_induction with
      | mem y hy =>
        rcases hy with ⟨f, hf, hyf⟩ | ⟨a, ha, hya⟩
        · obtain ⟨h, hm⟩ := hNu f hf
          have : (⟨P.evalAt (y : F), hTA y⟩ : ↥A) = ⟨P.evalAt (f : F), h⟩ := Subtype.ext (by
            change P.evalAt (y : F) = P.evalAt (f : F); rw [hyf])
          rw [this]; exact hm
        · have : (⟨P.evalAt (y : F), hTA y⟩ : ↥A) = a := Subtype.ext (by
            change P.evalAt (y : F) = (a : L)
            rw [hya, Place.evalAt_algebraMap_eq])
          rw [this]; exact ha
      | zero =>
        have : (⟨P.evalAt ((0 : ↥(Subring.closure s)) : F), hTA 0⟩ : ↥A) = 0 := Subtype.ext
          (evalAt_zero P)
        rw [this]; exact (maximalIdeal ↥A).zero_mem
      | add y z _ _ ihy ihz =>
        have : (⟨P.evalAt ((y + z : ↥(Subring.closure s)) : F), hTA (y + z)⟩ : ↥A) =
            ⟨P.evalAt (y : F), hTA y⟩ + ⟨P.evalAt (z : F), hTA z⟩ := Subtype.ext (evalAt_add_of_mem
              P hP (hTP y) (hTP z))
        rw [this]; exact (maximalIdeal ↥A).add_mem ihy ihz
      | smul r y _ ih =>
        have : (⟨P.evalAt ((r • y : ↥(Subring.closure s)) : F), hTA (r • y)⟩ : ↥A) =
            ⟨P.evalAt (r : F), hTA r⟩ * ⟨P.evalAt (y : F), hTA y⟩ := Subtype.ext
              (P.evalAt_mul_of_mem hP (hTP r) (hTP y))
        rw [this]; exact (maximalIdeal ↥A).mul_mem_left _ ih
    intro t
    refine ⟨hTP t, hTA t, ?_⟩
    obtain ⟨a, ha⟩ := hdec t
    have hval : (⟨P.evalAt (t : F), hTA t⟩ : ↥A) = a + ⟨P.evalAt ((t - cT a : ↥(Subring.closure s))
      : F), hTA _⟩ := by
      apply Subtype.ext
      change P.evalAt (t : F) = (a : L) + P.evalAt ((t - cT a : ↥(Subring.closure s)) : F)
      rw [show ((t - cT a : ↥(Subring.closure s)) : F) = (t : F) - algebraMap L F (a : L) from rfl,
        evalAt_sub_of_mem P hP (hTP t) (P.algebraMap_mem' _), Place.evalAt_algebraMap_eq]
      ring
    have hpm := h𝔭A _ ha
    constructor
    · intro hu ht
      exact (IsLocalRing.mem_maximalIdeal _).mp (h𝔭A t ht) hu
    · intro ht
      have ha' : a ∉ maximalIdeal ↥A := fun ham => ht (by
        have := (Ideal.span G).add_mem ha (hG2 a ham)
        rwa [sub_add_cancel] at this)
      rw [hval]
      by_contra hnu
      have : a + ⟨P.evalAt ((t - cT a : ↥(Subring.closure s)) : F), hTA _⟩ ∈ maximalIdeal ↥A :=
        (IsLocalRing.mem_maximalIdeal _).mpr hnu
      exact ha' ((Submodule.add_mem_iff_left _ hpm).mp this)
  · intro hTu
    refine ⟨fun f hf => (hTu ⟨f, hNT f hf⟩).1, fun f hf => ?_⟩
    obtain ⟨-, h, hu⟩ := hTu ⟨(f : F), hNT f f.2⟩
    exact ⟨h, (IsLocalRing.mem_maximalIdeal _).mpr fun hunit => (hu.mp hunit) (hG1 f hf)⟩

theorem Ws33.Core.core_two_fid
    {L F : Type*} [Field L] [Field F] [Algebra L F] (A : ValuationSubring L)
    (N₀ : Subring F) [IsLocalRing ↥N₀] (C' : Subring L) (hC'A : ∀ c : L, c ∈ C' → c ∈ A)
    (_hC'N : ∀ c : L, c ∈ C' → algebraMap L F c ∈ N₀)
    (hconst : ∀ g : ↥N₀, ∃ (o : ↥C') (h : algebraMap L F (o : L) ∈ N₀), ¬ IsUnit (g - ⟨_, h⟩))
    (T : Subring F) (hT : T = Subring.closure ((N₀ : Set F) ∪ Set.range (fun a : ↥A => algebraMap L
      F (a : L))))
    (𝔭 : Ideal ↥T)
    (h𝔭 : 𝔭 = Ideal.span ({t : ↥T | ∃ f : ↥N₀, ¬ IsUnit f ∧ (t : F) = (f : F)} ∪
      {t : ↥T | ∃ a : ↥A, a ∈ maximalIdeal ↥A ∧ (t : F) = algebraMap L F (a : L)}))
    (P : Place L F) (hP : P.IsRational) :
    ((∀ f : F, f ∈ N₀ → f ∈ P.toValuationSubring) ∧
      (∀ f : ↥N₀, ¬ IsUnit f → ∃ h : P.evalAt (f : F) ∈ A, (⟨P.evalAt (f : F), h⟩ : ↥A) ∈
        maximalIdeal ↥A)) ↔
    (∀ t : ↥T, (t : F) ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt (t : F) ∈ A, (IsUnit (⟨P.evalAt (t : F), h⟩ : ↥A) ↔ t ∉ 𝔭)) :=
  Ws33.Core.core_two A N₀ C' hC'A hconst T hT 𝔭 h𝔭 P hP

theorem Ws33.Core.core_composed
    {L F : Type*} [Field L] [Field F] [Algebra L F] (A : ValuationSubring L)
    (N₀ : Subring F) [IsLocalRing ↥N₀] (C' : Subring L) (hC'A : ∀ c : L, c ∈ C' → c ∈ A)
    (hconst : ∀ g : ↥N₀, ∃ (o : ↥C') (h : algebraMap L F (o : L) ∈ N₀), ¬ IsUnit (g - ⟨_, h⟩))
    (T : Subring F) (hT : T = Subring.closure ((N₀ : Set F) ∪ Set.range (fun a : ↥A => algebraMap L
      F (a : L))))
    (𝔭 : Ideal ↥T)
    (h𝔭 : 𝔭 = Ideal.span ({t : ↥T | ∃ f : ↥N₀, ¬ IsUnit f ∧ (t : F) = (f : F)} ∪
      {t : ↥T | ∃ a : ↥A, a ∈ maximalIdeal ↥A ∧ (t : F) = algebraMap L F (a : L)}))
    (Lx : Subring F) (hLx : ∀ f : F, f ∈ Lx ↔ ∃ b c : ↥T, c ∉ 𝔭 ∧ f * (c : F) = (b : F))
    (P : Place L F) (hP : P.IsRational) :
    ((∀ f : F, f ∈ N₀ → f ∈ P.toValuationSubring) ∧
      (∀ f : ↥N₀, ¬ IsUnit f → ∃ h : P.evalAt (f : F) ∈ A, (⟨P.evalAt (f : F), h⟩ : ↥A) ∈
        maximalIdeal ↥A)) ↔
    (∀ f : F, f ∈ Lx → f ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt f ∈ A, (IsUnit (⟨P.evalAt f, h⟩ : ↥A) ↔ ∃ g ∈ Lx, f * g = 1)) :=
  (Ws33.Core.core_two A N₀ C' hC'A hconst T hT 𝔭 h𝔭
      P hP).trans
    (Ws33.Core.core_one A T 𝔭 Lx hLx P hP)

theorem _root_.AlgebraicCurve.Place.forall_localSubring_iff_forall_localization
    {L F : Type*} [Field L] [Field F] [Algebra L F] (A : ValuationSubring L)
    (N₀ : Subring F) [IsLocalRing ↥N₀] (C' : Subring L) (hC'A : ∀ c : L, c ∈ C' → c ∈ A)
    (hconst : ∀ g : ↥N₀, ∃ (o : ↥C') (h : algebraMap L F (o : L) ∈ N₀), ¬ IsUnit (g - ⟨_, h⟩))
    (T : Subring F) (hT : T = Subring.closure ((N₀ : Set F) ∪ Set.range (fun a : ↥A => algebraMap L
      F (a : L))))
    (𝔭 : Ideal ↥T)
    (h𝔭 : 𝔭 = Ideal.span ({t : ↥T | ∃ f : ↥N₀, ¬ IsUnit f ∧ (t : F) = (f : F)} ∪
      {t : ↥T | ∃ a : ↥A, a ∈ maximalIdeal ↥A ∧ (t : F) = algebraMap L F (a : L)}))
    (Lx : Subring F) (hLx : ∀ f : F, f ∈ Lx ↔ ∃ b c : ↥T, c ∉ 𝔭 ∧ f * (c : F) = (b : F))
    (P : Place L F) (hP : P.IsRational) :
    ((∀ f : F, f ∈ N₀ → f ∈ P.toValuationSubring) ∧
      (∀ f : ↥N₀, ¬ IsUnit f → ∃ h : P.evalAt (f : F) ∈ A, (⟨P.evalAt (f : F), h⟩ : ↥A) ∈
        maximalIdeal ↥A)) ↔
    (∀ f : F, f ∈ Lx → f ∈ P.toValuationSubring ∧
        ∃ h : P.evalAt f ∈ A, (IsUnit (⟨P.evalAt f, h⟩ : ↥A) ↔ ∃ g ∈ Lx, f * g = 1)) :=
  Ws33.Core.core_composed A N₀ C' hC'A hconst T hT 𝔭 h𝔭 Lx hLx P hP