Exists_kaehlerToFunctionField_eq_smul_dCoord_of_mem_placesOf.lean

theorem KaehlerDifferential.span_singleton_D_eq_top_of_maximalIdeal_eq_span
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [IsLocalRing S]
    [Module.Finite S Ω[S⁄k]] [Algebra.FormallyUnramified k (IsLocalRing.ResidueField S)]
    {π : S} (hπ : IsLocalRing.maximalIdeal S = Ideal.span {π}) :
    Submodule.span S {D k S π} = ⊤

theorem KaehlerDifferential.exists_map_eq_smul_D_of_span_singleton_eq_top
    {k S F : Type*} [Field k] [CommRing S] [CommRing F] [Algebra k S] [Algebra k F] [Algebra S F]
    [IsScalarTower k S F] {π : S} (hπ : Submodule.span S {D k S π} = ⊤) (ω : Ω[S⁄k]) :
    ∃ s : S, KaehlerDifferential.map k k S F ω = algebraMap S F s • D k F (algebraMap S F π)

theorem IsLocalRing.maximalIdeal_eq_span_singleton_of_ringEquiv
    {S A : Type*} [CommRing S] [CommRing A] [IsLocalRing S] [IsLocalRing A] (e : S ≃+* A) {ϖ : A}
    (hϖ : IsLocalRing.maximalIdeal A = Ideal.span {ϖ}) :
    IsLocalRing.maximalIdeal S = Ideal.span {e.symm ϖ}

def algebraStalk (x : X) : Algebra k (X.presheaf.stalk x)

theorem isScalarTower_sections_stalk (W : X.Opens) (x : X) (hx : x ∈ W) :
    let := Scheme.TwoAffineOpenCover.algebraOfHom c W
    let := X.presheaf.algebra_section_stalk (⟨x, hx⟩ : W)
    let := algebraStalk c x
    IsScalarTower k Γ(X, W) (X.presheaf.stalk x) := by
  intro algSections algSectionStalk algStalk
  refine IsScalarTower.of_algebraMap_eq' ?_
  change _ = (X.presheaf.germ W x hx).hom.comp (((Scheme.ΓSpecIso (.of k)).inv ≫ c.appLE ⊤ W
    le_top).hom)
  rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Category.assoc]
  dsimp only [Scheme.Hom.appLE]
  rw [Category.assoc, TopCat.Presheaf.germ_res]

theorem isScalarTower_stalk_functionField [IsIntegral X] (x : X) :
    let := algebraStalk c x
    let := (baseToFunctionField c).toAlgebra
    IsScalarTower k (X.presheaf.stalk x) X.functionField := by
  intro algStalk algFunctionField
  refine IsScalarTower.of_algebraMap_eq' ?_
  rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra,
    baseToFunctionField,
    ← CommRingCat.hom_comp, ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
  congr 1
  simp only [Category.assoc]
  congr 1
  exact congrArg
    (fun φ : Γ(X, c ⁻¹ᵁ ⊤) ⟶ X.presheaf.stalk (genericPoint X) => c.app ⊤ ≫ φ)
    (X.presheaf.germ_stalkSpecializes (U := c ⁻¹ᵁ ⊤) (y := x) trivial
      (genericPoint_specializes x)).symm

theorem algebraMap_algebraStalk (x : X) :
    let := algebraStalk c x
    algebraMap k (X.presheaf.stalk x) =
      (c.stalkMap x).hom.comp
        ((Scheme.ΓSpecIso (.of k)).inv ≫ (Spec (.of k)).presheaf.germ ⊤ (c x) trivial).hom := by
  intro algStalk
  rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Category.assoc]
  exact congrArg
    (fun φ : Γ(Spec (.of k), ⊤) ⟶ X.presheaf.stalk x =>
      ((Scheme.ΓSpecIso (.of k)).inv ≫ φ).hom)
    (c.germ_stalkMap ⊤ x trivial).symm

theorem essFiniteType_stalk [LocallyOfFiniteType c] (x : X) :
    let := algebraStalk c x
    Algebra.EssFiniteType k (X.presheaf.stalk x) := by
  intro algStalk
  let point : PrimeSpectrum k := c x
  rw [← RingHom.essFiniteType_algebraMap, algebraMap_algebraStalk]
  refine RingHom.EssFiniteType.comp ?_ (LocallyOfFiniteType.stalkMap c x)
  have hgerm := congrArg CommRingCat.Hom.hom
    (Spec.algebraMap_stalkIso_inv (R := CommRingCat.of k) (x := point))
  rw [← hgerm, CommRingCat.hom_comp, CommRingCat.hom_ofHom]
  refine RingHom.EssFiniteType.comp ?_ ?_
  · rw [RingHom.essFiniteType_algebraMap]
    exact Algebra.EssFiniteType.of_isLocalization _ point.asIdeal.primeCompl
  · exact RingHom.FiniteType.essFiniteType
      (RingHom.FiniteType.of_surjective _ (Spec.stalkIso (.of k)
        point).commRingCatIsoToRingEquiv.symm.surjective)

