existsUnique_lift_fromNormalization_kummer_of_isAffineOpen.lean

theorem genericPoint_mem (V : X.Opens) [hV : Nonempty V] : genericPoint X ∈ V

theorem preimage_eq_top {A : CommRingCat.{u}} (φ : X.functionField ⟶ A) (V : X.Opens) [hV :
  Nonempty V] :
    (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)) ⁻¹ᵁ V = ⊤

theorem app_eq {A : CommRingCat.{u}} (φ : X.functionField ⟶ A) (V : X.Opens) [hV : Nonempty V] :
    (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)).app V =
      X.presheaf.germ V (genericPoint X) (genericPoint_mem V) ≫ φ ≫ (Scheme.ΓSpecIso A).inv ≫
        (Spec A).presheaf.map (homOfLE (le_top :
          (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)) ⁻¹ᵁ V ≤ ⊤)).op

abbrev KA : Type u

abbrev φK : X.functionField ⟶ CommRingCat.of (KA k g)

abbrev fK : Spec (CommRingCat.of (KA k g)) ⟶ X

def secIso (V : X.Opens) [Nonempty V] :
    Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) ≅ CommRingCat.of (KA k g)

theorem secIso_inv (V : X.Opens) [Nonempty V] :
    (secIso k g V).inv = (Scheme.ΓSpecIso (CommRingCat.of (KA k g))).inv ≫
      (Spec (CommRingCat.of (KA k g))).presheaf.map (homOfLE (le_top : (fK k g) ⁻¹ᵁ V ≤ ⊤)).op

theorem secIso_hom (V : X.Opens) [Nonempty V] :
    (secIso k g V).hom = (Spec (CommRingCat.of (KA k g))).presheaf.map
        (homOfLE (le_of_eq (preimage_eq_top (φK k g) V).symm) : ⊤ ⟶ (fK k g) ⁻¹ᵁ V).op ≫
      (Scheme.ΓSpecIso (CommRingCat.of (KA k g))).hom

theorem secIso_hom_app (V : X.Opens) [Nonempty V] (r : Γ(X, V)) :
    (secIso k g V).hom (((fK k g).app V) r) = algebraMap X.functionField (KA k g)
      (X.germToFunctionField V r)

theorem secIso_hom_res {V V' : X.Opens} [Nonempty V] [Nonempty V'] (i : (fK k g) ⁻¹ᵁ V' ⟶ (fK k g)
  ⁻¹ᵁ V)
    (z : Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V)) :
    (secIso k g V').hom ((Spec (CommRingCat.of (KA k g))).presheaf.map i.op z) = (secIso k g V).hom
      z

def secAlgEquiv (V : X.Opens) [Nonempty V] :
    letI := ((fK k g).app V).hom.toAlgebra
    Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) ≃ₐ[Γ(X, V)] KA k g :=
  letI := ((fK k g).app V).hom.toAlgebra
  AlgEquiv.ofRingEquiv (f := (secIso k g V).commRingCatIsoToRingEquiv) (fun r => by
    change (secIso k g V).hom (((fK k g).app V) r) = _
    rw [secIso_hom_app, IsScalarTower.algebraMap_apply Γ(X, V) X.functionField (KA k g)]
    rfl)

theorem secAlgEquiv_apply (V : X.Opens) [Nonempty V] (z : Γ(Spec (CommRingCat.of (KA k g)), (fK k
  g) ⁻¹ᵁ V)) :
    letI := ((fK k g).app V).hom.toAlgebra
    secAlgEquiv k g V z = (secIso k g V).hom z := rfl

theorem map_map {Z : Scheme.{u}} {A B C : Z.Opens} (i : B ⟶ A) (j : C ⟶ B) (l : C ⟶ A) (s : Γ(Z,
  A)) :
    Z.presheaf.map j.op (Z.presheaf.map i.op s) = Z.presheaf.map l.op s

theorem root_pow : (AdjoinRoot.root (Polynomial.X ^ k - Polynomial.C g : Polynomial
  X.functionField)) ^ k =
    algebraMap X.functionField (KA k g) g

def yval (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) :
    Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V) →+* KA k g

