FiniteCoequalizers.lean

def AlgHom.AreSplit (f g : A →ₐ[R] B) : Prop

def finULiftPiAlgEquiv (R : Type u) [CommRing R] (n : ℕ) :
    (Fin n → R) ≃ₐ[R] (ULift.{u, 0} (Fin n) → R)

lemma liftFinSplitEq {A B : Type u} [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (n m : ℕ)
    (eA : A ≃ₐ[R] (Fin n → R)) (eB : B ≃ₐ[R] (Fin m → R))
    (sigma : Fin m → Fin n)
    (h : eB.toAlgHom.comp f =
      (AlgHom.compRight R R sigma).comp eA.toAlgHom) :
    let eA' := eA.trans (finULiftPiAlgEquiv R n)
    let eB' := eB.trans (finULiftPiAlgEquiv R m)
    let sigma' : ULift.{u, 0} (Fin m) → ULift.{u, 0} (Fin n) :=
      fun i ↦ ULift.up (sigma i.down)
    eB'.toAlgHom.comp f =
      (AlgHom.compRight R R sigma').comp eA'.toAlgHom := by
  dsimp only
  ext x i
  have hx := DFunLike.congr_fun h x
  exact congrFun hx i.down

lemma AlgHom.AreSplit.iff_of_isScalarTower
    (T : Type u) [CommRing T] [Algebra R T] [Algebra S T]
    [IsScalarTower R S T] (f g : A →ₐ[R] B) :
    (AlgHom.AreSplit
      (Algebra.TensorProduct.map (.id T T) f)
      (Algebra.TensorProduct.map (.id T T) g)) ↔
    (AlgHom.AreSplit
      (Algebra.TensorProduct.map (.id T T)
        (Algebra.TensorProduct.map (.id S S) f))
      (Algebra.TensorProduct.map (.id T T)
        (Algebra.TensorProduct.map (.id S S) g)))

lemma AlgHom.exists_areSplit [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B] (f g : A →ₐ[R] B)
    (p : PrimeSpectrum R) :
    ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
      Module.Flat R S ∧
      IsOpenMap (PrimeSpectrum.comap (algebraMap R S)) ∧
      p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) ∧
      AlgHom.AreSplit
        (Algebra.TensorProduct.map (AlgHom.id S S) f)
        (Algebra.TensorProduct.map (AlgHom.id S S) g)

def sigmaMapCoforkGeneric {C : Type u}
    [Category.{v} C] {E F : Type w} (X : C) (sigma tau : F → E)
    [HasCoproductsOfShape E C] [HasCoproductsOfShape F C]
    [HasCoproductsOfShape (Function.Coequalizer sigma tau) C] :
    Cofork
      (Sigma.map' (f := fun _ : E ↦ X) (g := fun _ : F ↦ X)
        sigma (fun _ ↦ 𝟙 X))
      (Sigma.map' (f := fun _ : E ↦ X) (g := fun _ : F ↦ X)
        tau (fun _ ↦ 𝟙 X)) :=
  Cofork.ofπ
    (Sigma.map' (f := fun _ : Function.Coequalizer sigma tau ↦ X)
      (g := fun _ : E ↦ X)
      (Function.Coequalizer.mk sigma tau) (fun _ ↦ 𝟙 X))
    (by
      rw [Sigma.map'_comp_map', Sigma.map'_comp_map']
      apply Sigma.map'_eq
        (funext fun i ↦ Function.Coequalizer.condition sigma tau i)
      intro _
      simp)

def isColimitCoforkSigmaMap {C : Type u} [Category.{v} C]
    {E F : Type w} (X : C) (σ τ : E → F)
    [HasCoproductsOfShape E C] [HasCoproductsOfShape F C]
    [HasCoproductsOfShape (Function.Coequalizer σ τ) C] :
    IsColimit (sigmaMapCoforkGeneric X σ τ)

lemma map_sigmaMap_naturality {C : Type u} {D : Type u'}
    [Category.{v} C] [Category.{v'} D]
    [HasFiniteCoproducts C] [HasFiniteCoproducts D]
    (G : C ⥤ D) [PreservesFiniteCoproducts G]
    {E F : Type w} [Finite E] [Finite F]
    (X : C) (sigma : F → E) :
    (PreservesCoproduct.iso G (fun _ : F ↦ X)).hom ≫
        Sigma.map' sigma (fun _ ↦ 𝟙 (G.obj X)) =
      G.map (Sigma.map' sigma (fun _ ↦ 𝟙 X)) ≫
        (PreservesCoproduct.iso G (fun _ : E ↦ X)).hom := by
  apply (cancel_epi
    (PreservesCoproduct.iso G (fun _ : F ↦ X)).inv).1
  simp only [Iso.inv_hom_id_assoc]
  apply Sigma.hom_ext
  intro i
  rw [Sigma.ι_comp_map']
  simp only [Category.id_comp]
  symm
  calc
    Sigma.ι (fun _ : F ↦ G.obj X) i ≫
          (PreservesCoproduct.iso G (fun _ : F ↦ X)).inv ≫
          G.map (Sigma.map' sigma (fun _ ↦ 𝟙 X)) ≫
          (PreservesCoproduct.iso G (fun _ : E ↦ X)).hom =
        G.map (Sigma.ι (fun _ : F ↦ X) i) ≫
          G.map (Sigma.map' sigma (fun _ ↦ 𝟙 X)) ≫
          (PreservesCoproduct.iso G (fun _ : E ↦ X)).hom := by
            simp only [PreservesCoproduct.inv_hom, sigmaComparison,
              Sigma.ι_comp_desc_assoc]
    _ = G.map (Sigma.ι (fun _ : F ↦ X) i ≫
          Sigma.map' sigma (fun _ ↦ 𝟙 X)) ≫
          (PreservesCoproduct.iso G (fun _ : E ↦ X)).hom := by
            rw [G.map_comp]
            simp only [Category.assoc]
    _ = G.map (Sigma.ι (fun _ : E ↦ X) (sigma i)) ≫
          (PreservesCoproduct.iso G (fun _ : E ↦ X)).hom := by
            rw [Sigma.ι_comp_map']
            simp
    _ = Sigma.ι (fun _ : E ↦ G.obj X) (sigma i) := by
          simpa [← PreservesCoproduct.inv_hom] using
            (map_ι_comp_inv_sigmaComparison
              (G := G) (f := fun _ : E ↦ X) (sigma i))

def isColimitMapSigmaMapCofork {C : Type u} {D : Type u'}
    [Category.{v} C] [Category.{v'} D]
    [HasFiniteCoproducts C] [HasFiniteCoproducts D]
    (G : C ⥤ D) [PreservesFiniteCoproducts G]
    {E F : Type w} [Finite E] [Finite F]
    (X : C) (sigma tau : F → E)
    [Finite (Function.Coequalizer sigma tau)] :
    IsColimit (G.mapCocone (sigmaMapCoforkGeneric X sigma tau))

lemma preservesColimit_parallelPair_of_split
    {C : Type u} {D : Type u'}
    [Category.{v} C] [Category.{v'} D]
    [HasFiniteCoproducts C] [HasFiniteCoproducts D]
    (G : C ⥤ D) [PreservesFiniteCoproducts G]
    {A B : C} (f g : A ⟶ B)
    {E F : Type w} [Finite E] [Finite F]
    (X : C) (sigma tau : F → E)
    (eA : A ≅ ∐ fun _ : F ↦ X)
    (eB : B ≅ ∐ fun _ : E ↦ X)
    (hf : f ≫ eB.hom = eA.hom ≫
      Sigma.map' sigma (fun _ ↦ 𝟙 X))
    (hg : g ≫ eB.hom = eA.hom ≫
      Sigma.map' tau (fun _ ↦ 𝟙 X)) :
    PreservesColimit (parallelPair f g) G := by
  classical
  let Q := Function.Coequalizer sigma tau
  let : Finite Q := Finite.of_surjective
    (Function.Coequalizer.mk sigma tau)
    (Function.Coequalizer.mk_surjective sigma tau)
  let fModel : (∐ fun _ : F ↦ X) ⟶ ∐ fun _ : E ↦ X :=
    Sigma.map' sigma (fun _ ↦ 𝟙 X)
  let gModel : (∐ fun _ : F ↦ X) ⟶ ∐ fun _ : E ↦ X :=
    Sigma.map' tau (fun _ ↦ 𝟙 X)
  let model : Cofork fModel gModel :=
    sigmaMapCoforkGeneric X sigma tau
  have hmodel : IsColimit model :=
    isColimitCoforkSigmaMap X sigma tau
  have hmap : IsColimit (G.mapCocone model) := by
    exact isColimitMapSigmaMapCofork G X sigma tau
  have hpres : PreservesColimit (parallelPair fModel gModel) G :=
    preservesColimit_of_preserves_colimit_cocone
      (K := parallelPair fModel gModel) (t := model) hmodel hmap
  let : PreservesColimit (parallelPair fModel gModel) G := hpres
  let eDiagram : parallelPair f g ≅ parallelPair fModel gModel :=
    parallelPair.ext eA eB
      (by
        change f ≫ eB.hom = eA.hom ≫ fModel
        simpa only [fModel] using hf)
      (by
        change g ≫ eB.hom = eA.hom ≫ gModel
        simpa only [gModel] using hg)
  exact preservesColimit_of_iso_diagram G eDiagram.symm

instance finiteEtaleOverCategoryForCoequalizers (Y : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ Y)

lemma sigmaMap_comp_sigmaSpec {R : Type u} [CommRing R]
    {E F : Type u} (sigma : E → F) :
    Sigma.map' (f := fun _ : F ↦ Spec (.of R))
        (g := fun _ : E ↦ Spec (.of R)) sigma (fun _ ↦ 𝟙 _) ≫
      sigmaSpec (fun _ : F ↦ CommRingCat.of R) =
    sigmaSpec (fun _ : E ↦ CommRingCat.of R) ≫
      Spec.map (CommRingCat.ofHom (RingHom.compRight R sigma)) := by
  apply Sigma.hom_ext (f := fun _ : E ↦ Spec (.of R))
  intro e
  simp only [← Category.assoc, Sigma.ι_comp_map', Category.id_comp,
    ι_sigmaSpec]
  rw [← Spec.map_comp]
  congr 1

lemma sigmaSpec_comp_algebraMap {R : Type u} [CommRing R]
    (E : Type u) [Finite E] :
    sigmaSpec (fun _ : E ↦ CommRingCat.of R) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (E → R))) =
    Sigma.desc (fun _ : E ↦ 𝟙 (Spec (.of R))) := by
  apply Sigma.hom_ext (f := fun _ : E ↦ Spec (.of R))
  intro e
  simp only [← Category.assoc, ι_sigmaSpec, Sigma.ι_comp_desc]
  rw [← Spec.map_comp]
  convert Spec.map_id (.of R)
  ext x
  rfl

def specPiIsoSigma {R : Type u} [CommRing R]
    (E : Type u) [Finite E] :
    Spec (.of (E → R)) ≅ ∐ fun _ : E ↦ Spec (.of R) :=
  (asIso (sigmaSpec (fun _ : E ↦ CommRingCat.of R))).symm

def specMapAlgEquiv {R S T : Type u}
    [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] (e : S ≃ₐ[R] T) :
    Spec (.of S) ≅ Spec (.of T) where
  hom := Spec.map (CommRingCat.ofHom e.symm.toRingHom)
  inv := Spec.map (CommRingCat.ofHom e.toRingHom)
  hom_inv_id := by
    rw [← Spec.map_comp]
    convert Spec.map_id (.of S)
    ext x
    exact e.symm_apply_apply x
  inv_hom_id := by
    rw [← Spec.map_comp]
    convert Spec.map_id (.of T)
    ext x
    exact e.apply_symm_apply x

def specSplitIso {R S : Type u}
    [CommRing R] [CommRing S] [Algebra R S]
    {E : Type u} [Finite E] (e : S ≃ₐ[R] (E → R)) :
    Spec (.of S) ≅ ∐ fun _ : E ↦ Spec (.of R) :=
  specMapAlgEquiv e ≪≫ specPiIsoSigma E

lemma specSplitIso_hom_over {R S : Type u}
    [CommRing R] [CommRing S] [Algebra R S]
    {E : Type u} [Finite E] (e : S ≃ₐ[R] (E → R)) :
    (specSplitIso e).hom ≫
      Sigma.desc (fun _ : E ↦ 𝟙 (Spec (.of R))) =
    Spec.map (CommRingCat.ofHom (algebraMap R S)) := by
  rw [← sigmaSpec_comp_algebraMap E]
  simp only [specSplitIso, specPiIsoSigma, Iso.trans_hom, specMapAlgEquiv,
    Iso.symm_hom, asIso_inv, Category.assoc]
  slice_lhs 2 3 => rw [IsIso.inv_hom_id]
  simp only [Category.id_comp]
  rw [← Spec.map_comp]
  congr 1
  ext x
  exact e.symm.commutes x

lemma specMap_comp_specSplitIso {R S T : Type u}
    [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] {E F : Type u} [Finite E] [Finite F]
    (eS : S ≃ₐ[R] (E → R)) (eT : T ≃ₐ[R] (F → R))
    (f : S →ₐ[R] T) (sigma : F → E)
    (h : eT.toAlgHom.comp f =
      (AlgHom.compRight R R sigma).comp eS.toAlgHom) :
    Spec.map (CommRingCat.ofHom f.toRingHom) ≫ (specSplitIso eS).hom =
      (specSplitIso eT).hom ≫
        Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of R))) := by
  apply (cancel_mono (sigmaSpec (fun _ : E ↦ CommRingCat.of R))).1
  simp only [specSplitIso, specPiIsoSigma, Iso.trans_hom,
    specMapAlgEquiv, Iso.symm_hom, asIso_inv, Category.assoc]
  rw [sigmaMap_comp_sigmaSpec sigma]
  slice_lhs 3 4 => rw [IsIso.inv_hom_id]
  slice_rhs 2 3 => rw [IsIso.inv_hom_id]
  simp only [Category.comp_id, Category.id_comp]
  rw [← Spec.map_comp, ← Spec.map_comp]
  congr 1
  ext x
  simp only [CommRingCat.hom_comp, CommRingCat.hom_ofHom]
  change f (eS.symm x) = eT.symm ((RingHom.compRight R sigma) x)
  calc
    f (eS.symm x) = eT.symm (eT (f (eS.symm x))) :=
      (eT.symm_apply_apply _).symm
    _ = eT.symm ((AlgHom.compRight R R sigma) (eS (eS.symm x))) := by
      exact congrArg eT.symm (DFunLike.congr_fun h (eS.symm x))
    _ = eT.symm ((RingHom.compRight R sigma) x) := by
      congr 1
      ext i
      exact congrFun (eS.apply_symm_apply x) (sigma i)

def finiteEtaleRingEquiv (R : CommRingCat.{u})

def gammaAlgebraOfHom
    {R : Type u} [CommRing R] {Z : Scheme.{u}}
    (p : Z ⟶ Spec (.of R)) : Algebra R Γ(Z, ⊤)

lemma hom_eq_isoSpec_hom_comp_specMap_algebraMap
    {R : Type u} [CommRing R] {Z : Scheme.{u}} [IsAffine Z]
    (p : Z ⟶ Spec (.of R)) :
    letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
    p = Z.isoSpec.hom ≫
      Spec.map (CommRingCat.ofHom (algebraMap R Γ(Z, ⊤))) := by
  let : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
  change p = Z.isoSpec.hom ≫
    Spec.map ((Scheme.ΓSpecIso (.of R)).inv ≫ p.appTop)
  have hnat : Z.isoSpec.hom ≫ Spec.map p.appTop =
      p ≫ (Spec (.of R)).isoSpec.hom :=
    Scheme.isoSpec_hom_naturality p
  have hcancel : (Spec (.of R)).isoSpec.hom ≫
      Spec.map (Scheme.ΓSpecIso (.of R)).inv = 𝟙 _ := by
    rw [Scheme.isoSpec_Spec_hom, ← Spec.map_comp,
      Iso.inv_hom_id, Spec.map_id]
  calc
    p = p ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = p ≫ ((Spec (.of R)).isoSpec.hom ≫
        Spec.map (Scheme.ΓSpecIso (.of R)).inv) :=
      congrArg (fun k ↦ p ≫ k) hcancel.symm
    _ = (p ≫ (Spec (.of R)).isoSpec.hom) ≫
        Spec.map (Scheme.ΓSpecIso (.of R)).inv :=
      (Category.assoc _ _ _).symm
    _ = (Z.isoSpec.hom ≫ Spec.map p.appTop) ≫
        Spec.map (Scheme.ΓSpecIso (.of R)).inv :=
      congrArg (fun k ↦ k ≫ Spec.map (Scheme.ΓSpecIso (.of R)).inv)
        hnat.symm
    _ = Z.isoSpec.hom ≫
        (Spec.map p.appTop ≫
          Spec.map (Scheme.ΓSpecIso (.of R)).inv) :=
      Category.assoc _ _ _
    _ = Z.isoSpec.hom ≫
        Spec.map ((Scheme.ΓSpecIso (.of R)).inv ≫ p.appTop) := by
      rw [Spec.map_comp]

def overSpecAlgebra
    {R : Type u} [CommRing R] (L : FiniteEtale (Spec (.of R))) :
    Algebra R Γ(L.left, ⊤)

def pullbackIsoSpecTensorOfHom
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {Z : Scheme.{u}} [IsAffine Z] (p : Z ⟶ Spec (.of R)) :
    letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
    pullback p (Spec.map (CommRingCat.ofHom (algebraMap R S))) ≅
      Spec (.of (TensorProduct R S (Γ(Z, ⊤)))) := by
  letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
  let pS := Spec.map (CommRingCat.ofHom (algebraMap R S))
  let pΓ := Spec.map
    (CommRingCat.ofHom (algebraMap R Γ(Z, ⊤)))
  let e₀ : pullback p pS ≅ pullback pΓ pS :=
    asIso (pullback.map p pS pΓ pS
      Z.isoSpec.hom (𝟙 _) (𝟙 _)
      (by
        simpa only [Category.comp_id] using
          hom_eq_isoSpec_hom_comp_specMap_algebraMap p)
      (by simp))
  exact e₀ ≪≫ pullbackSymmetry pΓ pS ≪≫
    pullbackSpecIso R S Γ(Z, ⊤)

lemma pullbackIsoSpecTensorOfHom_hom_over
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {Z : Scheme.{u}} [IsAffine Z] (p : Z ⟶ Spec (.of R)) :
    letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
    (pullbackIsoSpecTensorOfHom p).hom ≫
        Spec.map (CommRingCat.ofHom
          (algebraMap S (TensorProduct R S (Γ(Z, ⊤))))) =
      pullback.snd p
        (Spec.map (CommRingCat.ofHom (algebraMap R S))) := by
  let : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
  simp [pullbackIsoSpecTensorOfHom, Category.assoc]

def pullbackSplitIsoOfHom
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {Z : Scheme.{u}} [IsAffine Z] (p : Z ⟶ Spec (.of R)) :
    letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
    ∀ {E : Type u} [Finite E]
      (_e : TensorProduct R S (Γ(Z, ⊤)) ≃ₐ[S] (E → S)),
      pullback p (Spec.map (CommRingCat.ofHom (algebraMap R S))) ≅
        ∐ fun _ : E ↦ Spec (.of S) := by
  letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
  intro E _ e
  exact pullbackIsoSpecTensorOfHom p ≪≫ specSplitIso e

lemma pullbackSplitIsoOfHom_hom_over
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {Z : Scheme.{u}} [IsAffine Z] (p : Z ⟶ Spec (.of R)) :
    letI : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
    ∀ {E : Type u} [Finite E]
      (e : TensorProduct R S (Γ(Z, ⊤)) ≃ₐ[S] (E → S)),
      (pullbackSplitIsoOfHom p e).hom ≫
          Sigma.desc (fun _ : E ↦ 𝟙 (Spec (.of S))) =
        pullback.snd p
          (Spec.map (CommRingCat.ofHom (algebraMap R S))) := by
  let : Algebra R Γ(Z, ⊤) := gammaAlgebraOfHom p
  intro E _ e
  simp only [pullbackSplitIsoOfHom, Iso.trans_hom, Category.assoc]
  rw [specSplitIso_hom_over e,
    pullbackIsoSpecTensorOfHom_hom_over p]

def pullbackSplitIso
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (L : FiniteEtale (Spec (.of R))) [IsAffine L.left] :
    letI : Algebra R Γ(L.left, ⊤) := overSpecAlgebra L
    ∀ {E : Type u} [Finite E]
      (_e : TensorProduct R S (Γ(L.left, ⊤)) ≃ₐ[S] (E → S)),
      ((FiniteEtale.pullback
        (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj L).left ≅
        ∐ fun _ : E ↦ Spec (.of S) := by
  let p : L.left ⟶ Spec (.of R) := L.hom
  change letI : Algebra R Γ(L.left, ⊤) := gammaAlgebraOfHom p
    ∀ {E : Type u} [Finite E]
      (_e : TensorProduct R S (Γ(L.left, ⊤)) ≃ₐ[S] (E → S)),
      pullback p (Spec.map (CommRingCat.ofHom (algebraMap R S))) ≅
        ∐ fun _ : E ↦ Spec (.of S)
  exact pullbackSplitIsoOfHom p

lemma pullbackSplitIso_hom_over
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (L : FiniteEtale (Spec (.of R))) [IsAffine L.left] :
    letI : Algebra R Γ(L.left, ⊤) := overSpecAlgebra L
    ∀ {E : Type u} [Finite E]
      (e : TensorProduct R S (Γ(L.left, ⊤)) ≃ₐ[S] (E → S)),
      (pullbackSplitIso L e).hom ≫
          Sigma.desc (fun _ : E ↦ 𝟙 (Spec (.of S))) =
        ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj L).hom := by
  let p : L.left ⟶ Spec (.of R) := L.hom
  change letI : Algebra R Γ(L.left, ⊤) := gammaAlgebraOfHom p
    ∀ {E : Type u} [Finite E]
      (e : TensorProduct R S (Γ(L.left, ⊤)) ≃ₐ[S] (E → S)),
      (pullbackSplitIsoOfHom p e).hom ≫
          Sigma.desc (fun _ : E ↦ 𝟙 (Spec (.of S))) =
        pullback.snd p
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))
  exact pullbackSplitIsoOfHom_hom_over p

lemma pullbackMap_pullbackSpecIso {R S A B : Type u}
    [CommRing R] [CommRing S] [CommRing A] [CommRing B]
    [Algebra R S] [Algebra R A] [Algebra R B]
    (f : A →ₐ[R] B) :
    let pS := Spec.map (CommRingCat.ofHom (algebraMap R S))
    let pA := Spec.map (CommRingCat.ofHom (algebraMap R A))
    let pB := Spec.map (CommRingCat.ofHom (algebraMap R B))
    let a := Spec.map (CommRingCat.ofHom f.toRingHom)
    let q := pullback.map pS pB pS pA (𝟙 _) a (𝟙 _)
      (by simp) (by
        rw [← Spec.map_comp]
        simp only [Category.comp_id]
        dsimp only [pB]
        congr 1
        ext x
        change (algebraMap R B) x = f ((algebraMap R A) x)
        exact (f.commutes x).symm)
    q ≫ (pullbackSpecIso R S A).hom =
      (pullbackSpecIso R S B).hom ≫
        Spec.map (CommRingCat.ofHom
          (Algebra.TensorProduct.map (AlgHom.id S S) f).toRingHom) := by
  dsimp only
  apply (cancel_mono (pullbackSpecIso R S A).inv).1
  rw [Category.assoc, Iso.hom_inv_id, Category.comp_id]
  apply pullback.hom_ext
  · simp only [Category.assoc, pullback.lift_fst, Category.comp_id,
      pullbackSpecIso_inv_fst]
    apply (cancel_epi (pullbackSpecIso R S B).inv).1
    rw [pullbackSpecIso_inv_fst]
    slice_rhs 1 2 => rw [Iso.inv_hom_id]
    simp only [Category.id_comp]
    rw [← Spec.map_comp]
    congr 1
    ext x
    simp
  · simp only [Category.assoc, pullback.lift_snd,
      pullbackSpecIso_inv_snd]
    apply (cancel_epi (pullbackSpecIso R S B).inv).1
    slice_lhs 1 2 => rw [pullbackSpecIso_inv_snd]
    slice_rhs 1 2 => rw [Iso.inv_hom_id]
    simp only [Category.id_comp]
    rw [← Spec.map_comp, ← Spec.map_comp]
    congr 1

def baseChangeMapOfHom
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {X Y : Scheme.{u}} (pX : X ⟶ Spec (.of R))
    (pY : Y ⟶ Spec (.of R)) (f : X ⟶ Y) (w : f ≫ pY = pX) :
    pullback pX (Spec.map (CommRingCat.ofHom (algebraMap R S))) ⟶
      pullback pY (Spec.map (CommRingCat.ofHom (algebraMap R S)))

lemma baseChangeMap_comp_pullbackIsoSpecTensorOfHom
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y]
    (pX : X ⟶ Spec (.of R)) (pY : Y ⟶ Spec (.of R))
    (f : X ⟶ Y) (w : f ≫ pY = pX) :
    letI : Algebra R Γ(X, ⊤) := gammaAlgebraOfHom pX
    letI : Algebra R Γ(Y, ⊤) := gammaAlgebraOfHom pY
    ∀ (fAlg : Γ(Y, ⊤) →ₐ[R] Γ(X, ⊤))
      (_hf : f.appTop.hom = fAlg.toRingHom),
      baseChangeMapOfHom pX pY f w ≫
          (pullbackIsoSpecTensorOfHom pY).hom =
        (pullbackIsoSpecTensorOfHom pX).hom ≫
          Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.map (AlgHom.id S S) fAlg).toRingHom) := by
  let : Algebra R Γ(X, ⊤) := gammaAlgebraOfHom pX
  let : Algebra R Γ(Y, ⊤) := gammaAlgebraOfHom pY
  intro fAlg hf
  let pS := Spec.map (CommRingCat.ofHom (algebraMap R S))
  let pΓX := Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, ⊤)))
  let pΓY := Spec.map (CommRingCat.ofHom (algebraMap R Γ(Y, ⊤)))
  let a := Spec.map (CommRingCat.ofHom fAlg.toRingHom)
  let eX : pullback pX pS ≅ pullback pΓX pS :=
    asIso (pullback.map pX pS pΓX pS
      X.isoSpec.hom (𝟙 _) (𝟙 _)
      (by simpa only [Category.comp_id] using
        hom_eq_isoSpec_hom_comp_specMap_algebraMap pX)
      (by simp))
  let eY : pullback pY pS ≅ pullback pΓY pS :=
    asIso (pullback.map pY pS pΓY pS
      Y.isoSpec.hom (𝟙 _) (𝟙 _)
      (by simpa only [Category.comp_id] using
        hom_eq_isoSpec_hom_comp_specMap_algebraMap pY)
      (by simp))
  let q : pullback pX pS ⟶ pullback pY pS :=
    baseChangeMapOfHom pX pY f w
  let qSpec : pullback pS pΓX ⟶ pullback pS pΓY :=
    pullback.map pS pΓX pS pΓY
      (𝟙 _) a (𝟙 _) (by simp) (by
        change Spec.map (CommRingCat.ofHom
            (algebraMap R Γ(X, ⊤))) ≫ 𝟙 _ =
          Spec.map (CommRingCat.ofHom fAlg.toRingHom) ≫
            Spec.map (CommRingCat.ofHom (algebraMap R Γ(Y, ⊤)))
        rw [← Spec.map_comp]
        simp only [Category.comp_id]
        congr 1
        ext r
        change (algebraMap R Γ(X, ⊤)) r =
          fAlg ((algebraMap R Γ(Y, ⊤)) r)
        exact (fAlg.commutes r).symm)
  have happ : f.appTop = CommRingCat.ofHom fAlg.toRingHom := by
    ext r
    exact DFunLike.congr_fun hf r
  have hnat : f ≫ Y.isoSpec.hom = X.isoSpec.hom ≫ a := by
    rw [← Scheme.isoSpec_hom_naturality f]
    dsimp only [a]
    rw [happ]
  have q_fst : q ≫ pullback.fst pY pS = pullback.fst pX pS ≫ f := by
    dsimp only [q, baseChangeMapOfHom, pullback.map]
    exact pullback.lift_fst _ _ _
  have q_snd : q ≫ pullback.snd pY pS = pullback.snd pX pS := by
    dsimp only [q, baseChangeMapOfHom, pullback.map]
    exact (pullback.lift_snd _ _ _).trans (Category.comp_id _)
  have eX_fst : eX.hom ≫ pullback.fst pΓX pS =
      pullback.fst pX pS ≫ X.isoSpec.hom := by
    simp [eX, pullback.map]
  have eX_snd : eX.hom ≫ pullback.snd pΓX pS =
      pullback.snd pX pS := by
    simp [eX, pullback.map]
  have eY_fst : eY.hom ≫ pullback.fst pΓY pS =
      pullback.fst pY pS ≫ Y.isoSpec.hom := by
    simp [eY, pullback.map]
  have eY_snd : eY.hom ≫ pullback.snd pΓY pS =
      pullback.snd pY pS := by
    simp [eY, pullback.map]
  have qSpec_fst : qSpec ≫ pullback.fst pS pΓY =
      pullback.fst pS pΓX := by
    simp [qSpec, pullback.map]
  have qSpec_snd : qSpec ≫ pullback.snd pS pΓY =
      pullback.snd pS pΓX ≫ a := by
    simp [qSpec, pullback.map]
  have hpre : q ≫ eY.hom ≫ (pullbackSymmetry pΓY pS).hom =
      eX.hom ≫ (pullbackSymmetry pΓX pS).hom ≫ qSpec := by
    apply pullback.hom_ext
    · simp only [Category.assoc]
      rw [pullbackSymmetry_hom_comp_fst, eY_snd, q_snd,
        qSpec_fst, pullbackSymmetry_hom_comp_fst, eX_snd]
    · simp only [Category.assoc]
      rw [pullbackSymmetry_hom_comp_snd, eY_fst,
        reassoc_of% q_fst, qSpec_snd,
        pullbackSymmetry_hom_comp_snd_assoc, reassoc_of% eX_fst, hnat]
  change q ≫ ((eY ≪≫ pullbackSymmetry pΓY pS ≪≫
      pullbackSpecIso R S Γ(Y, ⊤)).hom) =
    ((eX ≪≫ pullbackSymmetry pΓX pS ≪≫
      pullbackSpecIso R S Γ(X, ⊤)).hom) ≫
        Spec.map (CommRingCat.ofHom
          (Algebra.TensorProduct.map (AlgHom.id S S) fAlg).toRingHom)
  simp only [Iso.trans_hom, Category.assoc]
  slice_lhs 1 3 => rw [hpre]
  slice_lhs 3 4 => rw [pullbackMap_pullbackSpecIso fAlg]

lemma pullbackMap_comp_pullbackSplitIso
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (Lsource Ltarget : FiniteEtale (Spec (.of R)))
    [IsAffine Lsource.left] [IsAffine Ltarget.left]
    (f : Lsource ⟶ Ltarget) :
    letI : Algebra R Γ(Lsource.left, ⊤) := overSpecAlgebra Lsource
    letI : Algebra R Γ(Ltarget.left, ⊤) := overSpecAlgebra Ltarget
    ∀ (fAlg : Γ(Ltarget.left, ⊤) →ₐ[R] Γ(Lsource.left, ⊤))
      (_hf : f.left.appTop.hom = fAlg.toRingHom)
      {Esource Etarget : Type u} [Finite Esource] [Finite Etarget]
      (eTarget : TensorProduct R S Γ(Ltarget.left, ⊤) ≃ₐ[S] (Etarget → S))
      (eSource : TensorProduct R S Γ(Lsource.left, ⊤) ≃ₐ[S] (Esource → S))
      (sigma : Esource → Etarget)
      (_h : eSource.toAlgHom.comp
          (Algebra.TensorProduct.map (AlgHom.id S S) fAlg) =
        (AlgHom.compRight S S sigma).comp eTarget.toAlgHom),
      ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f).left ≫
          (pullbackSplitIso Ltarget eTarget).hom =
        (pullbackSplitIso Lsource eSource).hom ≫
          Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of S))) := by
  let pSource : Lsource.left ⟶ Spec (.of R) := Lsource.hom
  let pTarget : Ltarget.left ⟶ Spec (.of R) := Ltarget.hom
  change letI : Algebra R Γ(Lsource.left, ⊤) := gammaAlgebraOfHom pSource
    letI : Algebra R Γ(Ltarget.left, ⊤) := gammaAlgebraOfHom pTarget
    ∀ (fAlg : Γ(Ltarget.left, ⊤) →ₐ[R] Γ(Lsource.left, ⊤))
      (_hf : f.left.appTop.hom = fAlg.toRingHom)
      {Esource Etarget : Type u} [Finite Esource] [Finite Etarget]
      (eTarget : TensorProduct R S Γ(Ltarget.left, ⊤) ≃ₐ[S] (Etarget → S))
      (eSource : TensorProduct R S Γ(Lsource.left, ⊤) ≃ₐ[S] (Esource → S))
      (sigma : Esource → Etarget)
      (_h : eSource.toAlgHom.comp
          (Algebra.TensorProduct.map (AlgHom.id S S) fAlg) =
        (AlgHom.compRight S S sigma).comp eTarget.toAlgHom),
      ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f).left ≫
          (pullbackSplitIsoOfHom pTarget eTarget).hom =
        (pullbackSplitIsoOfHom pSource eSource).hom ≫
          Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of S)))
  let : Algebra R Γ(Lsource.left, ⊤) := gammaAlgebraOfHom pSource
  let : Algebra R Γ(Ltarget.left, ⊤) := gammaAlgebraOfHom pTarget
  intro fAlg hf Esource Etarget _ _ eTarget eSource sigma h
  have w : f.left ≫ pTarget = pSource := MorphismProperty.Over.w f
  let q := baseChangeMapOfHom (R := R) (S := S)
    pSource pTarget f.left w
  have hmap : ((FiniteEtale.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f).left = q := by
    rfl
  rw [hmap]
  dsimp only [q]
  simp only [pullbackSplitIsoOfHom, Iso.trans_hom]
  have hbase := baseChangeMap_comp_pullbackIsoSpecTensorOfHom
    (R := R) (S := S) pSource pTarget f.left w fAlg hf
  have hsplit := specMap_comp_specSplitIso eTarget eSource
    (Algebra.TensorProduct.map (AlgHom.id S S) fAlg) sigma h
  calc
    baseChangeMapOfHom pSource pTarget f.left w ≫
          ((pullbackIsoSpecTensorOfHom pTarget).hom ≫
            (specSplitIso eTarget).hom) =
        (baseChangeMapOfHom pSource pTarget f.left w ≫
          (pullbackIsoSpecTensorOfHom pTarget).hom) ≫
            (specSplitIso eTarget).hom := (Category.assoc _ _ _).symm
    _ = ((pullbackIsoSpecTensorOfHom pSource).hom ≫
          Spec.map (CommRingCat.ofHom
            (Algebra.TensorProduct.map
              (AlgHom.id S S) fAlg).toRingHom)) ≫
            (specSplitIso eTarget).hom :=
      congrArg (fun k ↦ k ≫ (specSplitIso eTarget).hom) hbase
    _ = (pullbackIsoSpecTensorOfHom pSource).hom ≫
          (Spec.map (CommRingCat.ofHom
              (Algebra.TensorProduct.map
                (AlgHom.id S S) fAlg).toRingHom) ≫
            (specSplitIso eTarget).hom) := Category.assoc _ _ _
    _ = (pullbackIsoSpecTensorOfHom pSource).hom ≫
          ((specSplitIso eSource).hom ≫
            Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of S)))) :=
      congrArg (fun k ↦ (pullbackIsoSpecTensorOfHom pSource).hom ≫ k)
        hsplit
    _ = ((pullbackIsoSpecTensorOfHom pSource).hom ≫
          (specSplitIso eSource).hom) ≫
            Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of S))) :=
      (Category.assoc _ _ _).symm

