Scheme_isAffineOpen_and_exists_linearEquiv_tensor_sections_of_isPullback.lean

theorem appLE_congr_hom {X Y : Scheme.{u}} {f g : X ⟶ Y} (hfg : f = g) (U : Y.Opens) (V : X.Opens)
    (h : V ≤ f ⁻¹ᵁ U) (h' : V ≤ g ⁻¹ᵁ U) : f.appLE U V h = g.appLE U V h'

theorem appLE_self_of_eq_id {X : Scheme.{u}} {k : X ⟶ X} (hk : k = 𝟙 X) (W : X.Opens)
    (h : W ≤ k ⁻¹ᵁ W) : k.appLE W W h = 𝟙 _

theorem appLE_comp_appLE_eq_id {P Q : Scheme.{u}} (f : P ⟶ Q) (g : Q ⟶ P) (hfg : f ≫ g = 𝟙 P)
    (W : P.Opens) (W' : Q.Opens) (h₁ : W' ≤ g ⁻¹ᵁ W) (h₂ : W ≤ f ⁻¹ᵁ W') :
    g.appLE W W' h₁ ≫ f.appLE W' W h₂ = 𝟙 _

theorem appLE_appLE_apply {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (k : X ⟶ Z) (hk : f ≫ g = k)
    (U : Z.Opens) (V : Y.Opens) (W : X.Opens) (e₁ : V ≤ g ⁻¹ᵁ U) (e₂ : W ≤ f ⁻¹ᵁ V)
    (e₃ : W ≤ k ⁻¹ᵁ U) (x : Γ(Z, U)) :
    (f.appLE V W e₂).hom ((g.appLE U V e₁).hom x) = (k.appLE U W e₃).hom x

def sectionsIso {P Q : Scheme.{u}} (e : P ≅ Q) (W : P.Opens) (W' : Q.Opens)
    (hW : W = e.hom ⁻¹ᵁ W') : Γ(Q, W') ≅ Γ(P, W) where
  hom := e.hom.appLE W' W hW.le
  inv := e.inv.appLE W W' (by
    rw [hW, ← Scheme.Hom.comp_preimage, e.inv_hom_id]; exact le_rfl)
  hom_inv_id := appLE_comp_appLE_eq_id e.inv e.hom e.inv_hom_id W' W _ _
  inv_hom_id := appLE_comp_appLE_eq_id e.hom e.inv e.hom_inv_id W W' _ _

theorem transport {R : Type u} [CommRing R] {P Q : Scheme.{u}} (e : P ≅ Q)
    (W : P.Opens) (W' : Q.Opens) (hW : W = e.hom ⁻¹ᵁ W')
    [iQ : Algebra R Γ(Q, W')] [iP : Algebra R Γ(P, W)]
    (halg : ∀ r : R, (e.hom.appLE W' W hW.le).hom (algebraMap R Γ(Q, W') r) = algebraMap R Γ(P, W)
      r) :
    ∃ σ : Γ(Q, W') ≃ₐ[R] Γ(P, W), ∀ x, σ x = (e.hom.appLE W' W hW.le).hom x

theorem
  _root_.AlgebraicGeometry.Scheme.isAffineOpen_and_exists_linearEquiv_tensor_sections_of_isPullback
    {R : Type u} [CommRing R] {X Y P : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of R)) (fY : Y ⟶ Spec (CommRingCat.of R))
    (p₁ : P ⟶ X) (p₂ : P ⟶ Y) (hP : IsPullback p₁ p₂ fX fY)
    (U : X.Opens) (hU : IsAffineOpen U) (V : Y.Opens) (hV : IsAffineOpen V) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom fX U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom fY V
    letI := Scheme.TwoAffineOpenCover.algebraOfHom (p₁ ≫ fX) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V)
    IsAffineOpen (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) ∧
    ∃ Φ : Γ(X, U) ⊗[R] Γ(Y, V) ≃ₗ[R] Γ(P, p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V),
      ∀ (a : Γ(X, U)) (b : Γ(Y, V)), Φ (a ⊗ₜ[R] b) =
        (p₁.appLE U (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) inf_le_left).hom a *
          (p₂.appLE V (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) inf_le_right).hom b := by
  let iU := Scheme.TwoAffineOpenCover.algebraOfHom fX U
  let iV := Scheme.TwoAffineOpenCover.algebraOfHom fY V
  let iW := Scheme.TwoAffineOpenCover.algebraOfHom (p₁ ≫ fX) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V)
  let iW' := Scheme.TwoAffineOpenCover.algebraOfHom (pullback.fst fX fY ≫ fX) (pullback.fst fX fY
    ⁻¹ᵁ U ⊓ pullback.snd fX fY ⁻¹ᵁ V)
  have h60 := isAffineOpen_and_exists_algEquiv_tensor_sections_fst_preimage_inf_snd_preimage
    fX fY U hU V hV
  obtain ⟨hW'aff, e₀, he₀⟩ := h60
  have he₁ : hP.isoPullback.hom ≫ pullback.fst fX fY = p₁ := hP.isoPullback_hom_fst
  have he₂ : hP.isoPullback.hom ≫ pullback.snd fX fY = p₂ := hP.isoPullback_hom_snd
  have hW : (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) = hP.isoPullback.hom ⁻¹ᵁ (pullback.fst fX fY ⁻¹ᵁ U ⊓ pullback.snd
    fX fY ⁻¹ᵁ V) := by
    rw [Scheme.Hom.preimage_inf, ← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, he₁, he₂]
  refine ⟨?_, ?_⟩
  · rw [hW]; exact hW'aff.preimage_of_isIso _
  have he₁' : hP.isoPullback.hom ≫ (pullback.fst fX fY ≫ fX) = p₁ ≫ fX := by
    rw [← Category.assoc, he₁]
  have hσ := E163G5A.transport (R := R) hP.isoPullback (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) (pullback.fst fX fY
    ⁻¹ᵁ U ⊓ pullback.snd fX fY ⁻¹ᵁ V) hW
    (iQ := Scheme.TwoAffineOpenCover.algebraOfHom (pullback.fst fX fY ≫ fX) (pullback.fst fX fY ⁻¹ᵁ
      U ⊓ pullback.snd fX fY ⁻¹ᵁ V))
    (iP := Scheme.TwoAffineOpenCover.algebraOfHom (p₁ ≫ fX) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V))
    (fun r => E163G5A.appLE_appLE_apply hP.isoPullback.hom (pullback.fst fX fY ≫ fX) (p₁ ≫ fX) he₁'
      ⊤ (pullback.fst fX fY ⁻¹ᵁ U ⊓ pullback.snd fX fY ⁻¹ᵁ V) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) le_top hW.le
        le_top ((Scheme.ΓSpecIso (.of R)).inv.hom r))
  obtain ⟨σ, hσ⟩ := hσ
  refine ⟨(e₀.trans σ).toLinearEquiv, fun a b => ?_⟩
  have h1 := E163G5A.appLE_appLE_apply hP.isoPullback.hom (pullback.fst fX fY) p₁ he₁
      U (pullback.fst fX fY ⁻¹ᵁ U ⊓ pullback.snd fX fY ⁻¹ᵁ V) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) inf_le_left
        hW.le inf_le_left a
  have h2 := E163G5A.appLE_appLE_apply hP.isoPullback.hom (pullback.snd fX fY) p₂ he₂
      V (pullback.fst fX fY ⁻¹ᵁ U ⊓ pullback.snd fX fY ⁻¹ᵁ V) (p₁ ⁻¹ᵁ U ⊓ p₂ ⁻¹ᵁ V) inf_le_right
        hW.le inf_le_right b
  rw [AlgEquiv.toLinearEquiv_apply, AlgEquiv.trans_apply, hσ, he₀ a b, map_mul, h1, h2]