SmoothProperCurve_nontrivial_tensor_sections_of_twoChartPoleDatum.lean

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 nontrivial_tensor_fields {R : Type u} [CommRing R] (𝔭 : Ideal R) [𝔭.IsPrime]
    (K F : Type u) [Field K] [Field F] [Algebra R K] [Algebra R F]
    (hK : ∀ r, algebraMap R K r = 0 ↔ r ∈ 𝔭) (hF : ∀ r, algebraMap R F r = 0 ↔ r ∈ 𝔭) :
    Nontrivial (K ⊗[R] F)

theorem eval_algebraMap_eq_zero_iff
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {U : C.Opens} (u : C) (hu : u ∈ U) (r : R) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    (C.evaluation U u hu).hom (algebraMap R Γ(C, U) r) = 0 ↔ r ∈ (c.base u).asIdeal := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  rw [Scheme.TwoAffineOpenCover.algebraMap_algebraOfHom]
  erw [Scheme.evaluation_eq_zero_iff_notMem_basicOpen, Scheme.basicOpen_appLE,
    basicOpen_eq_of_affine]
  rw [TopologicalSpace.Opens.mem_inf, not_and]
  constructor
  · intro h
    have h2 : u ∉ c ⁻¹ᵁ PrimeSpectrum.basicOpen r := h hu
    change ¬ (c.base u ∈ PrimeSpectrum.basicOpen r) at h2
    exact not_not.mp ((not_congr (PrimeSpectrum.mem_basicOpen r (c.base u))).mp h2)
  · intro hr _
    change ¬ (c.base u ∈ PrimeSpectrum.basicOpen r)
    exact fun h => ((PrimeSpectrum.mem_basicOpen r (c.base u)).mp h) hr

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) (_hU : IsAffineOpen U) (_hV : IsAffineOpen V) (_hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base)
    (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 c U
    Nontrivial (K ⊗[R] Γ(C, U)) := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  have : (RingHom.ker (algebraMap R K)).IsPrime := RingHom.ker_isPrime _
  let y : Spec (CommRingCat.of R) := ⟨RingHom.ker (algebraMap R K), RingHom.ker_isPrime _⟩
  obtain ⟨u, hcu, hur⟩ := exists_mem_fibre_not_mem_range c ε y
  have hu : u ∈ U := (hUε u).mpr hur
  let ev : Γ(C, U) →+* C.residueField u := (C.evaluation U u hu).hom
  let algRF : Algebra R (C.residueField u) := (ev.comp (algebraMap R Γ(C, U))).toAlgebra
  let evₐ : Γ(C, U) →ₐ[R] C.residueField u :=
    { ev with commutes' := fun _ => rfl }
  have hF : ∀ r : R, algebraMap R (C.residueField u) r = 0 ↔ r ∈ RingHom.ker (algebraMap R K) := by
    intro r
    change ev (algebraMap R Γ(C, U) r) = 0 ↔ _
    rw [eval_algebraMap_eq_zero_iff c u hu r, hcu]
  have hK : ∀ r : R, algebraMap R K r = 0 ↔ r ∈ RingHom.ker (algebraMap R K) := fun r => Iff.rfl
  have := nontrivial_tensor_fields (RingHom.ker (algebraMap R K)) K (C.residueField u) hK hF
  exact (Algebra.TensorProduct.map (AlgHom.id K K) evₐ).toRingHom.domain_nontrivial

theorem _root_.AlgebraicGeometry.SmoothProperCurve.nontrivial_tensor_sections_of_twoChartPoleDatum
    (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) (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : U ⊔ V = ⊤)
    (hUε : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base)
    (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 c U
    Nontrivial (K ⊗[R] Γ(C, U)) :=
  NONEMPTY.main R c ε U V hU hV hUV hUε f g hf hg hfg K