def splitBase (R : CommRingCat.{u}) : FiniteEtale (Spec R)

def forgetToUnderlyingScheme (Y : Scheme.{u}) :
    FiniteEtale Y ⥤ Scheme.{u}

instance (Y : Scheme.{u}) :
    PreservesFiniteCoproducts (forgetToUnderlyingScheme Y)

def forgetToScheme (R : CommRingCat.{u}) :
    FiniteEtale (Spec R) ⥤ Scheme.{u}

instance (R : CommRingCat.{u}) :
    PreservesFiniteCoproducts (forgetToScheme R)

lemma splitCopowerComparison_over
    (R : CommRingCat.{u}) {E : Type u} [Finite E] :
    (PreservesCoproduct.iso (forgetToScheme R)
      (fun _ : E ↦ splitBase R)).inv ≫
        (∐ fun _ : E ↦ splitBase R).hom =
      Sigma.desc (fun _ : E ↦ 𝟙 (Spec R)) := by
  apply Sigma.hom_ext
  intro i
  rw [PreservesCoproduct.inv_hom]
  exact (Category.assoc _ _ _).symm.trans
    ((congrArg (fun k : (forgetToScheme R).obj (splitBase R) ⟶
        (forgetToScheme R).obj (∐ fun _ : E ↦ splitBase R) =>
          k ≫ (∐ fun _ : E ↦ splitBase R).hom)
      (ι_comp_sigmaComparison (forgetToScheme R) (fun _ : E ↦ splitBase R) i)).trans
      ((MorphismProperty.Over.w (Sigma.ι (fun _ : E ↦ splitBase R) i)).trans
        (Sigma.ι_comp_desc (fun _ : E ↦ 𝟙 (Spec R)) i).symm))

