PullbackSectionsPushout.lean

theorem Scheme.Hom.isAffineOpen_preimage_and_isPushout_of_isPullback_aux
    {A : Type u} [CommRing A] {Y : Scheme.{u}} (gY : Y ⟶ Spec (CommRingCat.of A)) (U : Y.Opens) :
    (U.ι ≫ gY).appTop ≫ U.topIso.hom = gY.appLE ⊤ U le_top

theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_preimage_and_isPushout_of_isPullback
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
    {X Y : Scheme.{u}} (gY : Y ⟶ Spec (CommRingCat.of A)) (gX : X ⟶ Spec (CommRingCat.of B))
    (φ : X ⟶ Y) (hφ : IsPullback φ gX gY (Spec.map (CommRingCat.ofHom (algebraMap A B))))
    (U : Y.Opens) (hU : IsAffineOpen U) :
    IsAffineOpen (φ ⁻¹ᵁ U) ∧
      letI := gY.sectionsAlgebra U; letI := gX.sectionsAlgebra (φ ⁻¹ᵁ U)
      letI : Algebra Γ(Y, U) Γ(X, φ ⁻¹ᵁ U) := (φ.appLE U (φ ⁻¹ᵁ U) le_rfl).hom.toAlgebra
      ∀ [Algebra A Γ(X, φ ⁻¹ᵁ U)] [IsScalarTower A B Γ(X, φ ⁻¹ᵁ U)]
        [IsScalarTower A Γ(Y, U) Γ(X, φ ⁻¹ᵁ U)],
        Algebra.IsPushout A B Γ(Y, U) Γ(X, φ ⁻¹ᵁ U) := by
  have hbc : MorphismProperty.IsStableUnderBaseChange
      (fun {X Y : Scheme.{u}} (h : X ⟶ Y) => IsAffineHom h) :=
    isAffineHom_isStableUnderBaseChange
  have : IsAffineHom φ := hbc.of_isPullback hφ.flip inferInstance
  have hV : IsAffineOpen (φ ⁻¹ᵁ U) := hU.preimage φ
  refine ⟨hV, ?_⟩
  intro algA ist₁ ist₂
  have sq : IsPullback (φ ∣_ U) ((φ ⁻¹ᵁ U).ι ≫ gX) (U.ι ≫ gY)
      (Spec.map (CommRingCat.ofHom (algebraMap A B))) :=
    (isPullback_morphismRestrict φ U).paste_vert hφ
  let _ : IsAffine U := hU
  let _ : IsAffine (φ ⁻¹ᵁ U) := hV
  have H := isPushout_appTop_of_isPullback sq.flip
  let _ := gY.sectionsAlgebra U
  let _ := gX.sectionsAlgebra (φ ⁻¹ᵁ U)
  let _ : Algebra Γ(Y, U) Γ(X, φ ⁻¹ᵁ U) := (φ.appLE U (φ ⁻¹ᵁ U) le_rfl).hom.toAlgebra
  refine (CommRingCat.isPushout_iff_isPushout (R := A) (R' := B) (S := Γ(Y, U))
    (S' := Γ(X, φ ⁻¹ᵁ U))).mp ?_
  have e₁ : CommRingCat.ofHom (algebraMap A Γ(Y, U)) =
      (Scheme.ΓSpecIso (.of A)).inv ≫ gY.appLE ⊤ U le_top := rfl
  have e₂ : CommRingCat.ofHom (algebraMap B Γ(X, φ ⁻¹ᵁ U)) =
      (Scheme.ΓSpecIso (.of B)).inv ≫ gX.appLE ⊤ (φ ⁻¹ᵁ U) le_top := rfl
  have e₃ : CommRingCat.ofHom (algebraMap Γ(Y, U) Γ(X, φ ⁻¹ᵁ U)) =
      φ.appLE U (φ ⁻¹ᵁ U) le_rfl := rfl
  refine H.of_iso (Scheme.ΓSpecIso (.of A)) (Scheme.ΓSpecIso (.of B)) U.topIso (φ ⁻¹ᵁ U).topIso
    ?_ ?_ ?_ ?_
  · exact Scheme.ΓSpecIso_naturality _
  · rw [e₁, Iso.hom_inv_id_assoc]
    exact AlgebraicGeometry.Scheme.Hom.isAffineOpen_preimage_and_isPushout_of_isPullback_aux gY U
  · rw [e₂, Iso.hom_inv_id_assoc]
    exact AlgebraicGeometry.Scheme.Hom.isAffineOpen_preimage_and_isPushout_of_isPullback_aux gX (φ
      ⁻¹ᵁ U)
  · rw [e₃, ← Scheme.Hom.resLE_eq_morphismRestrict, Scheme.Hom.appTop, Scheme.Hom.resLE_app_top,
      Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]