Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case intro
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
c : Cone F :=
  (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)).mapCone
    (Under.liftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX))
this : PreservesFiniteLimits (Under.pushout (Scheme.Hom.appLE f US UT hUST))
val✝ : Fintype ι
hc : IsLimit c :=
  isLimitOfPreserves (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT))
    (Under.isLimitLiftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX) ⋯.some)
c'₀ : Cocone (D ⋙ G) := (colimit.cocone (D ⋙ G)).extend (eqToIso ⋯).hom
c' : Cone (D.op ⋙ G.op ⋙ Y.presheaf) := Functor.mapCone Y.presheaf c'₀.op
hc' : IsLimit c' :=
  (IsLimit.postcomposeHomEquiv
      (Functor.isoWhiskerRight
        (NatIso.op
          (NatIso.ofComponents
              (fun x ↦
                match x with
                | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                | Pairwise.pair i j => eqToIso ⋯)
              ⋯).symm)
        Y.presheaf)
      c')
    (⋯.some.ofIsoLimit
      (Cone.ext
        (Iso.refl
          (Functor.mapCone Y.presheaf
              ((Cocone.precompose
                      (NatIso.ofComponents
                          (fun x ↦
                            match x with
                            | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                            | Pairwise.pair i j => eqToIso ⋯)
                          ⋯).inv).obj
                  c'₀).op).pt)
        ⋯))
HαF₂ : ∀ (i j : ι), Mono (αF.app (op (Pairwise.pair i j)))
f₁ : c.pt ⟶ c'.pt := hc'.lift ((Cone.postcompose αF).obj c)
f₂ : c'.pt ⟶ c.pt :=
  hc.lift
    { pt := c'.pt,
      π :=
        {
          app := fun x ↦
            match x with
            | op (Pairwise.single i) => c'.π.app (op (Pairwise.single i)) ≫ inv (αF.app (op (Pairwise.single i)))
            | op (Pairwise.pair i j) =>
              c'.π.app (op (Pairwise.single i)) ≫
                inv (αF.app (op (Pairwise.single i))) ≫ F.map (Quiver.Hom.op (Pairwise.Hom.left i j)),
          naturality := ⋯ } }
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
let e : c.pt ≅ c'.pt := by
    refine ⟨f₁, f₂, hc.hom_ext ?_, hc'.hom_ext ?_⟩
    · rintro ⟨i | ⟨i, j⟩⟩ <;> simp [f₁, f₂]
    · rintro ⟨i | ⟨i, j⟩⟩
      · simp [f₁, f₂]
      · simpa [f₁, f₂] using c'.w (Quiver.Hom.op <| Pairwise.Hom.left i j)

Goal state after:
case intro
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
c : Cone F :=
  (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)).mapCone
    (Under.liftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX))
this : PreservesFiniteLimits (Under.pushout (Scheme.Hom.appLE f US UT hUST))
val✝ : Fintype ι
hc : IsLimit c :=
  isLimitOfPreserves (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT))
    (Under.isLimitLiftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX) ⋯.some)
c'₀ : Cocone (D ⋙ G) := (colimit.cocone (D ⋙ G)).extend (eqToIso ⋯).hom
c' : Cone (D.op ⋙ G.op ⋙ Y.presheaf) := Functor.mapCone Y.presheaf c'₀.op
hc' : IsLimit c' :=
  (IsLimit.postcomposeHomEquiv
      (Functor.isoWhiskerRight
        (NatIso.op
          (NatIso.ofComponents
              (fun x ↦
                match x with
                | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                | Pairwise.pair i j => eqToIso ⋯)
              ⋯).symm)
        Y.presheaf)
      c')
    (⋯.some.ofIsoLimit
      (Cone.ext
        (Iso.refl
          (Functor.mapCone Y.presheaf
              ((Cocone.precompose
                      (NatIso.ofComponents
                          (fun x ↦
                            match x with
                            | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                            | Pairwise.pair i j => eqToIso ⋯)
                          ⋯).inv).obj
                  c'₀).op).pt)
        ⋯))
HαF₂ : ∀ (i j : ι), Mono (αF.app (op (Pairwise.pair i j)))
f₁ : c.pt ⟶ c'.pt := hc'.lift ((Cone.postcompose αF).obj c)
f₂ : c'.pt ⟶ c.pt :=
  hc.lift
    { pt := c'.pt,
      π :=
        {
          app := fun x ↦
            match x with
            | op (Pairwise.single i) => c'.π.app (op (Pairwise.single i)) ≫ inv (αF.app (op (Pairwise.single i)))
            | op (Pairwise.pair i j) =>
              c'.π.app (op (Pairwise.single i)) ≫
                inv (αF.app (op (Pairwise.single i))) ≫ F.map (Quiver.Hom.op (Pairwise.Hom.left i j)),
          naturality := ⋯ } }
e : c.pt ≅ c'.pt := { hom := f₁, inv := f₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }
⊢ IsIso (pushoutSection H hUST hUSX hUY)