lemma splitCopowerComparison_naturality
    (R : CommRingCat.{u}) {E F : Type u} [Finite E] [Finite F]
    (sigma : F → E) :
    Sigma.map'
        (f := fun _ : E ↦
          (forgetToScheme R).obj (splitBase R))
        (g := fun _ : F ↦
          (forgetToScheme R).obj (splitBase R))
        sigma (fun _ ↦
          𝟙 ((forgetToScheme R).obj (splitBase R))) ≫
        (PreservesCoproduct.iso (forgetToScheme R)
          (fun _ : E ↦ splitBase R)).inv =
      (PreservesCoproduct.iso (forgetToScheme R)
        (fun _ : F ↦ splitBase R)).inv ≫
        (forgetToScheme R).map
          (Sigma.map' (f := fun _ : E ↦ splitBase R)
            (g := fun _ : F ↦ splitBase R)
            sigma (fun _ ↦ 𝟙 (splitBase R))) := by
  let h := CategoryTheory.Limits.map_sigmaMap_naturality
    (forgetToScheme R) (splitBase R) sigma
  apply (cancel_mono
    (PreservesCoproduct.iso (forgetToScheme R)
      (fun _ : E ↦ splitBase R)).hom).1
  rw [Category.assoc, Iso.inv_hom_id, Category.comp_id]
  rw [Category.assoc, ← h]
  rw [← Category.assoc, Iso.inv_hom_id, Category.id_comp]