theorem yval_apply (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    letI := ((fK k g).app V).hom.toAlgebra
    yval k g V hV s = (secIso k g V).hom (((fK k g).normalizationObjIso hV).hom s).val := rfl

theorem yval_injective (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) : Function.Injective (yval
  k g V hV)

theorem preimage_toNormalization (V : X.Opens) :
    (fK k g).toNormalization ⁻¹ᵁ ((fK k g).fromNormalization ⁻¹ᵁ V) = (fK k g) ⁻¹ᵁ V

theorem yval_eq_appLE (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    yval k g V hV s = (secIso k g V).hom ((fK k g).toNormalization.appLE ((fK k
      g).fromNormalization ⁻¹ᵁ V)
      ((fK k g) ⁻¹ᵁ V) (preimage_toNormalization k g V).ge s)

theorem yval_res {V V' : X.Opens} [Nonempty V] [Nonempty V'] (hV : IsAffineOpen V) (hV' :
  IsAffineOpen V')
    (i : (fK k g).fromNormalization ⁻¹ᵁ V' ⟶ (fK k g).fromNormalization ⁻¹ᵁ V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    yval k g V' hV' (((fK k g).normalization).presheaf.map i.op s) = yval k g V hV s

theorem normalizationObjIso_hom_app (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) (r : Γ(X, V)) :
    letI := ((fK k g).app V).hom.toAlgebra
    ((fK k g).normalizationObjIso hV).hom ((fK k g).fromNormalization.app V r) =
      algebraMap Γ(X, V) (integralClosure Γ(X, V) Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ
        V)) r := by
  let := ((fK k g).app V).hom.toAlgebra
  rw [(fK k g).fromNormalization_app hV]
  change (((fK k g).normalizationObjIso hV).inv ≫ ((fK k g).normalizationObjIso hV).hom)
    (algebraMap _ _ r) = _
  rw [Iso.inv_hom_id]
  rfl

theorem yval_app (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) (r : Γ(X, V)) :
    yval k g V hV ((fK k g).fromNormalization.app V r) = algebraMap X.functionField (KA k g)
      (X.germToFunctionField V r)

theorem exists_yval_eq_root (hk : k ≠ 0) (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) (h :
  X.functionField)
    (uV : Γ(X, V)) (huV : X.germToFunctionField V uV = g / h ^ k) :
    ∃ T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V),
      yval k g V hV T = algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _

theorem isIntegrallyClosed_sections (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) : IsIntegrallyClosed Γ(X, V)

theorem yval_eq_of_toNormalization_app_eq (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) (ρ : KA k g)
    (hT : (fK k g).toNormalization.app ((fK k g).fromNormalization ⁻¹ᵁ V) T =
      (Spec (CommRingCat.of (KA k g))).presheaf.map (homOfLE le_top).op
        ((Scheme.ΓSpecIso (CommRingCat.of (KA k g))).inv ρ)) :
    yval k g V hV T = ρ

theorem root_div_pow (h : X.functionField) :
    (algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _) ^ k = algebraMap X.functionField
      (KA k g) (g / h ^ k)

theorem comp_C_mul_X_comp {F : Type*} [Field F] (q : F[X]) (c : F) (hc : c ≠ 0) :
    (q.comp (Polynomial.C c⁻¹ * Polynomial.X)).comp (Polynomial.C c * Polynomial.X) = q

theorem mk_eq_zero_of_aeval_rho_eq_zero (hk : k ≠ 0) (h : X.functionField) (hh : h ≠ 0) (uV : Γ(X,
  V))
    (huV : X.germToFunctionField V uV = g / h ^ k) (p : Γ(X, V)[X])
    (hp : Polynomial.aeval (algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _) p = 0) :
    AdjoinRoot.mk (Polynomial.X ^ k - Polynomial.C uV) p = 0

theorem existsUnique_algHom (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) (hk : IsUnit
  ((k : ℕ) : Γ(X, V)))
    (uV : Γ(X, V)) (hu : IsUnit uV) (h : X.functionField) (hh : h ≠ 0)
    (huV : X.germToFunctionField V uV = g / h ^ k)
    (T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V))
    (hT : yval k g V hV T = algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _)
    (C : Type u) [CommRing C] [Algebra Γ(X, V) C] (c : C) (hc : c ^ k = algebraMap Γ(X, V) C uV) :
    letI := ((fK k g).fromNormalization.app V).hom.toAlgebra
    ∃! χ : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V) →ₐ[Γ(X, V)] C, χ T = c := by
  let algB := ((fK k g).fromNormalization.app V).hom.toAlgebra
  let algS := ((fK k g).app V).hom.toAlgebra
  have : IsIntegrallyClosed Γ(X, V) := isIntegrallyClosed_sections V hV hnorm
  have : IsFractionRing Γ(X, V) X.functionField := functionField_isFractionRing_of_isAffineOpen X V
    hV
  have hk0 : k ≠ 0 := by
    rintro rfl
    rw [Nat.cast_zero, isUnit_zero_iff] at hk
    exact zero_ne_one hk
  set ρ : KA k g := algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _ with hρ
  have hg : g = algebraMap Γ(X, V) X.functionField uV * h ^ k := by
    change g = X.germToFunctionField V uV * h ^ k
    rw [huV, div_mul_cancel₀ _ (pow_ne_zero _ hh)]
  obtain ⟨hIC, -, -⟩ :=
    IsIntegrallyClosed.integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
      (B := Γ(X, V)) (F := X.functionField) k hk uV hu h hh g hg
  obtain ⟨Ψ, hΨT⟩ : ∃ Ψ : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V) ≃ₐ[Γ(X, V)]
      Algebra.adjoin Γ(X, V) {ρ}, (Ψ T : KA k g) = ρ := by
    let Ψ₁ : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V) ≃ₐ[Γ(X, V)]
        integralClosure Γ(X, V) Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) :=
      AlgEquiv.ofRingEquiv (f := ((fK k g).normalizationObjIso hV).commRingCatIsoToRingEquiv) (fun
        a =>
        normalizationObjIso_hom_app k g V hV a)
    let e := secAlgEquiv k g V
    let Ψ₂ : integralClosure Γ(X, V) Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) ≃ₐ[Γ(X, V)]
        integralClosure Γ(X, V) (KA k g) :=
      (e.subalgebraMap _).trans (Subalgebra.equivOfEq _ _ (integralClosure_map_algEquiv e))
    let Ψ₃ : integralClosure Γ(X, V) (KA k g) ≃ₐ[Γ(X, V)] Algebra.adjoin Γ(X, V) {ρ} :=
      Subalgebra.equivOfEq _ _ hIC
    exact ⟨Ψ₁.trans (Ψ₂.trans Ψ₃), hT⟩
  suffices lift : ∀ (B₁ : Type u) [CommRing B₁] [Algebra Γ(X, V) B₁]
      (T₁ : B₁) (Ψ₁ : B₁ ≃ₐ[Γ(X, V)] Algebra.adjoin Γ(X, V) {ρ}),
      (Ψ₁ T₁ : KA k g) = ρ → ∃! χ : B₁ →ₐ[Γ(X, V)] C, χ T₁ = c by
    exact lift _ T Ψ hΨT
  intro B₁ instB₁ algB₁ T₁ Ψ₁ hΨT₁
  obtain ⟨fu, hfu⟩ : ∃ fu : Γ(X, V)[X], fu = Polynomial.X ^ k - Polynomial.C uV := ⟨_, rfl⟩
  have hρk : ρ ^ k = algebraMap Γ(X, V) (KA k g) uV := by
    rw [hρ, root_div_pow, ← huV, IsScalarTower.algebraMap_apply Γ(X, V) X.functionField (KA k g)]
    rfl
  let ρ' : Algebra.adjoin Γ(X, V) {ρ} := ⟨ρ, Algebra.self_mem_adjoin_singleton Γ(X, V) ρ⟩
  have hρ'root : fu.eval₂ (algebraMap Γ(X, V) (Algebra.adjoin Γ(X, V) {ρ})) ρ' = 0 := by
    apply Subtype.ext
    rw [← Polynomial.aeval_def, Polynomial.aeval_subalgebra_coe]
    change Polynomial.aeval ρ fu = 0
    rw [Polynomial.aeval_def, hfu, Polynomial.eval₂_sub, Polynomial.eval₂_X_pow,
      Polynomial.eval₂_C, hρk, sub_self]
  obtain ⟨θ, hθroot, hθinj, hθsurj⟩ :
      ∃ θ : AdjoinRoot fu →ₐ[Γ(X, V)] Algebra.adjoin Γ(X, V) {ρ},
        θ (AdjoinRoot.root fu) = ρ' ∧ Function.Injective θ ∧ Function.Surjective θ := by
    let θ : AdjoinRoot fu →ₐ[Γ(X, V)] Algebra.adjoin Γ(X, V) {ρ} :=
      AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) ρ' hρ'root
    have hθroot : θ (AdjoinRoot.root fu) = ρ' := AdjoinRoot.liftAlgHom_root _ _ _ _
    have hθsurj : Function.Surjective θ := by
      rintro ⟨y, hy⟩
      rw [Algebra.adjoin_singleton_eq_range_aeval] at hy
      obtain ⟨p, rfl⟩ := hy
      refine ⟨AdjoinRoot.mk fu p, Subtype.ext ?_⟩
      change ((AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) ρ' hρ'root (AdjoinRoot.mk fu p) :
        Algebra.adjoin Γ(X, V) {ρ}) : KA k g) = _
      refine (congrArg (fun y : Algebra.adjoin Γ(X, V) {ρ} => (y : KA k g))
        (AdjoinRoot.liftAlgHom_mk fu (Algebra.ofId _ _) ρ' hρ'root p)).trans ?_
      change ((Polynomial.eval₂ (algebraMap Γ(X, V) (Algebra.adjoin Γ(X, V) {ρ})) ρ' p :
        Algebra.adjoin Γ(X, V) {ρ}) : KA k g) =
        Polynomial.aeval ρ p
      rw [← Polynomial.aeval_def, Polynomial.aeval_subalgebra_coe]
    have hθinj : Function.Injective θ := by
      rw [injective_iff_map_eq_zero]
      intro x hx
      induction x using AdjoinRoot.induction_on with
      | ih p =>
        rw [hfu]
        apply mk_eq_zero_of_aeval_rho_eq_zero k g V hV hk0 h hh uV huV p
        have hx' := congrArg (fun y : Algebra.adjoin Γ(X, V) {ρ} => (y : KA k g)) hx
        change ((AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) ρ' hρ'root (AdjoinRoot.mk fu p) :
          Algebra.adjoin Γ(X, V) {ρ}) : KA k g) = 0 at hx'
        have hev := congrArg (fun y : Algebra.adjoin Γ(X, V) {ρ} => (y : KA k g))
          (AdjoinRoot.liftAlgHom_mk fu (Algebra.ofId _ _) ρ' hρ'root p)
        have hx'' := hev.symm.trans hx'
        change ((Polynomial.eval₂ (algebraMap Γ(X, V) (Algebra.adjoin Γ(X, V) {ρ})) ρ' p :
          Algebra.adjoin Γ(X, V) {ρ}) : KA k g) = 0
          at hx''
        rw [← Polynomial.aeval_def, Polynomial.aeval_subalgebra_coe] at hx''
        exact hx''
    exact ⟨θ, hθroot, hθinj, hθsurj⟩
  obtain ⟨Θ, hΘ⟩ : ∃ Θ : B₁ ≃ₐ[Γ(X, V)] AdjoinRoot fu,
      Θ = Ψ₁.trans (AlgEquiv.ofBijective θ ⟨hθinj, hθsurj⟩).symm := ⟨_, rfl⟩
  have hΘT : Θ T₁ = AdjoinRoot.root fu := by
    rw [hΘ, AlgEquiv.trans_apply]
    rw [AlgEquiv.symm_apply_eq]
    apply Subtype.ext
    rw [hΨT₁]
    change ρ = ((θ (AdjoinRoot.root fu) : Algebra.adjoin Γ(X, V) {ρ}) : KA k g)
    rw [hθroot]
  have hcroot : fu.eval₂ (algebraMap Γ(X, V) C) c = 0 := by
    rw [hfu, Polynomial.eval₂_sub, Polynomial.eval₂_X_pow, Polynomial.eval₂_C, hc, sub_self]
  refine ⟨(AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) c hcroot).comp Θ.toAlgHom, ?_, ?_⟩
  · change AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) c hcroot (Θ T₁) = c
    rw [hΘT]
    exact AdjoinRoot.liftAlgHom_root fu (Algebra.ofId _ _) c hcroot
  · intro χ hχ
    have key : χ.comp Θ.symm.toAlgHom = AdjoinRoot.liftAlgHom fu (Algebra.ofId _ _) c hcroot := by
      apply AdjoinRoot.algHom_ext
      refine Eq.trans ?_ (AdjoinRoot.liftAlgHom_root fu (Algebra.ofId _ _) c hcroot).symm
      change χ (Θ.symm (AdjoinRoot.root fu)) = c
      rw [← hΘT, Θ.symm_apply_apply, hχ]
    rw [← key]
    ext x
    change χ x = χ (Θ.symm (Θ x))
    rw [Θ.symm_apply_apply]