theorem finite_kaehler_stalk [LocallyOfFiniteType c] (x : X) :
    let := algebraStalk c x
    Module.Finite (X.presheaf.stalk x) Ω[X.presheaf.stalk x⁄k] := by
  intro algStalk
  have := essFiniteType_stalk c x
  infer_instance

theorem fromSpecResidueField_comp (x : X) :
    X.fromSpecResidueField x ≫ c =
      Spec.map ((Scheme.ΓSpecIso (.of k)).inv ≫ c.app ⊤ ≫ X.presheaf.germ (c ⁻¹ᵁ ⊤) x trivial ≫
        X.residue x)

theorem finite_residueField_of_isClosed [LocallyOfFiniteType c] (x : X) (hx : IsClosed ({x} : Set
  X)) :
    let := algebraStalk c x
    Module.Finite k (IsLocalRing.ResidueField (X.presheaf.stalk x)) := by
  intro algStalk
  have : JacobsonSpace X := LocallyOfFiniteType.jacobsonSpace c
  have : LocallyOfFiniteType (X.fromSpecResidueField x) :=
    isClosed_singleton_iff_locallyOfFiniteType.mp hx
  have hf : IsFinite (X.fromSpecResidueField x ≫ c) :=
    isFinite_iff_locallyOfFiniteType_of_jacobsonSpace.mpr inferInstance
  rw [fromSpecResidueField_comp, IsFinite.SpecMap_iff] at hf
  have : (algebraMap k (IsLocalRing.ResidueField (X.presheaf.stalk x))) =
      ((Scheme.ΓSpecIso (.of k)).inv ≫ c.app ⊤ ≫ X.presheaf.germ (c ⁻¹ᵁ ⊤) x trivial ≫ X.residue
        x).hom := by
    rfl
  rw [← RingHom.finite_algebraMap, this]
  exact hf

theorem formallyUnramified_residueField_of_isClosed [PerfectField k] [LocallyOfFiniteType c] (x : X)
    (hx : IsClosed ({x} : Set X)) :
    let := algebraStalk c x
    Algebra.FormallyUnramified k (IsLocalRing.ResidueField (X.presheaf.stalk x)) := by
  intro algStalk
  have := finite_residueField_of_isClosed c x hx
  have : Algebra.IsAlgebraic k (IsLocalRing.ResidueField (X.presheaf.stalk x)) := inferInstance
  exact Algebra.FormallyUnramified.of_isSeparable _ _

theorem locallyOfFiniteType_of_smoothOfRelativeDimension [SmoothOfRelativeDimension 1 c] :
    LocallyOfFiniteType c