def finiteEtalePullbackSplitIso
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (L : FiniteEtale (Spec (.of R))) [IsAffine L.left] :
    letI : Algebra R Γ(L.left, ⊤) := overSpecAlgebra L
    ∀ {E : Type u} [Finite E]
      (_e : TensorProduct R S Γ(L.left, ⊤) ≃ₐ[S] (E → S)),
      (FiniteEtale.pullback
        (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj L ≅
        ∐ fun _ : E ↦ splitBase (.of S) := by
  letI : Algebra R Γ(L.left, ⊤) := overSpecAlgebra L
  intro E _ e
  refine MorphismProperty.Over.isoMk
    ((pullbackSplitIso L e) ≪≫
      (PreservesCoproduct.iso (forgetToScheme (.of S))
        (fun _ : E ↦ splitBase (.of S))).symm) ?_
  have hc := splitCopowerComparison_over (.of S) (E := E)
  change ((pullbackSplitIso L e).hom ≫
      (PreservesCoproduct.iso (forgetToScheme (.of S))
        (fun _ : E ↦ splitBase (.of S))).inv) ≫
      (∐ fun _ : E ↦ splitBase (.of S)).hom =
    ((FiniteEtale.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).obj L).hom
  exact (Category.assoc _ _ _).trans
    ((congrArg (fun k ↦ (pullbackSplitIso L e).hom ≫ k) hc).trans
      (pullbackSplitIso_hom_over L e))

lemma finiteEtalePullbackSplitIso_naturality
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (Lsource Ltarget : FiniteEtale (Spec (.of R)))
    [IsAffine Lsource.left] [IsAffine Ltarget.left]
    (f : Lsource ⟶ Ltarget) :
    letI : Algebra R Γ(Lsource.left, ⊤) := overSpecAlgebra Lsource
    letI : Algebra R Γ(Ltarget.left, ⊤) := overSpecAlgebra Ltarget
    ∀ (fAlg : Γ(Ltarget.left, ⊤) →ₐ[R] Γ(Lsource.left, ⊤))
      (_hf : f.left.appTop.hom = fAlg.toRingHom)
      {Esource Etarget : Type u} [Finite Esource] [Finite Etarget]
      (eTarget : TensorProduct R S Γ(Ltarget.left, ⊤) ≃ₐ[S] (Etarget → S))
      (eSource : TensorProduct R S Γ(Lsource.left, ⊤) ≃ₐ[S] (Esource → S))
      (sigma : Esource → Etarget)
      (_h : eSource.toAlgHom.comp
          (Algebra.TensorProduct.map (AlgHom.id S S) fAlg) =
        (AlgHom.compRight S S sigma).comp eTarget.toAlgHom),
      (FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f ≫
          (finiteEtalePullbackSplitIso Ltarget eTarget).hom =
        (finiteEtalePullbackSplitIso Lsource eSource).hom ≫
          Sigma.map' sigma (fun _ ↦ 𝟙 (splitBase (.of S))) := by
  let : Algebra R Γ(Lsource.left, ⊤) := overSpecAlgebra Lsource
  let : Algebra R Γ(Ltarget.left, ⊤) := overSpecAlgebra Ltarget
  intro fAlg hf Esource Etarget _ _ eTarget eSource sigma h
  apply MorphismProperty.Over.Hom.ext
  change ((FiniteEtale.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f).left ≫
        ((pullbackSplitIso Ltarget eTarget).hom ≫
          (PreservesCoproduct.iso (forgetToScheme (.of S))
            (fun _ : Etarget ↦ splitBase (.of S))).inv) =
      ((pullbackSplitIso Lsource eSource).hom ≫
        (PreservesCoproduct.iso (forgetToScheme (.of S))
          (fun _ : Esource ↦ splitBase (.of S))).inv) ≫
        (Sigma.map' (f := fun _ : Etarget ↦ splitBase (.of S))
          (g := fun _ : Esource ↦ splitBase (.of S))
          sigma (fun _ ↦ 𝟙 (splitBase (.of S)))).left
  let csource := (PreservesCoproduct.iso (forgetToScheme (.of S))
    (fun _ : Esource ↦ splitBase (.of S))).inv
  let ctarget := (PreservesCoproduct.iso (forgetToScheme (.of S))
    (fun _ : Etarget ↦ splitBase (.of S))).inv
  have hnat : Sigma.map' sigma (fun _ ↦ 𝟙 (Spec (.of S))) ≫ ctarget =
      csource ≫ (Sigma.map' (f := fun _ : Etarget ↦ splitBase (.of S))
        (g := fun _ : Esource ↦ splitBase (.of S))
        sigma (fun _ ↦ 𝟙 (splitBase (.of S)))).left :=
    splitCopowerComparison_naturality (.of S) sigma
  exact (Category.assoc _ _ _).symm.trans
    ((congrArg (fun k ↦ k ≫ ctarget)
      (pullbackMap_comp_pullbackSplitIso Lsource Ltarget f
        fAlg hf eTarget eSource sigma h)).trans
      ((Category.assoc _ _ _).trans
        ((congrArg (fun k ↦ (pullbackSplitIso Lsource eSource).hom ≫ k) hnat).trans
          (Category.assoc _ _ _).symm)))

lemma preservesColimit_pullback_parallelPair_of_areSplit
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (Lsource Ltarget : FiniteEtale (Spec (.of R)))
    [IsAffine Lsource.left] [IsAffine Ltarget.left]
    (f g : Lsource ⟶ Ltarget) :
    letI : Algebra R Γ(Lsource.left, ⊤) := overSpecAlgebra Lsource
    letI : Algebra R Γ(Ltarget.left, ⊤) := overSpecAlgebra Ltarget
    ∀ (fAlg gAlg : Γ(Ltarget.left, ⊤) →ₐ[R] Γ(Lsource.left, ⊤))
      (_hf : f.left.appTop.hom = fAlg.toRingHom)
      (_hg : g.left.appTop.hom = gAlg.toRingHom)
      (_hsplit : Algebra.AlgHom.AreSplit
        (Algebra.TensorProduct.map (AlgHom.id S S) fAlg)
        (Algebra.TensorProduct.map (AlgHom.id S S) gAlg))
      {C : Type (u + 1)} [Category.{u} C] [HasFiniteCoproducts C]
      (G : FiniteEtale (Spec (.of S)) ⥤ C)
      [PreservesFiniteCoproducts G],
      PreservesColimit
        (parallelPair
          ((FiniteEtale.pullback
            (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f)
          ((FiniteEtale.pullback
            (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map g)) G := by
  let : Algebra R Γ(Lsource.left, ⊤) := overSpecAlgebra Lsource
  let : Algebra R Γ(Ltarget.left, ⊤) := overSpecAlgebra Ltarget
  intro fAlg gAlg hf hg hsplit C _ _ G _
  rcases hsplit with ⟨n, m, eTarget₀, eSource₀, sigma₀, tau₀,
    hsigma₀, htau₀⟩
  let Etarget := ULift.{u, 0} (Fin n)
  let Esource := ULift.{u, 0} (Fin m)
  let eTarget := eTarget₀.trans (Algebra.finULiftPiAlgEquiv S n)
  let eSource := eSource₀.trans (Algebra.finULiftPiAlgEquiv S m)
  let sigma : Esource → Etarget := fun i ↦ ULift.up (sigma₀ i.down)
  let tau : Esource → Etarget := fun i ↦ ULift.up (tau₀ i.down)
  have hsigma : eSource.toAlgHom.comp
      (Algebra.TensorProduct.map (AlgHom.id S S) fAlg) =
      (AlgHom.compRight S S sigma).comp eTarget.toAlgHom := by
    simpa only [eTarget, eSource, sigma] using
      Algebra.liftFinSplitEq
        (Algebra.TensorProduct.map (AlgHom.id S S) fAlg)
        n m eTarget₀ eSource₀ sigma₀ hsigma₀
  have htau : eSource.toAlgHom.comp
      (Algebra.TensorProduct.map (AlgHom.id S S) gAlg) =
      (AlgHom.compRight S S tau).comp eTarget.toAlgHom := by
    simpa only [eTarget, eSource, tau] using
      Algebra.liftFinSplitEq
        (Algebra.TensorProduct.map (AlgHom.id S S) gAlg)
        n m eTarget₀ eSource₀ tau₀ htau₀
  exact CategoryTheory.Limits.preservesColimit_parallelPair_of_split G
    ((FiniteEtale.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map f)
    ((FiniteEtale.pullback
      (Spec.map (CommRingCat.ofHom (algebraMap R S)))).map g)
    (splitBase (.of S)) sigma tau
    (finiteEtalePullbackSplitIso Lsource eSource)
    (finiteEtalePullbackSplitIso Ltarget eTarget)
    (finiteEtalePullbackSplitIso_naturality Lsource Ltarget f
      fAlg hf eTarget eSource sigma hsigma)
    (finiteEtalePullbackSplitIso_naturality Lsource Ltarget g
      gAlg hg eTarget eSource tau htau)

instance finiteEtaleOverCategoryForLocalCoequalizers (Y : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ Y)

instance finiteEtaleHasPullbacksAlongForCoequalizers
    {Y Z : Scheme.{u}} (f : Y ⟶ Z) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance finiteEtaleBaseChangeAlongForCoequalizers
    {Y Z : Scheme.{u}} (f : Y ⟶ Z) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

def overToBase (Z : FiniteEtale X) : Over Z ⥤ FiniteEtale Z.left where
  obj A := FiniteEtale.mk A.hom.left
  map {A B} f := MorphismProperty.Over.homMk f.left.left (by
    change f.left.left ≫ B.hom.left = A.hom.left
    exact congrArg (fun k => k.left) (CategoryTheory.Over.w f))
  map_id _ := rfl
  map_comp _ _ := rfl

def overToBaseFullyFaithful (Z : FiniteEtale X) :
    (overToBase Z).FullyFaithful where
  preimage {A B} f := CategoryTheory.Over.homMk
    (MorphismProperty.Over.homMk f.left (by
      rw [← MorphismProperty.Over.w B.hom, ← MorphismProperty.Over.w A.hom]
      change (f.left ≫ B.hom.left) ≫ Z.hom = A.hom.left ≫ Z.hom
      have hf : f.left ≫ B.hom.left = A.hom.left := MorphismProperty.Over.w f
      exact congrArg (fun k => k ≫ Z.hom) hf))
    (by
      apply MorphismProperty.Over.Hom.ext
      change f.left ≫ B.hom.left = A.hom.left
      exact MorphismProperty.Over.w f)
  map_preimage _ := rfl
  preimage_map _ := rfl

instance (Z : FiniteEtale X) : (overToBase Z).Full

instance (Z : FiniteEtale X) : (overToBase Z).Faithful

instance (Z : FiniteEtale X) : (overToBase Z).EssSurj where
  mem_essImage A := by
    let hcomp : IsFiniteEtale (A.hom ≫ Z.hom) :=
      MorphismProperty.comp_mem @IsFiniteEtale A.hom Z.hom A.prop Z.prop
    let AoverX : FiniteEtale X :=
      MorphismProperty.Over.mk ⊤ (A.hom ≫ Z.hom) hcomp
    let f : AoverX ⟶ Z := by
      dsimp only [AoverX, FiniteEtale.mk]
      exact MorphismProperty.Over.homMk A.hom (by rfl)
    let B : Over Z := CategoryTheory.Over.mk f
    refine ⟨B, ?_⟩
    refine ⟨?_⟩
    dsimp only [B, f, AoverX, overToBase, FiniteEtale.mk,
      MorphismProperty.Over.mk]
    exact MorphismProperty.Over.isoMk (Iso.refl A.left) (by rfl)

instance (Z : FiniteEtale X) : (overToBase Z).IsEquivalence where

def localDiagram
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    WalkingParallelPair ⥤ FiniteEtale
      (Spec (.of (s.pt.left.affineOpenCover.X i : Type u)))

def localRingEquiv
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)

def localRingSource
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)

def localRingTarget
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)

def localRingMapLeft
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    localRingTarget s i ⟶ localRingSource s i

def localRingMapRight
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    localRingTarget s i ⟶ localRingSource s i

def localUnderForget
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)

def localAlgHomLeft
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    (localRingTarget s i).right →ₐ[s.pt.left.affineOpenCover.X i]
      (localRingSource s i).right

def localAlgHomRight
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    (localRingTarget s i).right →ₐ[s.pt.left.affineOpenCover.X i]
      (localRingSource s i).right

lemma localAlgHomLeft_toRingHom
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    ((localDiagram s i).map WalkingParallelPairHom.left).left.appTop.hom =
      (localAlgHomLeft s i).toRingHom

lemma localAlgHomRight_toRingHom
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀) :
    ((localDiagram s i).map WalkingParallelPairHom.right).left.appTop.hom =
      (localAlgHomRight s i).toRingHom

lemma preservesColimit_baseChanged_localDiagram_of_areSplit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)
    {S : Type u} [CommRing S]
    [Algebra (s.pt.left.affineOpenCover.X i) S]
    (hsplit : Algebra.AlgHom.AreSplit
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomLeft s i))
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomRight s i)))
    {C : Type (u + 1)} [Category.{u} C] [HasFiniteCoproducts C]
    (G : FiniteEtale (Spec (.of S)) ⥤ C)
    [PreservesFiniteCoproducts G] :
    PreservesColimit
      (parallelPair
        ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom
            (algebraMap (s.pt.left.affineOpenCover.X i) S)))).map
              ((localDiagram s i).map WalkingParallelPairHom.left))
        ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom
            (algebraMap (s.pt.left.affineOpenCover.X i) S)))).map
              ((localDiagram s i).map WalkingParallelPairHom.right))) G

