IsPullback_exists_iso_Spec_quotient_comp_morphismRestrict_eq.lean

def tau (π : T' →+* T) (hπ : Function.Surjective π) (φ : T' →+* C) :
    T →+* C ⧸ (RingHom.ker π).map φ

theorem tau_apply (π : T' →+* T) (hπ : Function.Surjective π) (φ : T' →+* C) (k : T') :
    tau π hπ φ (π k) = Ideal.Quotient.mk _ (φ k)

theorem tau_comp (π : T' →+* T) (hπ : Function.Surjective π) (φ : T' →+* C) :
    (tau π hπ φ).comp π = (Ideal.Quotient.mk ((RingHom.ker π).map φ)).comp φ

theorem isPushout_quotient (π : T' →+* T) (hπ : Function.Surjective π) (φ : T' →+* C) :
    IsPushout (CommRingCat.ofHom φ) (CommRingCat.ofHom π)
      (CommRingCat.ofHom (Ideal.Quotient.mk ((RingHom.ker π).map φ))) (CommRingCat.ofHom (tau π hπ
        φ))

theorem isNilpotent_map {T' C : Type u} [CommRing T'] [CommRing C] (φ : T' →+* C) {K : Ideal T'}
    (hK : IsNilpotent K) : IsNilpotent (K.map φ)

theorem _root_.AlgebraicGeometry.IsPullback.exists_iso_Spec_quotient_comp_morphismRestrict_eq
    {T' T : Type u} [CommRing T'] [CommRing T] (π : T' →+* T) (hπ : Function.Surjective π)
    (hker : IsNilpotent (RingHom.ker π))
    {P P₀ : Scheme.{u}} (p : P ⟶ Spec (CommRingCat.of T')) (p₀ : P₀ ⟶ Spec (CommRingCat.of T))
    (G : P₀ ⟶ P) (hG : IsPullback G p₀ p (Spec.map (CommRingCat.ofHom π)))
    (D : P.Opens) (hD : IsAffineOpen D) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom p D
    IsNilpotent ((RingHom.ker π).map (algebraMap T' Γ(P, D))) ∧
    ∃ ε : Spec (CommRingCat.of (Γ(P, D) ⧸ (RingHom.ker π).map (algebraMap T' Γ(P, D)))) ≅ ↑(G ⁻¹ᵁ
      D),
      ε.hom ≫ G ∣_ D ≫ hD.isoSpec.hom =
        Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ((RingHom.ker π).map (algebraMap T' Γ(P,
          D))))) := by
  let inst := Scheme.TwoAffineOpenCover.algebraOfHom p D
  refine ⟨E163TC.isNilpotent_map _ hker, ?_⟩
  have hφ : CommRingCat.ofHom (algebraMap T' Γ(P, D)) =
      (Scheme.ΓSpecIso (.of T')).inv ≫ p.appLE ⊤ D le_top := rfl
  have hDp : hD.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap T' Γ(P, D))) = (D.ι ≫ p) ≫ 𝟙
    _ := by
    rw [Category.comp_id, hφ, Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ← IsAffineOpen.fromSpec_top,
      IsAffineOpen.SpecMap_appLE_fromSpec p (isAffineOpen_top _) hD le_top,
        IsAffineOpen.isoSpec_hom,
      IsAffineOpen.toSpecΓ_fromSpec_assoc]
  have sq1 : IsPullback (G ∣_ D) ((G ⁻¹ᵁ D).ι ≫ p₀) (D.ι ≫ p) (Spec.map (CommRingCat.ofHom π)) :=
    (isPullback_morphismRestrict G D).paste_vert hG
  have sq2 : IsPullback hD.isoSpec.hom (D.ι ≫ p) (Spec.map (CommRingCat.ofHom (algebraMap T' Γ(P,
    D))))
      (𝟙 _) := IsPullback.of_horiz_isIso ⟨hDp⟩
  have sq3 := sq1.paste_horiz sq2
  rw [Category.comp_id] at sq3
  have sq4 := isPullback_SpecMap_of_isPushout _ _ _ _
    (E163TC.isPushout_quotient π hπ (algebraMap T' Γ(P, D)))
  exact ⟨sq4.isoIsPullback _ _ sq3,
    by rw [← Category.assoc]; exact sq4.isoIsPullback_hom_fst _ _ sq3⟩