theorem _root_.AlgebraicCurve.exists_kaehlerToFunctionField_eq_smul_dCoord_of_mem_placesOf
    {k : Type u} [Field k] [PerfectField k] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of k))
    [IsIntegral X] [SmoothOfRelativeDimension 1 c]
    (U : X.Opens) [Nonempty U]
    (η : letI := Scheme.TwoAffineOpenCover.algebraOfHom c U; Ω[Γ(X, U)⁄k])
    (v : letI := (baseToFunctionField c).toAlgebra; Place k X.functionField)
    (hv : letI := (baseToFunctionField c).toAlgebra; v ∈ placesOf c U) :
    let := (baseToFunctionField c).toAlgebra
    ∃ f ∈ v.toValuationSubring, kaehlerToFunctionField c U η = f • v.dCoord := by
  intro algFunctionField
  let := Scheme.TwoAffineOpenCover.algebraOfHom c U
  obtain ⟨x, hxU, hxcl, hrange⟩ := hv
  let := algebraStalk c x
  let := X.presheaf.algebra_section_stalk (⟨x, hxU⟩ : U)
  have := isScalarTower_sections_stalk c U x hxU
  have := isScalarTower_stalk_functionField c x
  have : IsScalarTower Γ(X, U) (X.presheaf.stalk x) X.functionField := functionField_isScalarTower
    X U ⟨x, hxU⟩
  have hφ : algebraMap Γ(X, U) X.functionField =
      (algebraMap (X.presheaf.stalk x) X.functionField).comp (algebraMap Γ(X, U) (X.presheaf.stalk
        x)) :=
    IsScalarTower.algebraMap_eq Γ(X, U) (X.presheaf.stalk x) X.functionField
  have hinj : Function.Injective (algebraMap (X.presheaf.stalk x) X.functionField) :=
    IsFractionRing.injective (X.presheaf.stalk x) X.functionField
  have hmem : ∀ s, algebraMap (X.presheaf.stalk x) X.functionField s ∈ v.toValuationSubring := fun
    s => by
    have : algebraMap (X.presheaf.stalk x) X.functionField s ∈ (algebraMap (X.presheaf.stalk x)
      X.functionField).range :=
      ⟨s, rfl⟩
    rw [hrange] at this
    exact this
  have hsurj : ∀ t ∈ v.toValuationSubring, ∃ s, algebraMap (X.presheaf.stalk x) X.functionField s =
    t := fun t ht => by
    have : t ∈ v.toValuationSubring.toSubring := ht
    rw [← hrange] at this
    exact this
  let ψ : X.presheaf.stalk x →+* v.toValuationSubring :=
    (algebraMap (X.presheaf.stalk x) X.functionField).codRestrict v.toValuationSubring hmem
  have hψ : Function.Bijective ψ :=
    ⟨fun a b h => hinj (congrArg Subtype.val h), fun t => by
      obtain ⟨s, hs⟩ := hsurj t.1 t.2; exact ⟨s, Subtype.ext hs⟩⟩
  let e : X.presheaf.stalk x ≃+* v.toValuationSubring := RingEquiv.ofBijective ψ hψ
  have he : ∀ s, ((e s : v.toValuationSubring) : X.functionField) = algebraMap _ X.functionField s
    := fun s => rfl
  have hϖ := (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose_spec
  have hdC : v.dCoord = D k X.functionField
      (((IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose :
        v.toValuationSubring) :
        X.functionField) := rfl
  have hmax : IsLocalRing.maximalIdeal (X.presheaf.stalk x) =
      Ideal.span {e.symm (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose}
        :=
    IsLocalRing.maximalIdeal_eq_span_singleton_of_ringEquiv e hϖ.maximalIdeal_eq
  have hφπ : algebraMap (X.presheaf.stalk x) X.functionField
      (e.symm (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose) =
      (((IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose :
        v.toValuationSubring) :
        X.functionField) := by
    rw [← he, e.apply_symm_apply]
  have := locallyOfFiniteType_of_smoothOfRelativeDimension c
  have hfin : Module.Finite (X.presheaf.stalk x) Ω[X.presheaf.stalk x⁄k] := finite_kaehler_stalk c x
  have hunr : Algebra.FormallyUnramified k (IsLocalRing.ResidueField (X.presheaf.stalk x)) :=
    formallyUnramified_residueField_of_isClosed c x hxcl
  have hspan := KaehlerDifferential.span_singleton_D_eq_top_of_maximalIdeal_eq_span (k := k) hmax
  have hD : ∀ s' : X.presheaf.stalk x, ∃ t : X.presheaf.stalk x,
      D k X.functionField (algebraMap _ X.functionField s') =
        algebraMap _ X.functionField t • v.dCoord := fun s' => by
    obtain ⟨t, ht⟩ := KaehlerDifferential.exists_map_eq_smul_D_of_span_singleton_eq_top
      (F := X.functionField) hspan (D k (X.presheaf.stalk x) s')
    refine ⟨t, ?_⟩
    rw [KaehlerDifferential.map_D] at ht
    rw [ht, hφπ, hdC]
  have hgen : ∀ b : Γ(X, U), kaehlerToFunctionField c U (D k Γ(X, U) b) =
      D k X.functionField (algebraMap _ X.functionField (algebraMap Γ(X, U) (X.presheaf.stalk x)
        b)) := fun b => by
    rw [kaehlerToFunctionField_D, ← RingHom.comp_apply, ← hφ]
    rfl
  suffices H : ∀ θ ∈ Submodule.span Γ(X, U) (Set.range (D k Γ(X, U))),
      ∃ s : X.presheaf.stalk x, kaehlerToFunctionField c U θ = algebraMap _ X.functionField s •
        v.dCoord by
    obtain ⟨s, hs⟩ := H η
      (by rw [KaehlerDifferential.span_range_derivation]; exact Submodule.mem_top)
    exact ⟨_, hmem s, hs⟩
  intro θ hθ
  refine Submodule.span_induction ?_ ⟨0, by simp⟩ ?_ ?_ hθ
  · rintro _ ⟨b, rfl⟩
    obtain ⟨t, ht⟩ := hD (algebraMap Γ(X, U) (X.presheaf.stalk x) b)
    exact ⟨t, by rw [hgen, ht]⟩
  · rintro θ₁ θ₂ - - ⟨s₁, h₁⟩ ⟨s₂, h₂⟩
    exact ⟨s₁ + s₂, by rw [map_add, h₁, h₂, map_add, add_smul]⟩
  · rintro a θ - ⟨s, hs⟩
    refine ⟨algebraMap Γ(X, U) (X.presheaf.stalk x) a * s, ?_⟩
    rw [kaehlerToFunctionField_smul, hs, map_mul, ← RingHom.comp_apply, ← hφ, smul_smul]
    rfl