structure LocalSplitComponent
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)
    (p : PrimeSpectrum (s.pt.left.affineOpenCover.X i)) where
  S : Type u
  [commRing : CommRing S]
  [algebra : Algebra (s.pt.left.affineOpenCover.X i) S]
  flat : Module.Flat (s.pt.left.affineOpenCover.X i) S
  openMap : IsOpenMap (PrimeSpectrum.comap
    (algebraMap (s.pt.left.affineOpenCover.X i) S))
  mem_range : p ∈ Set.range (PrimeSpectrum.comap
    (algebraMap (s.pt.left.affineOpenCover.X i) S))
  split : Algebra.AlgHom.AreSplit
    (Algebra.TensorProduct.map (.id S S) (localAlgHomLeft s i))
    (Algebra.TensorProduct.map (.id S S) (localAlgHomRight s i))

theorem exists_localSplitComponent
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)
    (p : PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    Nonempty (LocalSplitComponent s i p)

def localSplitComponent
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (i : s.pt.left.affineOpenCover.I₀)
    (p : PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    LocalSplitComponent s i p

def localSplitObj
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g)
    (j : Σ i : s.pt.left.affineOpenCover.I₀,
      PrimeSpectrum (s.pt.left.affineOpenCover.X i)) : Scheme

def localSplitMap
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g)
    (j : Σ i : s.pt.left.affineOpenCover.I₀,
      PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    localSplitObj s j ⟶ s.pt.left

theorem localSplitMap_flat_and_isOpenMap
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g)
    (j : Σ i : s.pt.left.affineOpenCover.I₀,
      PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    Flat (localSplitMap s j) ∧ IsOpenMap (localSplitMap s j)

theorem localSplitMap_jointly_surjective
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) :
    ∀ x : s.pt.left,
      ∃ (j : Σ i : s.pt.left.affineOpenCover.I₀,
          PrimeSpectrum (s.pt.left.affineOpenCover.X i))
        (y : localSplitObj s j), localSplitMap s j y = x

