exists_algEquiv_sections_pullback_fst_preimage_tensor_of_isAffineOpen.lean

theorem
  _root_.AlgebraicGeometry.exists_algEquiv_sections_pullback_fst_preimage_tensor_of_isAffineOpen
    (K : Type u) [CommRing K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
    (H : Type u) [CommRing H] [Algebra K H] :
    letI _instK : ∀ V : A.Opens, Algebra K Γ(A, V) := fun V =>
      Scheme.TwoAffineOpenCover.algebraOfHom f V
    letI _instKP : ∀ W : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap K H)))).Opens,
        Algebra K Γ(pullback f (Spec.map (CommRingCat.ofHom (algebraMap K H))), W) := fun W =>
      Scheme.TwoAffineOpenCover.algebraOfHom (pullback.fst f (Spec.map (CommRingCat.ofHom
        (algebraMap K H))) ≫ f) W
    ∃ ε : ∀ (V : A.Opens) (_ : IsAffineOpen V),
        Γ(pullback f (Spec.map (CommRingCat.ofHom (algebraMap K H))),
            (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K H)))) ⁻¹ᵁ V) ≃ₐ[K] Γ(A, V)
              ⊗[K] H,
      (∀ (V : A.Opens) (_ : IsAffineOpen V),
          IsAffineOpen ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K H)))) ⁻¹ᵁ V)) ∧
      (∀ (V : A.Opens) (hV : IsAffineOpen V) (a : Γ(A, V)),
          ε V hV (((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K H)))).app V).hom a) =
            a ⊗ₜ[K] (1 : H)) ∧
      (∀ (V : A.Opens) (hV : IsAffineOpen V) (h : H),
          ε V hV (((pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap K H)))).appLE ⊤
              ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K H)))) ⁻¹ᵁ V) le_top).hom
            ((Scheme.ΓSpecIso (CommRingCat.of H)).inv.hom h)) = (1 : Γ(A, V)) ⊗ₜ[K] h) ∧
      (∀ (V V' : A.Opens) (hV : IsAffineOpen V) (hV' : IsAffineOpen V') (hle : V' ≤ V)
          (s : Γ(pullback f (Spec.map (CommRingCat.ofHom (algebraMap K H))),
            (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K H)))) ⁻¹ᵁ V)),
          Algebra.TensorProduct.map (Scheme.TwoAffineOpenCover.restrictAlgHom f hle) (AlgHom.id K
            H) (ε V hV s) =
            ε V' hV' (((pullback f (Spec.map (CommRingCat.ofHom (algebraMap K H)))).presheaf.map
              (homOfLE ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap K
                H)))).preimage_mono hle)).op).hom s)) := by
  let SKH := Spec.map (CommRingCat.ofHom (algebraMap K H))
  let P := pullback f SKH
  let p₁ := pullback.fst f SKH
  let p₂ := pullback.snd f SKH
  let instK : ∀ V : A.Opens, Algebra K Γ(A, V) := fun V => Scheme.TwoAffineOpenCover.algebraOfHom f
    V
  let instKP : ∀ W : P.Opens, Algebra K Γ(P, W) := fun W => Scheme.TwoAffineOpenCover.algebraOfHom
    (p₁ ≫ f) W
  let instHP : ∀ W : P.Opens, Algebra H Γ(P, W) := fun W => Scheme.TwoAffineOpenCover.algebraOfHom
    p₂ W
  have towerP : ∀ W : P.Opens, IsScalarTower K H Γ(P, W) := by
    intro W
    refine IsScalarTower.of_algebraMap_eq fun k => ?_
    change ((p₁ ≫ f).appLE ⊤ W le_top).hom ((Scheme.ΓSpecIso (.of K)).inv.hom k) =
      (p₂.appLE ⊤ W le_top).hom ((Scheme.ΓSpecIso (.of H)).inv.hom (algebraMap K H k))
    have h1 : (p₁ ≫ f).appLE ⊤ W le_top = (p₂ ≫ SKH).appLE ⊤ W le_top := by
      simp only [p₁, p₂, pullback.condition]
    rw [h1, ← Scheme.Hom.appLE_comp_appLE p₂ SKH ⊤ ⊤ W le_top le_top]
    change (p₂.appLE ⊤ W le_top).hom ((SKH.appLE ⊤ ⊤ le_top).hom ((Scheme.ΓSpecIso (.of K)).inv.hom
      k)) = _
    congr 1
    have h2 := Scheme.ΓSpecIso_inv_naturality (CommRingCat.ofHom (algebraMap K H))
    have h3 : SKH.appLE ⊤ ⊤ le_top = SKH.appTop := by
      rw [Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]
      rfl
    rw [h3]
    exact (congrArg (fun φ => φ.hom k) h2).symm
  have key : ∀ (V : A.Opens) (hV : IsAffineOpen V),
      ∃ ε : Γ(P, p₁ ⁻¹ᵁ V) ≃ₐ[K] Γ(A, V) ⊗[K] H,
        (∀ a : Γ(A, V), ε ((p₁.app V).hom a) = a ⊗ₜ[K] (1 : H)) ∧
        (∀ h : H, ε ((p₂.appLE ⊤ (p₁ ⁻¹ᵁ V) le_top).hom ((Scheme.ΓSpecIso (.of H)).inv.hom h)) = (1
          : Γ(A, V)) ⊗ₜ[K] h) := by
    intro V hV
    obtain ⟨e, he⟩ := Scheme.exists_algEquiv_tensor_sections_pullback_fst_preimage_of_isAffineOpen
      f V hV H
    let ε : Γ(P, p₁ ⁻¹ᵁ V) ≃ₐ[K] Γ(A, V) ⊗[K] H :=
      ((e.restrictScalars K).symm).trans (Algebra.TensorProduct.comm K H Γ(A, V))
    refine ⟨ε, fun a => ?_, fun h => ?_⟩
    · change Algebra.TensorProduct.comm K H Γ(A, V) (e.symm ((p₁.app V).hom a)) = a ⊗ₜ[K] 1
      rw [← he a, e.symm_apply_apply, Algebra.TensorProduct.comm_tmul]
    · change Algebra.TensorProduct.comm K H Γ(A, V) (e.symm (algebraMap H Γ(P, p₁ ⁻¹ᵁ V) h)) = 1
        ⊗ₜ[K] h
      rw [AlgEquiv.commutes, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
        RingHom.id_apply,
        Algebra.TensorProduct.comm_tmul]
  choose ε hε₁ hε₂ using key
  have : IsAffineHom p₁ := Scheme.TwoAffineOpenCover.isAffineHom_fst f H
  refine ⟨ε, fun V hV => hV.preimage p₁, fun V hV a => hε₁ V hV a, fun V hV h => hε₂ V hV h, ?_⟩
  intro V V' hV hV' hle s
  obtain ⟨t, rfl⟩ := (ε V hV).symm.surjective s
  rw [AlgEquiv.apply_symm_apply]
  let F₁ : Γ(A, V) ⊗[K] H →ₐ[K] Γ(A, V') ⊗[K] H :=
    Algebra.TensorProduct.map (Scheme.TwoAffineOpenCover.restrictAlgHom f hle) (AlgHom.id K H)
  let res : Γ(P, p₁ ⁻¹ᵁ V) →ₐ[K] Γ(P, p₁ ⁻¹ᵁ V') := Scheme.TwoAffineOpenCover.restrictAlgHom (p₁ ≫
    f) (p₁.preimage_mono hle)
  let F₂ : Γ(A, V) ⊗[K] H →ₐ[K] Γ(A, V') ⊗[K] H :=
    ((ε V' hV').toAlgHom.comp res).comp (ε V hV).symm.toAlgHom
  have hF : F₁ = F₂ := by
    apply Algebra.TensorProduct.ext'
    intro a h
    change Algebra.TensorProduct.map _ _ (a ⊗ₜ[K] h) = ε V' hV' (res ((ε V hV).symm (a ⊗ₜ[K] h)))
    rw [Algebra.TensorProduct.map_tmul, AlgHom.id_apply]
    have hsplit : a ⊗ₜ[K] h = (a ⊗ₜ[K] (1 : H)) * ((1 : Γ(A, V)) ⊗ₜ[K] h) := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    rw [hsplit, ← hε₁ V hV a, ← hε₂ V hV h, ← map_mul, AlgEquiv.symm_apply_apply, map_mul, map_mul]
    have hr₁ : res ((p₁.app V).hom a) = (p₁.app V').hom ((A.presheaf.map (homOfLE hle).op).hom a)
      := by
      change (p₁.appLE V (p₁ ⁻¹ᵁ V') (p₁.preimage_mono hle)).hom a = (A.presheaf.map (homOfLE
        hle).op ≫ p₁.app V').hom a
      rw [Scheme.Hom.app_eq_appLE p₁ (U := V'), Scheme.Hom.map_appLE]
    have hr₂ : res ((p₂.appLE ⊤ (p₁ ⁻¹ᵁ V) le_top).hom ((Scheme.ΓSpecIso (.of H)).inv.hom h)) =
        (p₂.appLE ⊤ (p₁ ⁻¹ᵁ V') le_top).hom ((Scheme.ΓSpecIso (.of H)).inv.hom h) := by
      change (P.presheaf.map (homOfLE (p₁.preimage_mono hle)).op).hom ((p₂.appLE ⊤ (p₁ ⁻¹ᵁ V)
        le_top).hom _) = _
      rw [← CommRingCat.comp_apply]
      erw [Scheme.Hom.appLE_map]
    rw [hr₁, hr₂, hε₁ V' hV', hε₂ V' hV', Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    rfl
  exact congrArg (fun F : Γ(A, V) ⊗[K] H →ₐ[K] Γ(A, V') ⊗[K] H => F t) hF