SmoothProperCurve_transcendental_app_of_twoChart_of_section_mem.lean

theorem zero_or_isUnit_of_isAlgebraic {K D : Type u} [Field K] [CommRing D] [IsDomain D]
  [Algebra K D]
    (a : D) (h : IsAlgebraic K a) : a = 0 ∨ IsUnit a

theorem zero_or_isUnit_of_isField {D : Type u} [CommRing D] (hD : IsField D) (a : D) : a =
  0 ∨ IsUnit a

theorem exists_mem_fibre_not_mem_range
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : NeronModelInfra.SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (y : Spec (CommRingCat.of R)) :
    ∃ u : C, c.base u = y ∧ u ∉ Set.range ε.1.base

theorem main
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : NeronModelInfra.SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U V : C.Opens) (hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base) (hεV : ∀ x ∈ Set.range ε.1.base, x ∈ V)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hf : U ⊓ V = C.basicOpen f) (hg : U ⊓ V = C.basicOpen g)
    (_hfg : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
      (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1)
    (K : Type u) [Field K] [Algebra R K] :
    (letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) ∧
    (letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
        ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ V);
      Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app V).hom g))
        := by
  let sK := Scheme.TwoAffineOpenCover.specMap R K
  let CK := pullback c sK
  let π : CK ⟶ C := pullback.fst c sK
  let σ : CK ⟶ Spec (CommRingCat.of K) := pullback.snd c sK
  let UK : CK.Opens := π ⁻¹ᵁ U
  let VK : CK.Opens := π ⁻¹ᵁ V
  let fK : Γ(CK, UK) := (π.app U).hom f
  let gK : Γ(CK, VK) := (π.app V).hom g
  let t : Spec (CommRingCat.of K) := IsLocalRing.closedPoint K
  let y : Spec (CommRingCat.of R) := sK.base t
  have : IsIntegral CK :=
    pullback_of_geometrically (GeometricallyIntegral.geometrically_isIntegral (f := c)) K sK
  have hUVf : UK ⊓ VK = CK.basicOpen fK := by
    change π ⁻¹ᵁ U ⊓ π ⁻¹ᵁ V = CK.basicOpen ((π.app U).hom f)
    rw [← Scheme.preimage_basicOpen, ← hf]; rfl
  have hUVg : UK ⊓ VK = CK.basicOpen gK := by
    change π ⁻¹ᵁ U ⊓ π ⁻¹ᵁ V = CK.basicOpen ((π.app V).hom g)
    rw [← Scheme.preimage_basicOpen, ← hg]; rfl
  have hcov : UK ⊔ VK = ⊤ := by
    change π ⁻¹ᵁ U ⊔ π ⁻¹ᵁ V = ⊤
    rw [← Scheme.Hom.preimage_sup, hUV]; rfl
  obtain ⟨u, hcu, hur⟩ := exists_mem_fibre_not_mem_range c ε y
  have huU : u ∈ U := (hUε u).mpr hur
  obtain ⟨zU, hzU, -⟩ := Scheme.Pullback.exists_preimage_pullback (f := c) (g := sK) u t hcu
  have hzU' : zU ∈ UK := by
    change π.base zU ∈ U
    change (pullback.fst c sK).base zU = u at hzU
    rw [hzU]; exact huU
  have hcε : ∀ z, c.base (ε.1.base z) = z := fun z => by
    have := Scheme.Hom.comp_apply ε.1 c z
    rw [ε.2] at this
    exact this.symm
  obtain ⟨zV, hzV, -⟩ := Scheme.Pullback.exists_preimage_pullback (f := c) (g := sK)
    (ε.1.base y) t (hcε y)
  have hzV' : zV ∈ VK := by
    change π.base zV ∈ V
    change (pullback.fst c sK).base zV = ε.1.base y at hzV
    rw [hzV]; exact hεV _ ⟨y, rfl⟩
  have hzVU : zV ∉ UK := by
    change π.base zV ∉ U
    change (pullback.fst c sK).base zV = ε.1.base y at hzV
    rw [hzV]; exact fun h => (hUε _).mp h ⟨y, rfl⟩
  have hirr := (IrreducibleSpace.isIrreducible_univ CK).isPreirreducible
  have not_disjoint : UK ⊓ VK ≠ ⊥ := by
    intro hbot
    obtain ⟨w, -, hwU, hwV⟩ := hirr _ _ UK.isOpen VK.isOpen ⟨zU, trivial, hzU'⟩ ⟨zV, trivial, hzV'⟩
    have hw : w ∈ UK ⊓ VK := ⟨hwU, hwV⟩
    rw [hbot] at hw
    exact hw
  have not_VK_le_UK : ¬ (VK ≤ UK) := fun h => hzVU (h hzV')
  have : Nonempty UK := ⟨⟨zU, hzU'⟩⟩
  have : Nonempty VK := ⟨⟨zV, hzV'⟩⟩
  have : IsDomain Γ(CK, UK) := IsIntegral.component_integral UK
  have : IsDomain Γ(CK, VK) := IsIntegral.component_integral VK
  have hg_cases : ¬ (gK = 0 ∨ IsUnit gK) := by
    rintro (h0 | hunit)
    · apply not_disjoint
      rw [hUVg, h0]
      exact Scheme.basicOpen_zero _ _
    · apply not_VK_le_UK
      have hb : CK.basicOpen gK = VK := Scheme.basicOpen_of_isUnit _ hunit
      intro w hw
      have : w ∈ UK ⊓ VK := by rw [hUVg, hb]; exact hw
      exact this.1
  refine ⟨?_, ?_⟩
  · let := Scheme.TwoAffineOpenCover.algebraOfHom σ UK
    intro halg
    rcases zero_or_isUnit_of_isAlgebraic fK halg with h0 | hunit
    · apply not_disjoint
      rw [hUVf, h0]
      exact Scheme.basicOpen_zero _ _
    · have hb : CK.basicOpen fK = UK := Scheme.basicOpen_of_isUnit _ hunit
      have hle : UK ≤ VK := by
        intro w hw
        have : w ∈ UK ⊓ VK := by rw [hUVf, hb]; exact hw
        exact this.2
      have htop : VK = ⊤ := by
        apply top_le_iff.mp
        rw [← hcov]
        exact sup_le hle le_rfl
      have hF : IsField Γ(CK, ⊤) := isField_of_universallyClosed (f := σ)
      let e : Γ(CK, ⊤) ≃+* Γ(CK, VK) :=
        (CK.presheaf.mapIso (eqToIso htop).op).commRingCatIsoToRingEquiv
      have hFV : IsField Γ(CK, VK) := MulEquiv.isField hF e.symm.toMulEquiv
      exact hg_cases (zero_or_isUnit_of_isField hFV gK)
  · let := Scheme.TwoAffineOpenCover.algebraOfHom σ VK
    intro halg
    exact hg_cases (zero_or_isUnit_of_isAlgebraic gK halg)

theorem _root_.AlgebraicGeometry.SmoothProperCurve.transcendental_app_of_twoChart_of_section_mem
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U V : C.Opens) (hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base) (hεV : ∀ x ∈ Set.range ε.1.base, x ∈ V)
    (f : Γ(C, U)) (g : Γ(C, V))
    (hf : U ⊓ V = C.basicOpen f) (hg : U ⊓ V = C.basicOpen g)
    (hfg : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
      (C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1) :
    (∀ (K : Type u) [Field K] [Algebra R K],
        letI := Scheme.TwoAffineOpenCover.algebraOfHom
          (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
          ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
        Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) ∧
      (∀ (K : Type u) [Field K] [Algebra R K],
        letI := Scheme.TwoAffineOpenCover.algebraOfHom
          (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
          ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ V);
        Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app V).hom
          g)) :=
  ⟨fun K _ _ => (ORDERTRANSC.main R c ε U V hUV hUε hεV f g hf hg hfg K).1,
   fun K _ _ => (ORDERTRANSC.main R c ε U V hUV hUε hεV f g hf hg hfg K).2⟩