theorem algebraMap_germ (U : X.Opens) (x : X) (hx : x ∈ U) (s : Γ(X, U)) :
    algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ U x hx s) =
      @Scheme.germToFunctionField X _ U ⟨⟨x, hx⟩⟩ s

theorem appLE_eq_of_eq {Z Z' : Scheme.{u}} {f₁ f₂ : Z' ⟶ Z} (e : f₁ = f₂) (U : Z.Opens) (W :
  Z'.Opens)
    (h₁ : W ≤ f₁ ⁻¹ᵁ U) (h₂ : W ≤ f₂ ⁻¹ᵁ U) : f₁.appLE U W h₁ = f₂.appLE U W h₂

theorem appLE_top_top {Z Z' : Scheme.{u}} (f : Z' ⟶ Z) (e : (⊤ : Z'.Opens) ≤ f ⁻¹ᵁ ⊤) : f.appLE ⊤ ⊤
  e = f.appTop

theorem fromSpec_appLE_top {Y : Scheme.{u}} {U : Y.Opens} (hU : IsAffineOpen U) (e : (⊤ : (Spec
  Γ(Y, U)).Opens) ≤ hU.fromSpec ⁻¹ᵁ U) :
    hU.fromSpec.appLE U ⊤ e = (Scheme.ΓSpecIso Γ(Y, U)).inv

theorem eq_toSpecΓ_SpecMap_appLE_fromSpec {Z : Scheme.{u}} (z : Z ⟶ X) (V : X.Opens) (hV :
  IsAffineOpen V)
    (hz : z ⁻¹ᵁ V = ⊤) : z = Z.toSpecΓ ≫ Spec.map (z.appLE V ⊤ hz.ge) ≫ hV.fromSpec

theorem _root_.AlgebraicGeometry.existsUnique_lift_fromNormalization_kummer_of_isAffineOpen
    {X : Scheme.{u}} [IsIntegral X]
    (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x))
    (k : ℕ) (g : X.functionField)
    (V : X.Opens) (hV : IsAffineOpen V) (hVne : Nonempty V) (hk : IsUnit ((k : ℕ) : Γ(X, V)))
    (u : Γ(X, V)) (hu : IsUnit u) (h : X.functionField) (hh : h ≠ 0)
    (hval : ∀ (x : X) (hx : x ∈ V),
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ V x hx u) = g / h ^ k) :
    let A' := AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial X.functionField)
    let f₀ := Spec.map (CommRingCat.ofHom (algebraMap X.functionField A')) ≫ X.fromSpecStalk
      (genericPoint X)
    let π := f₀.fromNormalization
    let Y := f₀.normalization
    ∀ T : Γ(Y, π ⁻¹ᵁ V),
      f₀.toNormalization.app (π ⁻¹ᵁ V) T =
        (Spec (CommRingCat.of A')).presheaf.map (homOfLE le_top).op
          ((Scheme.ΓSpecIso (CommRingCat.of A')).inv (algebraMap X.functionField A' h⁻¹ *
            AdjoinRoot.root _)) →
      ∀ (Z : Scheme.{u}) (z : Z ⟶ X), z ⁻¹ᵁ V = ⊤ →
        ∀ τ : Γ(Z, ⊤), Z.presheaf.map (homOfLE le_top).op τ ^ k = z.app V u →
          ∃! s : Z ⟶ Y, s ≫ π = z ∧ s.app (π ⁻¹ᵁ V) T = Z.presheaf.map (homOfLE le_top).op τ := by
  intro A' f₀ π Y T hT Z z hz τ hτ
  have := hVne
  change ∃! s : Z ⟶ (fK k g).normalization, s ≫ (fK k g).fromNormalization = z ∧
      s.app ((fK k g).fromNormalization ⁻¹ᵁ V) T = Z.presheaf.map (homOfLE le_top).op τ
  have hT' : (fK k g).toNormalization.app ((fK k g).fromNormalization ⁻¹ᵁ V) T =
      (Spec (CommRingCat.of (KA k g))).presheaf.map (homOfLE le_top).op
        ((Scheme.ΓSpecIso (CommRingCat.of (KA k g))).inv (algebraMap X.functionField (KA k g) h⁻¹ *
          AdjoinRoot.root _)) := hT
  clear hT
  have hρ := yval_eq_of_toNormalization_app_eq k g V hV T _ hT'
  have huV : X.germToFunctionField V u = g / h ^ k := by
    obtain ⟨⟨x, hx⟩⟩ := hVne
    rw [← algebraMap_germ V x hx u]
    exact hval x hx
  let algC : Algebra Γ(X, V) Γ(Z, ⊤) := (z.appLE V ⊤ hz.ge).hom.toAlgebra
  have hτ' : τ ^ k = algebraMap Γ(X, V) Γ(Z, ⊤) u := by
    have h1 := congrArg (Z.presheaf.map (homOfLE hz.ge).op) hτ
    rw [map_pow, map_map _ _ (𝟙 _), op_id, CategoryTheory.Functor.map_id, CommRingCat.id_apply]
      at h1
    exact h1
  suffices lift : ∀ (Y₁ : Scheme.{u}) (π₁ : Y₁ ⟶ X)
      (hπV : IsAffineOpen (π₁ ⁻¹ᵁ V)) (T₁ : Γ(Y₁, π₁ ⁻¹ᵁ V)),
      (letI := (π₁.app V).hom.toAlgebra
       ∃! χ : Γ(Y₁, π₁ ⁻¹ᵁ V) →ₐ[Γ(X, V)] Γ(Z, ⊤), χ T₁ = τ) →
      ∃! s : Z ⟶ Y₁, s ≫ π₁ = z ∧
        s.app (π₁ ⁻¹ᵁ V) T₁ = Z.presheaf.map (homOfLE le_top).op τ by
    exact lift _ _ (hV.preimage _) T
      (existsUnique_algHom k g V hV hnorm hk u hu h hh huV T hρ Γ(Z, ⊤) τ hτ')
  intro Y₁ π₁ hπV T₁ hUP
  let algB₁ : Algebra Γ(X, V) Γ(Y₁, π₁ ⁻¹ᵁ V) := (π₁.app V).hom.toAlgebra
  obtain ⟨χ, hχT, hχuniq⟩ := hUP
  have hχA : ∀ a : Γ(X, V), χ (π₁.app V a) = z.appLE V ⊤ hz.ge a := fun a => χ.commutes a
  obtain ⟨φ, hφ⟩ : ∃ φ : Γ(Y₁, π₁ ⁻¹ᵁ V) ⟶ Γ(Z, ⊤),
      φ = CommRingCat.ofHom χ.toRingHom := ⟨_, rfl⟩
  have hφA : π₁.app V ≫ φ = z.appLE V ⊤ hz.ge := by
    rw [hφ]
    ext a
    exact hχA a
  have F1 : hπV.fromSpec ≫ π₁ = Spec.map (π₁.app V) ≫ hV.fromSpec := by
    rw [← IsAffineOpen.SpecMap_appLE_fromSpec π₁ hV hπV le_rfl, Scheme.Hom.appLE_eq_app]
  have F2 := eq_toSpecΓ_SpecMap_appLE_fromSpec z V hV hz
  have F3 : ∀ φ' : Γ(Y₁, π₁ ⁻¹ᵁ V) ⟶ Γ(Z, ⊤),
      (Z.toSpecΓ ≫ Spec.map φ').appTop = (Scheme.ΓSpecIso _).hom ≫ φ' := by
    intro φ'
    exact ΓSpec_adjunction_homEquiv_eq φ'
  have e₂ : (⊤ : (Spec Γ(Y₁, π₁ ⁻¹ᵁ V)).Opens) ≤
      hπV.fromSpec ⁻¹ᵁ (π₁ ⁻¹ᵁ V) := by rw [IsAffineOpen.fromSpec_preimage_self]
  have F4 : ∀ (t : Z ⟶ Spec Γ(Y₁, π₁ ⁻¹ᵁ V))
      (e : (⊤ : Z.Opens) ≤ (t ≫ hπV.fromSpec) ⁻¹ᵁ (π₁ ⁻¹ᵁ V)),
      (t ≫ hπV.fromSpec).appLE (π₁ ⁻¹ᵁ V) ⊤ e = (Scheme.ΓSpecIso _).inv ≫ t.appTop := by
    intro t e
    rw [← Scheme.Hom.appLE_comp_appLE t hπV.fromSpec (π₁ ⁻¹ᵁ V) ⊤ ⊤ e₂ le_top,
      fromSpec_appLE_top hπV e₂]
    exact congrArg (fun f => (Scheme.ΓSpecIso _).inv ≫ f) (appLE_top_top t le_top)
  have hcomp : ((Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec) ≫ π₁ = z := by
    rw [Category.assoc, Category.assoc, F1, ← Spec.map_comp_assoc, hφA, ← F2]
  refine ⟨(Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec, ⟨hcomp, ?_⟩, ?_⟩
  · have e : (⊤ : Z.Opens) ≤ ((Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec) ⁻¹ᵁ (π₁ ⁻¹ᵁ V) := by
      rw [← Scheme.Hom.comp_preimage, hcomp, hz]
    have happLE : ((Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec).appLE (π₁ ⁻¹ᵁ V) ⊤ e = φ := by
      rw [F4, F3, Iso.inv_hom_id_assoc]
    have hval : ((Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec).appLE (π₁ ⁻¹ᵁ V) ⊤ e T₁ = τ := by
      rw [happLE, hφ]
      exact hχT
    rw [Scheme.Hom.appLE, CommRingCat.comp_apply] at hval
    have h2 := congrArg (Z.presheaf.map (homOfLE (le_top :
      ((Z.toSpecΓ ≫ Spec.map φ) ≫ hπV.fromSpec) ⁻¹ᵁ (π₁ ⁻¹ᵁ V) ≤ ⊤)).op) hval
    rw [map_map _ _ (𝟙 _), op_id, CategoryTheory.Functor.map_id, CommRingCat.id_apply] at h2
    exact h2
  · rintro s' ⟨h1', h2'⟩
    have hrange : Set.range s' ⊆ Set.range hπV.fromSpec := by
      rw [IsAffineOpen.range_fromSpec]
      rintro _ ⟨x, rfl⟩
      change π₁ (s' x) ∈ V
      rw [← Scheme.Hom.comp_apply, h1']
      have : x ∈ z ⁻¹ᵁ V := by rw [hz]; trivial
      exact this
    obtain ⟨t', ht'⟩ : ∃ t' : Z ⟶ Spec Γ(Y₁, π₁ ⁻¹ᵁ V),
        t' ≫ hπV.fromSpec = s' :=
      ⟨IsOpenImmersion.lift hπV.fromSpec s' hrange, IsOpenImmersion.lift_fac _ _ _⟩
    obtain ⟨φ', hφ'def⟩ : ∃ φ' : Γ(Y₁, π₁ ⁻¹ᵁ V) ⟶ Γ(Z, ⊤),
        φ' = (Scheme.ΓSpecIso _).inv ≫ t'.appTop := ⟨_, rfl⟩
    have e' : (⊤ : Z.Opens) ≤ s' ⁻¹ᵁ (π₁ ⁻¹ᵁ V) := by
      rw [← Scheme.Hom.comp_preimage, h1', hz]
    have hs'appLE : s'.appLE (π₁ ⁻¹ᵁ V) ⊤ e' = φ' := by
      rw [hφ'def, ← F4 t' (by rw [ht']; exact e')]
      exact appLE_eq_of_eq ht'.symm _ _ _ _
    have hφ'A : ∀ a : Γ(X, V), φ' (π₁.app V a) = z.appLE V ⊤ hz.ge a := by
      intro a
      rw [← hs'appLE]
      have heq := (Scheme.Hom.comp_appLE s' π₁ V ⊤ e').symm.trans
        (appLE_eq_of_eq h1' V ⊤ e' hz.ge)
      exact CategoryTheory.ConcreteCategory.congr_hom heq a
    have hφ'T₁ : φ' T₁ = τ := by
      rw [← hs'appLE, Scheme.Hom.appLE, CommRingCat.comp_apply, h2', map_map _ _ (𝟙 _), op_id,
        CategoryTheory.Functor.map_id, CommRingCat.id_apply]
    let χ' : Γ(Y₁, π₁ ⁻¹ᵁ V) →ₐ[Γ(X, V)] Γ(Z, ⊤) :=
      { φ'.hom with commutes' := fun a => hφ'A a }
    have hχ' : χ' = χ := hχuniq χ' hφ'T₁
    have hφφ' : φ' = φ := by
      rw [hφ]
      ext x
      change χ' x = χ x
      rw [hχ']
    have ht'eq : t' = Z.toSpecΓ ≫ Spec.map φ := by
      apply ext_of_isAffine
      rw [F3, ← hφφ', hφ'def, Iso.hom_inv_id_assoc]
    rw [← ht', ht'eq]