FunctionFieldConstantExtension.lean

theorem germToFunctionField_algebraOfHom
    {K : Type} [Field K] {X : Scheme} [IsIntegral X]
    (c : X ⟶ Spec (.of K)) (U : X.Opens) [Nonempty U] (a : K) :
    let _ := algebraOfHom c U
    X.germToFunctionField U (algebraMap K Γ(X, U) a) = baseToFunctionField c a := by
  let _ := algebraOfHom c U
  change (X.germToFunctionField U).hom
    ((c.appLE ⊤ U le_top).hom ((Scheme.ΓSpecIso (.of K)).inv.hom a)) = _
  change (X.germToFunctionField U).hom
    ((X.presheaf.map (homOfLE (show U ≤ ⊤ from le_top)).op).hom
      (c.appTop.hom ((Scheme.ΓSpecIso (.of K)).inv.hom a))) = _
  exact X.presheaf.germ_res_apply (homOfLE (show U ≤ ⊤ from le_top))
    (genericPoint X) _ (c.appTop.hom ((Scheme.ΓSpecIso (.of K)).inv.hom a))

theorem adjoin_range_functionField_baseChange
    {K : Type} [Field K] (K' : Type) [Field K'] [Algebra K K']
    {X : Scheme} [IsIntegral X] (c : X ⟶ Spec (.of K))
    [IsIntegral (pullback c (specMap K K'))]
    (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U]
    [Nonempty ((pullback.fst c (specMap K K')) ⁻¹ᵁ U)]
    (φ : X.functionField →+* (pullback c (specMap K K')).functionField)
    (hsq : ∀ a : Γ(X, U),
      (pullback c (specMap K K')).germToFunctionField
        ((pullback.fst c (specMap K K')) ⁻¹ᵁ U)
        (((pullback.fst c (specMap K K')).app U).hom a) =
          φ (X.germToFunctionField U a)) :
    let _ : Algebra K' (pullback c (specMap K K')).functionField :=
      (baseToFunctionField (pullback.snd c (specMap K K'))).toAlgebra
    IntermediateField.adjoin K' (Set.range φ) = ⊤ := by
  let Y := pullback c (specMap K K')
  let V := (pullback.fst c (specMap K K')) ⁻¹ᵁ U
  let _ := algebraOfHom c U
  let _ := algebraOfHom (pullback.snd c (specMap K K')) V
  let _ : Algebra K' Y.functionField :=
    (baseToFunctionField (pullback.snd c (specMap K K'))).toAlgebra
  have htower : IsScalarTower K' Γ(Y, V) Y.functionField :=
    IsScalarTower.of_algebraMap_eq fun a =>
      (germToFunctionField_algebraOfHom (pullback.snd c (specMap K K')) V a).symm
  have hV : IsAffineOpen V :=
    IsAffine.of_isIso
      (Scheme.TwoAffineOpenCover.AffineBaseChange.pullbackAffineOpenIsoSpecTensor
        c K' U hU).hom
  have hfrac : IsFractionRing Γ(Y, V) Y.functionField :=
    functionField_isFractionRing_of_isAffineOpen Y V hV
  obtain ⟨e, he⟩ := exists_algEquiv_tensorProduct_sections_preimage K' c U hU
  apply IntermediateField.adjoin_range_eq_top_of_tensor_fraction e
    (X.germToFunctionField U).hom φ
  intro a
  rw [he]
  exact hsq a

theorem exists_functionField_constantExtension
    {K : Type} [Field K] (K' : Type) [Field K'] [Algebra K K']
    {X : Scheme} [IsIntegral X] (c : X ⟶ Spec (.of K))
    [IsIntegral (pullback c (specMap K K'))] :
    let _ : Algebra K' (pullback c (specMap K K')).functionField :=
      (baseToFunctionField (pullback.snd c (specMap K K'))).toAlgebra
    ∃ φ : X.functionField →+* (pullback c (specMap K K')).functionField,
      (∀ (U : X.Opens) [Nonempty U]
          [Nonempty ((pullback.fst c (specMap K K')) ⁻¹ᵁ U)]
          (a : Γ(X, U)),
        (pullback c (specMap K K')).germToFunctionField
          ((pullback.fst c (specMap K K')) ⁻¹ᵁ U)
          (((pullback.fst c (specMap K K')).app U).hom a) =
            φ (X.germToFunctionField U a)) ∧
      IntermediateField.adjoin K' (Set.range φ) = ⊤ := by
  let Y := pullback c (specMap K K')
  let f : Y ⟶ X := pullback.fst c (specMap K K')
  let _ : Algebra K' Y.functionField :=
    (baseToFunctionField (pullback.snd c (specMap K K'))).toAlgebra
  have hη (U : X.Opens) (hU : (U : Set X).Nonempty) :
      genericPoint Y ∈ f ⁻¹ᵁ U := by
    have h := genericPoint_mem_preimage_comp_pullback_fst_of_injective_algebraMap
      (algebraMap K K').injective c (𝟙 Y) U hU
    simpa only [Category.id_comp] using h
  have hf : f.base (genericPoint Y) = genericPoint X := by
    have hgp : IsGenericPoint (f.base (genericPoint Y)) Set.univ := by
      rw [isGenericPoint_iff_specializes]
      intro z
      simp only [Set.mem_univ, iff_true]
      rw [specializes_iff_forall_open]
      intro U hU hzU
      exact hη ⟨U, hU⟩ ⟨z, hzU⟩
    exact (hgp.inseparable (genericPoint_spec X)).eq
  obtain ⟨φ, hφ⟩ := exists_ringHom_functionField_germ_eq_of_base_genericPoint_eq f hf
  have hs (U : X.Opens) [Nonempty U] [Nonempty (f ⁻¹ᵁ U)] (a : Γ(X, U)) :
      Y.germToFunctionField (f ⁻¹ᵁ U) ((f.app U).hom a) =
        φ (X.germToFunctionField U a) := by
    have hUset : (U : Set X).Nonempty :=
      ⟨(Classical.choice ‹Nonempty U›).1, (Classical.choice ‹Nonempty U›).2⟩
    exact (hφ U (((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr
      ⟨(Classical.choice ‹Nonempty U›).1,
        Set.mem_univ _, (Classical.choice ‹Nonempty U›).2⟩)
      (hη U hUset) a).symm
  refine ⟨φ, hs, ?_⟩
  let U := (X.affineCover.f (X.affineCover.idx (genericPoint X))).opensRange
  have hU : IsAffineOpen U := isAffineOpen_opensRange (X.affineCover.f _)
  have hne : Nonempty U := ⟨⟨genericPoint X, X.affineCover.covers _⟩⟩
  have hne' : Nonempty (f ⁻¹ᵁ U) :=
    ⟨⟨genericPoint Y, hη U ⟨genericPoint X, X.affineCover.covers _⟩⟩⟩
  exact adjoin_range_functionField_baseChange K' c U hU φ (hs U)