theorem localSplitMap_mem_fpqcPrecoverage
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) :
    Presieve.ofArrows (localSplitObj s) (localSplitMap s) ∈
      Scheme.fpqcPrecoverage s.pt.left

def overToBaseMapCoforkIsColimit {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s) :
    IsColimit ((overToBase s.pt).mapCocone
      (CategoryTheory.Over.liftCocone s (𝟙 s.pt)))

def baseChangedLocalCoforkMapIsColimit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s)
    (i : s.pt.left.affineOpenCover.I₀)
    {S : Type u} [CommRing S]
    [Algebra (s.pt.left.affineOpenCover.X i) S]
    (hsplit : Algebra.AlgHom.AreSplit
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomLeft s i))
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomRight s i)))
    {C : Type (u + 1)} [Category.{u} C] [HasFiniteCoproducts C]
    (G : FiniteEtale (Spec (.of S)) ⥤ C)
    [PreservesFiniteCoproducts G] :
    IsColimit
      (G.mapCocone
        ((FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom
            (algebraMap (s.pt.left.affineOpenCover.X i) S)))).mapCocone
          ((FiniteEtale.pullback
            (s.pt.left.affineOpenCover.f i)).mapCocone
            ((overToBase s.pt).mapCocone
              (CategoryTheory.Over.liftCocone s (𝟙 s.pt))))))

def localSplitCoforkForgetAfterPullbackIsColimit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s)
    (i : s.pt.left.affineOpenCover.I₀)
    {S : Type u} [CommRing S]
    [Algebra (s.pt.left.affineOpenCover.X i) S]
    (hsplit : Algebra.AlgHom.AreSplit
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomLeft s i))
      (Algebra.TensorProduct.map (AlgHom.id S S) (localAlgHomRight s i)))
    {U : Scheme.{u}} (q : U ⟶ Spec (.of S)) :
    IsColimit
      ((FiniteEtale.pullback
          (q ≫ (Spec.map (CommRingCat.ofHom
              (algebraMap (s.pt.left.affineOpenCover.X i) S))) ≫
            s.pt.left.affineOpenCover.f i) ⋙
        forgetToUnderlyingScheme U).mapCocone
        ((overToBase s.pt).mapCocone
          (CategoryTheory.Over.liftCocone s (𝟙 s.pt))))

