GenusZeroPunctured.lean

theorem exists_ratFunc_algEquiv_infinity_of_genus_zero (hg : genusFF K F = 0)
    (v : Place K F) :
    ∃ e : RatFunc K ≃ₐ[K] F,
      Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
        (RationalFunctionField.placeInfty K) = v := by
  classical
  obtain ⟨w, _, hnot, _⟩ :=
    exists_place_notMem_ord_neg_and_forall_ord_eq_one (K := K) (F := F) {v}
  have hne : w ≠ v := fun h => hnot (Finset.mem_singleton.mpr h)
  obtain ⟨t, _, htr, hgen, hord⟩ := exists_parameter_of_genus_zero hg w v hne
  let e : RatFunc K ≃ₐ[K] F := (RatFunc.algEquivOfTranscendental t htr).trans
    ((IntermediateField.equivOfEq hgen).trans IntermediateField.topEquiv)
  have heX : e RatFunc.X = t := by
    change ((RatFunc.algEquivOfTranscendental t htr) RatFunc.X : F) = t
    rw [RatFunc.algEquivOfTranscendental_X]
  refine ⟨e, ?_⟩
  let u := Place.congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
    (RationalFunctionField.placeInfty K)
  have hneg : u.ord t = -1 := by
    rw [← heX]
    exact (Place.ord_congrRingEquiv e.toRingEquiv (fun a => e.commutes a)
      (RationalFunctionField.placeInfty K) RatFunc.X).trans
        (RationalFunctionField.ord_placeInfty_X K)
  have hv : u = v := by
    by_contra huv
    rw [hord, ite_eq_right huv] at hneg
    split_ifs at hneg <;> omega
  exact hv

theorem nonempty_affineLine_iso_of_genus_zero_complement
    (M : CurveModel K F) (hg : genusFF K F = 0) (x : closedPoints M.C)
    (U : M.C.Opens) (hU : (U : Set M.C) = {x.1}ᶜ) :
    Nonempty (U.toScheme ≅ Spec (.of K[X]))

theorem subsingleton_fundamentalGroup_of_genus_zero_complement
    (M : CurveModel K F) (hg : genusFF K F = 0) (x : closedPoints M.C)
    (U : M.C.Opens) (hU : (U : Set M.C) = {x.1}ᶜ)
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    Subsingleton π₁ᵉᵗ(ξ)