SmoothProperCurve_flat_aeval_of_twoChartPoleDatum.lean

theorem flat_aeval_of_injective {κ D : Type u} [Field κ] [CommRing D] [IsDomain D] [Algebra κ D] (y
  : D)
    (hinj : Function.Injective (Polynomial.aeval y : κ[X] →ₐ[κ] D)) :
    (Polynomial.aeval y : κ[X] →ₐ[κ] D).toRingHom.Flat

theorem flat_of_subsingleton {A D : Type u} [CommRing A] [CommRing D] [Subsingleton D] (φ : A →+*
  D) :
    φ.Flat

theorem flat_sections [Flat c] {U : X.Opens} (hU : IsAffineOpen U) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    Module.Flat R Γ(X, U) := by
  have h : RingHom.Flat (c.appLE ⊤ U le_top).hom :=
    HasRingHomProperty.appLE (P := @Flat) (f := c) inferInstance ⟨⊤, isAffineOpen_top _⟩ ⟨U, hU⟩
      le_top
  have h2 : RingHom.Flat ((Scheme.ΓSpecIso (.of R)).inv ≫ c.appLE ⊤ U le_top).hom := by
    rw [CommRingCat.hom_comp]
    exact RingHom.Flat.comp
      (RingHom.Flat.of_bijective (Scheme.ΓSpecIso (.of
        R)).symm.commRingCatIsoToRingEquiv.bijective) h
  exact h2

theorem finitePresentation_sections [LocallyOfFinitePresentation c] {U : X.Opens} (hU :
  IsAffineOpen U) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    Algebra.FinitePresentation R Γ(X, U) := by
  have h : RingHom.FinitePresentation (c.appLE ⊤ U le_top).hom :=
    HasRingHomProperty.appLE (P := @LocallyOfFinitePresentation) (f := c) inferInstance
      ⟨⊤, isAffineOpen_top _⟩ ⟨U, hU⟩ le_top
  have h2 : RingHom.FinitePresentation ((Scheme.ΓSpecIso (.of R)).inv ≫ c.appLE ⊤ U le_top).hom :=
    by
    rw [CommRingCat.hom_comp]
    exact RingHom.finitePresentation_respectsIso.2 _
      (Scheme.ΓSpecIso (.of R)).symm.commRingCatIsoToRingEquiv h
  exact h2

theorem fibreMap_comp_polyEquivTensor
    [Algebra R[X] B] [IsScalarTower R R[X] B] (hX : algebraMap R[X] B Polynomial.X = f) :
    (Algebra.TensorProduct.map (AlgHom.id κ κ) (IsScalarTower.toAlgHom R R[X] B)).toRingHom.comp
        (polyEquivTensor R κ).toRingHom =
      (Polynomial.aeval ((1 : κ) ⊗ₜ[R] f) : κ[X] →ₐ[κ] κ ⊗[R] B).toRingHom

theorem flat_fibreMap_of_flat_aeval
    [Algebra R[X] B] [IsScalarTower R R[X] B] (hX : algebraMap R[X] B Polynomial.X = f)
    (h : (Polynomial.aeval ((1 : κ) ⊗ₜ[R] f) : κ[X] →ₐ[κ] κ ⊗[R] B).toRingHom.Flat) :
    (Algebra.TensorProduct.map (AlgHom.id κ κ) (IsScalarTower.toAlgHom R R[X] B)).toRingHom.Flat

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) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    (Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Flat := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  have : Smooth c := SmoothOfRelativeDimension.smooth 1 c
  have : Module.Flat R Γ(C, U) := flat_sections c hU
  have : Algebra.FinitePresentation R Γ(C, U) := finitePresentation_sections c hU
  let algXB : Algebra R[X] Γ(C, U) := (Polynomial.aeval f : R[X] →ₐ[R] Γ(C, U)).toRingHom.toAlgebra
  have : IsScalarTower R R[X] Γ(C, U) := IsScalarTower.of_algebraMap_eq fun r => by
    change algebraMap R Γ(C, U) r = (Polynomial.aeval f : R[X] →ₐ[R] Γ(C, U)) (algebraMap R R[X] r)
    rw [AlgHom.commutes]
  have hX : algebraMap R[X] Γ(C, U) Polynomial.X = f := Polynomial.aeval_X f
  change Module.Flat R[X] Γ(C, U)
  refine Module.Flat.of_finitePresentation_of_forall_flat_residueField_tensorProduct
    (R := R) (A := R[X]) (B := Γ(C, U)) fun p _ => ?_
  refine flat_fibreMap_of_flat_aeval f p.ResidueField hX ?_
  by_cases hne : Nontrivial (p.ResidueField ⊗[R] Γ(C, U))
  · have := AlgebraicGeometry.isDomain_tensorProduct_sections_of_geometricallyIntegral c U hU
      p.ResidueField hne
    exact flat_aeval_of_injective _
      (AlgebraicGeometry.SmoothProperCurve.injective_aeval_tensor_of_twoChartPoleDatum
        R c ε U V hU hV hUV hUε f g hf hg hfg p.ResidueField hne)
  · have : Subsingleton (p.ResidueField ⊗[R] Γ(C, U)) := not_nontrivial_iff_subsingleton.mp hne
    exact flat_of_subsingleton _

theorem _root_.AlgebraicGeometry.SmoothProperCurve.flat_aeval_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) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    (Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Flat :=
  U3bFLAT.main R c ε U V hU hV hUV hUε f g hf hg hfg