lemma pullback_congrHom_map_naturality
    {W Y T S : Scheme.{u}} {a a' : W ⟶ S} {b b' : Y ⟶ S}
    (p : T ⟶ S) (i : W ⟶ Y) (ha : a = a') (hb : b = b')
    (e : a ≫ 𝟙 S = i ≫ b) (e' : a' ≫ 𝟙 S = i ≫ b') :
    (pullback.congrHom ha rfl).hom ≫
        pullback.map a' p b' p i (𝟙 T) (𝟙 S) e'
          (by simp) =
      pullback.map a p b p i (𝟙 T) (𝟙 S) e
          (by simp) ≫
        (pullback.congrHom hb rfl).hom := by
  simp only [pullback.congrHom, asIso_hom]
  rw [pullback.map_comp, pullback.map_comp]
  simp

lemma pullback_congrHom_map_naturality_inv
    {W Y T S : Scheme.{u}} {a a' : W ⟶ S} {b b' : Y ⟶ S}
    (p : T ⟶ S) (i : W ⟶ Y) (ha : a = a') (hb : b = b')
    (e : a ≫ 𝟙 S = i ≫ b) (e' : a' ≫ 𝟙 S = i ≫ b') :
    (pullback.congrHom ha rfl).inv ≫
        pullback.map a p b p i (𝟙 T) (𝟙 S) e
          (by simp) =
      pullback.map a' p b' p i (𝟙 T) (𝟙 S) e'
          (by simp) ≫
        (pullback.congrHom hb rfl).inv := by
  simp only [pullback.congrHom_inv]
  rw [pullback.map_comp, pullback.map_comp]
  simp

lemma pullback_congrHom_map_naturality_right_rfl
    {W Y T S : Scheme.{u}} {a a' : W ⟶ S} {b : Y ⟶ S}
    (p : T ⟶ S) (i : W ⟶ Y) (ha : a = a')
    (e : a ≫ 𝟙 S = i ≫ b) (e' : a' ≫ 𝟙 S = i ≫ b) :
    (pullback.congrHom ha rfl).hom ≫
        pullback.map a' p b p i (𝟙 T) (𝟙 S) e'
          (by simp) =
      pullback.map a p b p i (𝟙 T) (𝟙 S) e
          (by simp) := by
  simpa [pullback.congrHom] using
    pullback_congrHom_map_naturality p i ha (rfl : b = b) e e'

def forwardLeft : pullback p (a ≫ c) ⟶ pullback p c

def forwardRight : pullback p (a ≫ c) ⟶ pullback p c

def forwardPi : pullback p c ⟶ U

def forwardCofork : Cofork (forwardLeft p) (forwardRight hc p)

def reverseLeft : pullback (a ≫ c) p ⟶ pullback c p

def reverseRight : pullback (a ≫ c) p ⟶ pullback c p

def reversePi : pullback c p ⟶ pullback (𝟙 Z) p

def reverseCofork : Cofork (reverseLeft p) (reverseRight hc p)

def reversePointIso : pullback (𝟙 Z) p ≅ U

def reverseForwardIsColimitEquiv :
    IsColimit (reverseCofork hc p) ≃ IsColimit (forwardCofork hc p)

def zeroBMNLeft : pullback p (a ≫ c) ⟶ pullback p c

def zeroBMNRight : pullback p (a ≫ c) ⟶ pullback p c

lemma forwardLeft_eq_zeroBMNLeft :
    forwardLeft (a := a) (c := c) p = zeroBMNLeft (a := a) (c := c) p

lemma forwardRight_eq_zeroBMNRight :
    forwardRight hc p = zeroBMNRight hc p

def zeroBMNCofork : Cofork (zeroBMNLeft p) (zeroBMNRight hc p)

def forwardZeroBMNIsColimitEquiv :
    IsColimit (forwardCofork hc p) ≃ IsColimit (zeroBMNCofork hc p)

def pointSource (s : Cofork f g) : FiniteEtale s.pt.left

def pointMiddle (s : Cofork f g) : FiniteEtale s.pt.left

def pointTarget (s : Cofork f g) : FiniteEtale s.pt.left

def pointLeft (s : Cofork f g) : pointSource s ⟶ pointMiddle s

def pointRight (s : Cofork f g) : pointSource s ⟶ pointMiddle s

def pointPi (s : Cofork f g) : pointMiddle s ⟶ pointTarget s

def pointCofork (s : Cofork f g) : Cofork (pointLeft s) (pointRight s)

def nestedDiagram
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    WalkingParallelPair ⥤ Scheme.{u}

def nestedUnderlyingCofork
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    Cocone (nestedDiagram s p)

def pullbackCofork (s : Cofork f g) (p : U ⟶ s.pt.left) :
    Cofork ((FiniteEtale.pullback p).map (pointLeft s))
      ((FiniteEtale.pullback p).map (pointRight s))

def underlyingPullbackCofork (s : Cofork f g) (p : U ⟶ s.pt.left) :
    Cofork (((FiniteEtale.pullback p).map (pointLeft s)).left)
      (((FiniteEtale.pullback p).map (pointRight s)).left)

def normalizedNestedCofork
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    Cofork
      ((nestedDiagram s p).map WalkingParallelPairHom.left)
      ((nestedDiagram s p).map WalkingParallelPairHom.right)

lemma nestedSourceHom_eq
    (s : Cofork f g) :
    (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left =
      (f ≫ s.π).left

lemma nestedMiddleHom_eq
    (s : Cofork f g) :
    (s.ι.app WalkingParallelPair.one ≫ 𝟙 s.pt).left =
      s.π.left

lemma nested_zero_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).obj WalkingParallelPair.zero =
      ((FiniteEtale.pullback p).obj (pointSource s)).left

lemma nested_one_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).obj WalkingParallelPair.one =
      ((FiniteEtale.pullback p).obj (pointMiddle s)).left

lemma nested_point_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (normalizedNestedCofork s p).pt =
      (underlyingPullbackCofork s p).pt

lemma nested_pi_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (normalizedNestedCofork s p).π =
      (underlyingPullbackCofork s p).π

def nestedSourceIso
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).obj WalkingParallelPair.zero ≅
      ((FiniteEtale.pullback p).obj (pointSource s)).left

def nestedMiddleIso
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).obj WalkingParallelPair.one ≅
      ((FiniteEtale.pullback p).obj (pointMiddle s)).left

def nestedPointIso
    (s : Cofork f g) (p : U ⟶ s.pt.left)

lemma pullbackLeft_left (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).map (pointLeft s)).left =
      Limits.pullback.lift
        (Limits.pullback.fst ((f ≫ s.π).left) p ≫ f.left)
        (Limits.pullback.snd ((f ≫ s.π).left) p)
        (by
          change (Limits.pullback.fst ((f ≫ s.π).left) p ≫ f.left) ≫
              s.π.left = Limits.pullback.snd ((f ≫ s.π).left) p ≫ p
          calc
            _ = Limits.pullback.fst ((f ≫ s.π).left) p ≫
                (f.left ≫ s.π.left) := Category.assoc _ _ _
            _ = Limits.pullback.fst ((f ≫ s.π).left) p ≫
                (f ≫ s.π).left := rfl
            _ = Limits.pullback.snd ((f ≫ s.π).left) p ≫ p :=
              Limits.pullback.condition) := by
  rfl

lemma pullbackRight_left (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).map (pointRight s)).left =
      Limits.pullback.lift
        (Limits.pullback.fst ((f ≫ s.π).left) p ≫ g.left)
        (Limits.pullback.snd ((f ≫ s.π).left) p)
        (by
          change (Limits.pullback.fst ((f ≫ s.π).left) p ≫ g.left) ≫
              s.π.left = Limits.pullback.snd ((f ≫ s.π).left) p ≫ p
          let h : f.left ≫ s.π.left = g.left ≫ s.π.left :=
            congrArg (fun k ↦ k.left) s.condition
          calc
            _ = Limits.pullback.fst ((f ≫ s.π).left) p ≫
                (g.left ≫ s.π.left) := Category.assoc _ _ _
            _ = Limits.pullback.fst ((f ≫ s.π).left) p ≫
                (f.left ≫ s.π.left) :=
              congrArg
                (fun k ↦ Limits.pullback.fst ((f ≫ s.π).left) p ≫ k)
                h.symm
            _ = Limits.pullback.fst ((f ≫ s.π).left) p ≫
                (f ≫ s.π).left := rfl
            _ = Limits.pullback.snd ((f ≫ s.π).left) p ≫ p :=
              Limits.pullback.condition) := by
  rfl

lemma pullbackPi_left (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).map (pointPi s)).left =
      Limits.pullback.lift
        (Limits.pullback.fst s.π.left p ≫ s.π.left)
        (Limits.pullback.snd s.π.left p)
        (by
          change (Limits.pullback.fst s.π.left p ≫ s.π.left) ≫
              𝟙 s.pt.left = Limits.pullback.snd s.π.left p ≫ p
          simpa only [Category.comp_id] using
            (Limits.pullback.condition :
              Limits.pullback.fst s.π.left p ≫ s.π.left =
                Limits.pullback.snd s.π.left p ≫ p)) := by
  rfl

lemma nestedLeft_left (s : Cofork f g)
    (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).map WalkingParallelPairHom.left =
      Limits.pullback.lift
        (Limits.pullback.fst
          (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫ f.left)
        (Limits.pullback.snd
          (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p)
        (by
          change (Limits.pullback.fst
              (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫
                f.left) ≫
              (s.ι.app WalkingParallelPair.one ≫ 𝟙 s.pt).left =
            Limits.pullback.snd
              (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫ p
          rw [nestedSourceHom_eq, nestedMiddleHom_eq]
          calc
            _ = Limits.pullback.fst (f ≫ s.π).left p ≫
                (f.left ≫ s.π.left) := Category.assoc _ _ _
            _ = Limits.pullback.fst (f ≫ s.π).left p ≫
                (f ≫ s.π).left := rfl
            _ = Limits.pullback.snd (f ≫ s.π).left p ≫ p :=
              Limits.pullback.condition) := by
  rfl

lemma nestedRight_left (s : Cofork f g)
    (p : U ⟶ s.pt.left) :
    (nestedDiagram s p).map WalkingParallelPairHom.right =
      Limits.pullback.lift
        (Limits.pullback.fst
          (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫ g.left)
        (Limits.pullback.snd
          (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p)
        (by
          change (Limits.pullback.fst
              (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫
                g.left) ≫
              (s.ι.app WalkingParallelPair.one ≫ 𝟙 s.pt).left =
            Limits.pullback.snd
              (s.ι.app WalkingParallelPair.zero ≫ 𝟙 s.pt).left p ≫ p
          rw [nestedSourceHom_eq, nestedMiddleHom_eq]
          have hfg : f.left ≫ s.π.left = g.left ≫ s.π.left :=
            congrArg (fun k ↦ k.left) s.condition
          calc
            _ = Limits.pullback.fst (f ≫ s.π).left p ≫
                (g.left ≫ s.π.left) := Category.assoc _ _ _
            _ = Limits.pullback.fst (f ≫ s.π).left p ≫
                (f.left ≫ s.π.left) :=
              congrArg
                (fun k ↦ Limits.pullback.fst (f ≫ s.π).left p ≫ k)
                hfg.symm
            _ = Limits.pullback.fst (f ≫ s.π).left p ≫
                (f ≫ s.π).left := rfl
            _ = Limits.pullback.snd (f ≫ s.π).left p ≫ p :=
              Limits.pullback.condition) := by
  rfl

def normalizedUnderlyingIsColimitEquiv
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    IsColimit (normalizedNestedCofork s p) ≃
      IsColimit (underlyingPullbackCofork s p)

def nestedUnderlyingIsColimitEquiv
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    IsColimit (nestedUnderlyingCofork s p) ≃
      IsColimit (underlyingPullbackCofork s p)

lemma underlying_left_eq_reverseLeft
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).map (pointLeft s)).left =
      AlgebraicGeometry.reverseLeft p

lemma underlying_right_eq_reverseRight
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).map (pointRight s)).left =
      AlgebraicGeometry.reverseRight
        (congrArg (fun k ↦ k.left) s.condition) p := by
  exact pullbackRight_left s p

lemma underlying_pi_eq_reversePi
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (underlyingPullbackCofork s p).π =
      AlgebraicGeometry.reversePi p

lemma underlyingPoint_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    (underlyingPullbackCofork s p).pt =
      Limits.pullback (𝟙 s.pt.left) p

lemma underlyingSource_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).obj (pointSource s)).left =
      Limits.pullback (f ≫ s.π).left p

lemma underlyingMiddle_eq
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    ((FiniteEtale.pullback p).obj (pointMiddle s)).left =
      Limits.pullback s.π.left p

def underlyingPointIso
    (s : Cofork f g) (p : U ⟶ s.pt.left)

def underlyingSourceIso
    (s : Cofork f g) (p : U ⟶ s.pt.left)

def underlyingMiddleIso
    (s : Cofork f g) (p : U ⟶ s.pt.left)

lemma scheme_comp_eqToHom_heq
    {W Y Z : Scheme.{u}} (h : W ⟶ Y) (e : Y = Z) :
    h ≫ eqToHom e ≍ h

lemma scheme_eqToHom_comp_comp_eqToHom_heq
    {V W Y Z : Scheme.{u}} (h : W ⟶ Y) (e₁ : V = W) (e₂ : Y = Z) :
    eqToHom e₁ ≫ h ≫ eqToHom e₂ ≍ h

def underlyingReverseIsColimitEquiv
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    IsColimit (underlyingPullbackCofork s p) ≃
      IsColimit (AlgebraicGeometry.reverseCofork
        (congrArg (fun k ↦ k.left) s.condition) p) :=
  Cofork.isColimitEquivOfIsos
    (underlyingPullbackCofork s p)
    (AlgebraicGeometry.reverseCofork
      (congrArg (fun k ↦ k.left) s.condition) p)
    (underlyingSourceIso s p) (underlyingMiddleIso s p)
    (underlyingPointIso s p)
    (by
      rw [underlying_left_eq_reverseLeft]
      change eqToHom (underlyingSource_eq s p) ≫
          AlgebraicGeometry.reverseLeft p =
        AlgebraicGeometry.reverseLeft p ≫
          eqToHom (underlyingMiddle_eq s p)
      apply eq_of_heq
      exact (eqToHom_comp_heq _ _).trans
        (scheme_comp_eqToHom_heq _ _).symm)
    (by
      rw [underlying_right_eq_reverseRight]
      change eqToHom (underlyingSource_eq s p) ≫
          AlgebraicGeometry.reverseRight
            (congrArg (fun k ↦ k.left) s.condition) p =
        AlgebraicGeometry.reverseRight
            (congrArg (fun k ↦ k.left) s.condition) p ≫
          eqToHom (underlyingMiddle_eq s p)
      apply eq_of_heq
      exact (eqToHom_comp_heq _ _).trans
        (scheme_comp_eqToHom_heq _ _).symm)
    (by
      rw [underlying_pi_eq_reversePi]
      change eqToHom (underlyingMiddle_eq s p).symm ≫
          AlgebraicGeometry.reversePi p ≫
            eqToHom (underlyingPoint_eq s p) =
        AlgebraicGeometry.reversePi p
      apply eq_of_heq
      exact scheme_eqToHom_comp_comp_eqToHom_heq _ _ _)

def underlyingZeroBMNIsColimitEquiv
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    IsColimit (underlyingPullbackCofork s p) ≃
      IsColimit (AlgebraicGeometry.zeroBMNCofork
        (congrArg (fun k ↦ k.left) s.condition) p) :=
  (underlyingReverseIsColimitEquiv s p).trans
    ((AlgebraicGeometry.reverseForwardIsColimitEquiv
      (congrArg (fun k ↦ k.left) s.condition) p).trans
      (AlgebraicGeometry.forwardZeroBMNIsColimitEquiv
        (congrArg (fun k ↦ k.left) s.condition) p))

def nestedZeroBMNIsColimitEquiv
    (s : Cofork f g) (p : U ⟶ s.pt.left) :
    IsColimit (nestedUnderlyingCofork s p) ≃
      IsColimit (AlgebraicGeometry.zeroBMNCofork
        (congrArg (fun k ↦ k.left) s.condition) p) :=
  (nestedUnderlyingIsColimitEquiv s p).trans
    (underlyingZeroBMNIsColimitEquiv s p)

theorem nonempty_isColimit_zeroBMN_of_nested
    (s : Cofork f g) (p : U ⟶ s.pt.left)
    (h : IsColimit
      ((FiniteEtale.pullback p ⋙ forgetToUnderlyingScheme U).mapCocone
        ((overToBase s.pt).mapCocone
          (CategoryTheory.Over.liftCocone s (𝟙 s.pt))))) :
    Nonempty
      (IsColimit (AlgebraicGeometry.zeroBMNCofork
        (congrArg (fun k ↦ k.left) s.condition) p)) :=
  ⟨nestedZeroBMNIsColimitEquiv s p h⟩

def schemePullbackCoforkForDescent
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) {U : Scheme.{u}} (r : U ⟶ s.pt.left)

theorem schemePullbackCoforkForDescent_isColimit_congr
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) {U : Scheme.{u}} {r r' : U ⟶ s.pt.left}
    (h : r = r')
    (hr : Nonempty (IsColimit (schemePullbackCoforkForDescent s r))) :
    Nonempty (IsColimit (schemePullbackCoforkForDescent s r'))

theorem localSplitZeroBMNIsColimit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s)
    (j : Σ i : s.pt.left.affineOpenCover.I₀,
      PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    Nonempty
      (IsColimit
        (schemePullbackCoforkForDescent s (localSplitMap s j)))

theorem localSplitOverlapZeroBMNIsColimit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s)
    (j k : Σ i : s.pt.left.affineOpenCover.I₀,
      PrimeSpectrum (s.pt.left.affineOpenCover.X i)) :
    let r := pullback.fst (localSplitMap s j)
        (localSplitMap s k) ≫ localSplitMap s j
    Nonempty (IsColimit (schemePullbackCoforkForDescent s r)) := by
  dsimp only
  let := (localSplitComponent s j.1 j.2).commRing
  let := (localSplitComponent s j.1 j.2).algebra
  let q := pullback.fst (localSplitMap s j) (localSplitMap s k)
  have hdirect := localSplitCoforkForgetAfterPullbackIsColimit
    s hs j.1 (localSplitComponent s j.1 j.2).split q
  apply PullbackCoforkTransport.nonempty_isColimit_zeroBMN_of_nested
    s (q ≫ localSplitMap s j)
  simpa only [q, localSplitMap, localSplitObj, Category.assoc] using hdirect

def forgetToUnderlyingSchemeMapCoconeIsColimit
    {A B : FiniteEtale X} {f g : A ⟶ B}
    (s : Cofork f g) (hs : IsColimit s) :
    IsColimit ((forgetToUnderlyingScheme X).mapCocone s)

theorem forgetCompOverForgetPreservesParallelPair
    {A B : FiniteEtale X} (f g : A ⟶ B) :
    PreservesColimit (parallelPair f g)
      (FiniteEtale.forget X ⋙ CategoryTheory.Over.forget X)

instance forgetCompOverForgetPreservesCoequalizers :
    PreservesColimitsOfShape WalkingParallelPair
      (FiniteEtale.forget X ⋙ CategoryTheory.Over.forget X) where
  preservesColimit {K} := by
    let := forgetCompOverForgetPreservesParallelPair
      (K.map WalkingParallelPairHom.left)
      (K.map WalkingParallelPairHom.right)
    exact preservesColimit_of_iso_diagram _ (diagramIsoParallelPair K).symm

instance forgetPreservesCoequalizers :
    PreservesColimitsOfShape WalkingParallelPair (FiniteEtale.forget X)

instance forgetPreservesFiniteColimits :
    PreservesFiniteColimits (FiniteEtale.forget X)

instance forgetCompOverForgetPreservesFiniteColimits :
    PreservesFiniteColimits
      (FiniteEtale.forget X ⋙ CategoryTheory.Over.forget X)