Definitions/Def_AlgebraicGeometry_DescentAction.lean

import Mathlib

set_option autoImplicit false

universe u

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite

namespace AlgebraicGeometry

namespace DescentAction

variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')

noncomputable def unitMap : X' ⟶ pullback (x' ≫ s) s :=
  pullback.lift (𝟙 X') x' (by rw [Category.id_comp])

noncomputable def proj₁₃ :
    pullback (pullback.snd (x' ≫ s) s ≫ s) s ⟶ pullback (x' ≫ s) s :=
  pullback.lift (pullback.fst _ _ ≫ pullback.fst _ _) (pullback.snd _ _)
    (by rw [Category.assoc, pullback.condition]; exact pullback.condition)

@[reassoc (attr := simp)] theorem unitMap_fst : unitMap s x' ≫ pullback.fst _ _ = 𝟙 X' := pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem unitMap_snd : unitMap s x' ≫ pullback.snd _ _ = x' := pullback.lift_snd _ _ _
@[reassoc (attr := simp)] theorem proj₁₃_fst :
    proj₁₃ s x' ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _ := pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem proj₁₃_snd : proj₁₃ s x' ≫ pullback.snd _ _ = pullback.snd _ _ :=
  pullback.lift_snd _ _ _

noncomputable def toTriple : pullback (x' ≫ s) s ⟶ pullback (pullback.snd (x' ≫ s) s ≫ s) s :=
  pullback.lift (𝟙 _) (pullback.fst _ _ ≫ x')
    (by rw [Category.id_comp, Category.assoc]; exact pullback.condition.symm)

@[reassoc (attr := simp)] theorem toTriple_fst : toTriple s x' ≫ pullback.fst _ _ = 𝟙 _ := pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem toTriple_snd : toTriple s x' ≫ pullback.snd _ _ = pullback.fst _ _ ≫ x' :=
  pullback.lift_snd _ _ _

theorem toTriple_proj₁₃ : toTriple s x' ≫ proj₁₃ s x' = pullback.fst _ _ ≫ unitMap s x' := by
  apply pullback.hom_ext
  · rw [Category.assoc, proj₁₃_fst, toTriple_fst_assoc, Category.assoc, unitMap_fst, Category.comp_id]
  · rw [Category.assoc, proj₁₃_snd, toTriple_snd, Category.assoc, unitMap_snd]

variable {s x'} in

noncomputable def actMap (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' = pullback.snd _ _) :
    pullback (pullback.snd (x' ≫ s) s ≫ s) s ⟶ pullback (x' ≫ s) s :=
  pullback.lift (pullback.fst _ _ ≫ act) (pullback.snd _ _)
    (by rw [Category.assoc, reassoc_of% h]; exact pullback.condition)

variable {s x'} in
@[reassoc (attr := simp)] theorem actMap_fst (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' = pullback.snd _ _) :
    actMap act h ≫ pullback.fst _ _ = pullback.fst _ _ ≫ act := pullback.lift_fst _ _ _
variable {s x'} in
@[reassoc (attr := simp)] theorem actMap_snd (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' = pullback.snd _ _) :
    actMap act h ≫ pullback.snd _ _ = pullback.snd _ _ := pullback.lift_snd _ _ _

noncomputable def flipMap {X : Scheme.{u}} (f : X ⟶ S) :
    pullback (pullback.snd f s ≫ s) s ⟶ pullback f s :=
  pullback.lift (pullback.fst _ _ ≫ pullback.fst f s) (pullback.snd _ _)
    (by rw [Category.assoc, pullback.condition]; exact pullback.condition)

@[reassoc (attr := simp)] theorem flipMap_fst {X : Scheme.{u}} (f : X ⟶ S) :
    flipMap s f ≫ pullback.fst f s = pullback.fst _ _ ≫ pullback.fst f s := pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem flipMap_snd {X : Scheme.{u}} (f : X ⟶ S) :
    flipMap s f ≫ pullback.snd f s = pullback.snd _ _ := pullback.lift_snd _ _ _

end DescentAction

structure DescentAction {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S') where

  act : pullback (x' ≫ s) s ⟶ X'
  act_comp : act ≫ x' = pullback.snd _ _
  unit_act : DescentAction.unitMap s x' ≫ act = 𝟙 X'
  trans : DescentAction.actMap act act_comp ≫ act = DescentAction.proj₁₃ s x' ≫ act

namespace DescentAction

variable {S S' : Scheme.{u}} (s : S' ⟶ S)

noncomputable def canonical {X : Scheme.{u}} (f : X ⟶ S) : DescentAction s (pullback.snd f s) where
  act := flipMap s f
  act_comp := flipMap_snd s f
  unit_act := by
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, unitMap_fst_assoc, Category.id_comp]
    · rw [Category.assoc, flipMap_snd, unitMap_snd, Category.id_comp]
  trans := by
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, actMap_fst_assoc, flipMap_fst, Category.assoc, flipMap_fst,
        proj₁₃_fst_assoc]
    · rw [Category.assoc, flipMap_snd, actMap_snd, Category.assoc, flipMap_snd, proj₁₃_snd]

variable {s} in

def Effective {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x') : Prop :=
  ∃ (X : Scheme.{u}) (f : X ⟶ S) (e : pullback f s ≅ X') (he : e.hom ≫ x' = pullback.snd f s),
    pullback.map (pullback.snd f s ≫ s) s (x' ≫ s) s e.hom (𝟙 S') (𝟙 S)
        (by rw [Category.comp_id, ← Category.assoc, he]) (by rw [Category.comp_id, Category.id_comp]) ≫ A.act =
      (canonical s f).act ≫ e.hom

end DescentAction

namespace DescentAction

variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')

noncomputable def invol : pullback (x' ≫ s) s ⟶ pullback (x' ≫ s) s :=
  pullback.lift A.act (pullback.fst _ _ ≫ x')
    (by rw [reassoc_of% A.act_comp, Category.assoc]; exact pullback.condition.symm)

@[reassoc (attr := simp)] theorem invol_fst : A.invol ≫ pullback.fst _ _ = A.act := pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem invol_snd : A.invol ≫ pullback.snd _ _ = pullback.fst _ _ ≫ x' :=
  pullback.lift_snd _ _ _

theorem toTriple_actMap : toTriple s x' ≫ actMap A.act A.act_comp = A.invol := by
  apply pullback.hom_ext
  · rw [Category.assoc, actMap_fst, toTriple_fst_assoc, invol_fst]
  · rw [Category.assoc, actMap_snd, toTriple_snd, invol_snd]

@[reassoc (attr := simp)] theorem invol_act : A.invol ≫ A.act = pullback.fst _ _ := by
  rw [← toTriple_actMap, Category.assoc, A.trans, ← Category.assoc, toTriple_proj₁₃, Category.assoc, A.unit_act,
    Category.comp_id]

@[reassoc (attr := simp)] theorem invol_invol : A.invol ≫ A.invol = 𝟙 _ := by
  apply pullback.hom_ext
  · rw [Category.assoc, invol_fst, invol_act, Category.id_comp]
  · rw [Category.assoc, invol_snd, invol_fst_assoc, A.act_comp, Category.id_comp]

noncomputable def involIso : pullback (x' ≫ s) s ≅ pullback (x' ≫ s) s :=
  ⟨A.invol, A.invol, A.invol_invol, A.invol_invol⟩

theorem act_eq_invol_fst : A.act = A.involIso.hom ≫ pullback.fst _ _ := (A.invol_fst).symm

theorem hom_ext {T : Scheme.{u}} {a b : T ⟶ pullback (x' ≫ s) s} (h₁ : a ≫ pullback.fst _ _ = b ≫ pullback.fst _ _)
    (h₂ : a ≫ A.act = b ≫ A.act) : a = b := by
  apply pullback.hom_ext h₁
  rw [← A.act_comp, reassoc_of% h₂]

theorem equivalence (T : Scheme.{u}) :
    _root_.Equivalence fun x y : T ⟶ X' => ∃ φ : T ⟶ pullback (x' ≫ s) s, φ ≫ pullback.fst _ _ = x ∧ φ ≫ A.act = y where
  refl x := ⟨x ≫ unitMap s x', by rw [Category.assoc, unitMap_fst, Category.comp_id],
    by rw [Category.assoc, A.unit_act, Category.comp_id]⟩
  symm := by
    rintro x y ⟨φ, hφ, hφ'⟩
    exact ⟨φ ≫ A.invol, by rw [Category.assoc, invol_fst, hφ'], by rw [Category.assoc, invol_act, hφ]⟩
  trans := by
    rintro x y z ⟨φ, hφ, hφ'⟩ ⟨ψ, hψ, hψ'⟩
    have w : φ ≫ pullback.snd (x' ≫ s) s ≫ s = (ψ ≫ pullback.snd (x' ≫ s) s) ≫ s := by
      rw [Category.assoc, ← pullback.condition, reassoc_of% hψ, ← reassoc_of% hφ', reassoc_of% A.act_comp,
        pullback.condition]
    let k : T ⟶ pullback (pullback.snd (x' ≫ s) s ≫ s) s := pullback.lift φ (ψ ≫ pullback.snd _ _) w
    have hk₁ : k ≫ actMap A.act A.act_comp = ψ := by
      apply pullback.hom_ext
      · rw [Category.assoc, actMap_fst, pullback.lift_fst_assoc, hφ', hψ]
      · rw [Category.assoc, actMap_snd, pullback.lift_snd]
    refine ⟨k ≫ proj₁₃ s x', by rw [Category.assoc, proj₁₃_fst, pullback.lift_fst_assoc, hφ], ?_⟩
    rw [Category.assoc, ← A.trans, ← Category.assoc, hk₁, hψ']

end DescentAction

namespace DescentAction

section repAct

variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))

noncomputable def fstOver : (Over.map s).obj (Over.mk (pullback.snd (x' ≫ s) s)) ⟶ (Over.map s).obj (Over.mk x') :=
  Over.homMk (pullback.fst (x' ≫ s) s) pullback.condition

noncomputable def univ : G.obj (op ((Over.map s).obj (Over.mk x'))) := hX'.homEquiv (𝟙 (Over.mk x'))

noncomputable def repActOver : Over.mk (pullback.snd (x' ≫ s) s) ⟶ Over.mk x' :=
  hX'.homEquiv.symm (G.map (fstOver s x').op (univ s G x' hX'))

noncomputable def repAct : pullback (x' ≫ s) s ⟶ X' := (repActOver s G x' hX').left

theorem repAct_comp : repAct s G x' hX' ≫ x' = pullback.snd _ _ := Over.w _

theorem map_repActOver_univ :
    G.map ((Over.map s).map (repActOver s G x' hX')).op (univ s G x' hX') =
      G.map (fstOver s x').op (univ s G x' hX') := by
  have h := hX'.homEquiv_comp (repActOver s G x' hX') (𝟙 _)
  rw [Category.comp_id] at h
  have h' : hX'.homEquiv (repActOver s G x' hX') = G.map (fstOver s x').op (univ s G x' hX') := by
    rw [repActOver, Equiv.apply_symm_apply]
  exact h.symm.trans h'

theorem homEquiv_eq_map_univ {U : Over S'} (g : U ⟶ Over.mk x') :
    hX'.homEquiv g = G.map ((Over.map s).map g).op (univ s G x' hX') := by
  have h := hX'.homEquiv_comp g (𝟙 _)
  rw [Category.comp_id] at h
  exact h

theorem unitMap_repAct : unitMap s x' ≫ repAct s G x' hX' = 𝟙 X' := by
  let υ : Over.mk x' ⟶ Over.mk (pullback.snd (x' ≫ s) s) := Over.homMk (unitMap s x') (unitMap_snd s x')
  have hυ : (Over.map s).map υ ≫ fstOver s x' = 𝟙 _ := by
    ext
    change unitMap s x' ≫ pullback.fst _ _ = 𝟙 _
    exact unitMap_fst s x'
  have key : υ ≫ repActOver s G x' hX' = 𝟙 _ := by
    apply hX'.homEquiv.injective
    rw [hX'.homEquiv_comp, repActOver, Equiv.apply_symm_apply]
    change G.map ((Over.map s).map υ).op (G.map (fstOver s x').op (univ s G x' hX')) = univ s G x' hX'
    rw [← types_comp_apply (G.map _) (G.map _), ← G.map_comp, ← op_comp, hυ, op_id, G.map_id, types_id_apply]
  exact congrArg (fun k => k.left) key

theorem actMap_repAct :
    actMap (repAct s G x' hX') (repAct_comp s G x' hX') ≫ repAct s G x' hX' =
      proj₁₃ s x' ≫ repAct s G x' hX' := by

  let α : Over.mk (pullback.snd (pullback.snd (x' ≫ s) s ≫ s) s) ⟶ Over.mk (pullback.snd (x' ≫ s) s) :=
    Over.homMk (actMap (repAct s G x' hX') (repAct_comp s G x' hX')) (actMap_snd _ (repAct_comp s G x' hX'))
  let π : Over.mk (pullback.snd (pullback.snd (x' ≫ s) s ≫ s) s) ⟶ Over.mk (pullback.snd (x' ≫ s) s) :=
    Over.homMk (proj₁₃ s x') (proj₁₃_snd s x')

  let f₁ : (Over.map s).obj (Over.mk (pullback.snd (pullback.snd (x' ≫ s) s ≫ s) s)) ⟶
      (Over.map s).obj (Over.mk (pullback.snd (x' ≫ s) s)) :=
    Over.homMk (pullback.fst _ _) pullback.condition
  have hα : (Over.map s).map α ≫ fstOver s x' = f₁ ≫ (Over.map s).map (repActOver s G x' hX') := by
    ext
    change actMap (repAct s G x' hX') (repAct_comp s G x' hX') ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ repAct s G x' hX'
    exact actMap_fst _ (repAct_comp s G x' hX')
  have hπ : (Over.map s).map π ≫ fstOver s x' = f₁ ≫ fstOver s x' := by
    ext
    change proj₁₃ s x' ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _
    exact proj₁₃_fst s x'
  have key : α ≫ repActOver s G x' hX' = π ≫ repActOver s G x' hX' := by
    apply hX'.homEquiv.injective
    rw [hX'.homEquiv_comp, hX'.homEquiv_comp, repActOver, Equiv.apply_symm_apply]
    change G.map ((Over.map s).map α).op (G.map (fstOver s x').op (univ s G x' hX')) =
      G.map ((Over.map s).map π).op (G.map (fstOver s x').op (univ s G x' hX'))
    rw [← types_comp_apply (G.map _) (G.map _), ← G.map_comp, ← op_comp, hα,
      ← types_comp_apply (G.map (fstOver s x').op) (G.map _), ← G.map_comp, ← op_comp, hπ,
      op_comp, op_comp, G.map_comp, G.map_comp, types_comp_apply, types_comp_apply]
    erw [map_repActOver_univ]
  exact congrArg (fun k => k.left) key

noncomputable def ofRepresentableBy : DescentAction s x' where
  act := repAct s G x' hX'
  act_comp := repAct_comp s G x' hX'
  unit_act := unitMap_repAct s G x' hX'
  trans := actMap_repAct s G x' hX'

end repAct

end DescentAction

namespace DescentAction

section rep

variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X') (he : e.hom ≫ x' = pullback.snd f s)

noncomputable def cover : (Over.map s).obj (Over.mk (pullback.snd f s)) ⟶ Over.mk f :=
  Over.homMk (pullback.fst f s) pullback.condition

theorem counit_app_eq_cover : (Over.mapPullbackAdj s).counit.app (Over.mk f) = cover s f := by
  ext
  simp [cover]

noncomputable def eOver : Over.mk (pullback.snd f s) ≅ Over.mk x' := Over.isoMk e he

noncomputable def univBC : G.obj (op ((Over.map s).obj (Over.mk (pullback.snd f s)))) :=
  G.map ((Over.map s).map (eOver s x' f e he).hom).op (univ s G x' hX')

noncomputable def eRel : pullback (pullback.snd f s ≫ s) s ⟶ pullback (x' ≫ s) s :=
  pullback.map _ _ _ _ e.hom (𝟙 _) (𝟙 _) (by rw [Category.comp_id, ← Category.assoc, he])
    (by rw [Category.comp_id, Category.id_comp])

@[reassoc (attr := simp)] theorem eRel_fst : eRel s x' f e he ≫ pullback.fst _ _ = pullback.fst _ _ ≫ e.hom :=
  pullback.lift_fst _ _ _
@[reassoc (attr := simp)] theorem eRel_snd : eRel s x' f e he ≫ pullback.snd _ _ = pullback.snd _ _ :=
  (pullback.lift_snd _ _ _).trans (Category.comp_id _)

theorem univBC_compatible
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
    {Z : Over S} (p₁ p₂ : Z ⟶ (Over.map s).obj (Over.mk (pullback.snd f s)))
    (hp : p₁ ≫ cover s f = p₂ ≫ cover s f) :
    G.map p₁.op (univBC s G x' hX' f e he) = G.map p₂.op (univBC s G x' hX' f e he) := by

  let XS : Over S := (Over.map s).obj (Over.mk (pullback.snd f s))
  let ES : Over S := (Over.map s).obj (Over.mk (pullback.snd (pullback.snd f s ≫ s) s))
  let ES' : Over S := (Over.map s).obj (Over.mk (pullback.snd (x' ≫ s) s))
  have hp' : p₁.left ≫ pullback.fst f s = p₂.left ≫ pullback.fst f s := congrArg (fun k => k.left) hp

  let r : Z.left ⟶ pullback (pullback.snd f s ≫ s) s :=
    pullback.lift p₁.left (p₂.left ≫ pullback.snd f s)
      ((Over.w p₁).trans ((Over.w p₂).symm.trans (Category.assoc _ _ _).symm))
  let rS : Z ⟶ ES := Over.homMk r (by
    change r ≫ pullback.snd _ _ ≫ s = Z.hom
    rw [pullback.lift_snd_assoc, Category.assoc]
    exact Over.w p₂)
  let fstS : ES ⟶ XS := Over.homMk (pullback.fst _ _) pullback.condition
  let flipS : ES ⟶ XS := Over.homMk (flipMap s f) (by
    change flipMap s f ≫ pullback.snd f s ≫ s = pullback.snd _ _ ≫ s
    rw [flipMap_snd_assoc])
  have h₁ : p₁ = rS ≫ fstS := by
    ext
    exact (pullback.lift_fst _ _ _).symm
  have h₂ : p₂ = rS ≫ flipS := by
    ext
    change p₂.left = r ≫ flipMap s f
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, pullback.lift_fst_assoc]
      exact hp'.symm
    · rw [Category.assoc, flipMap_snd]
      exact (pullback.lift_snd _ _ _).symm

  let eS : XS ⟶ (Over.map s).obj (Over.mk x') := (Over.map s).map (eOver s x' f e he).hom
  let eRelS : ES ⟶ ES' := Over.homMk (eRel s x' f e he) (by
    change eRel s x' f e he ≫ pullback.snd _ _ ≫ s = pullback.snd _ _ ≫ s
    rw [eRel_snd_assoc])
  have h₃ : fstS ≫ eS = eRelS ≫ fstOver s x' := by
    ext
    change pullback.fst _ _ ≫ e.hom = eRel s x' f e he ≫ pullback.fst _ _
    exact (eRel_fst s x' f e he).symm
  have h₄ : flipS ≫ eS = eRelS ≫ (Over.map s).map (repActOver s G x' hX') := by
    ext
    change flipMap s f ≫ e.hom = eRel s x' f e he ≫ repAct s G x' hX'
    exact hcompat.symm
  rw [h₁, h₂, op_comp, op_comp, G.map_comp, G.map_comp, types_comp_apply, types_comp_apply]
  congr 1
  change G.map fstS.op (G.map eS.op (univ s G x' hX')) = G.map flipS.op (G.map eS.op (univ s G x' hX'))
  rw [← types_comp_apply (G.map eS.op) (G.map fstS.op), ← G.map_comp, ← op_comp, h₃,
    ← types_comp_apply (G.map eS.op) (G.map flipS.op), ← G.map_comp, ← op_comp, h₄,
    op_comp, op_comp, G.map_comp, G.map_comp, types_comp_apply, types_comp_apply, map_repActOver_univ]

theorem existsUnique_univX (hG : Presieve.IsSheafFor G (Presieve.singleton (cover s f)))
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom) :
    ∃! ζ : G.obj (op (Over.mk f)), G.map (cover s f).op ζ = univBC s G x' hX' f e he :=
  (Presieve.isSheafFor_singleton.1 hG) _ (fun p₁ p₂ hp => univBC_compatible s G x' hX' f e he hcompat p₁ p₂ hp)

noncomputable def coverT (T : Over S) : (Over.map s).obj ((Over.pullback s).obj T) ⟶ T :=
  Over.homMk (pullback.fst T.hom s) pullback.condition

theorem counit_app_eq_coverT (T : Over S) : (Over.mapPullbackAdj s).counit.app T = coverT s T := by
  ext
  simp [coverT]

theorem hom_mk_w {T : Over S} (m : T ⟶ Over.mk f) : m.left ≫ f = T.hom := Over.w m

noncomputable def bc {T : Over S} (m : T ⟶ Over.mk f) : (Over.pullback s).obj T ⟶ Over.mk x' :=
  (Over.pullback s).map m ≫ (eOver s x' f e he).hom

theorem bc_left {T : Over S} (m : T ⟶ Over.mk f) :
    (bc s x' f e he m).left = pullback.lift (pullback.fst T.hom s ≫ m.left) (pullback.snd T.hom s)
      (by rw [Category.assoc, hom_mk_w]; exact pullback.condition) ≫ e.hom := rfl

theorem coverT_comp {T : Over S} (m : T ⟶ Over.mk f) :
    coverT s T ≫ m = (Over.map s).map ((Over.pullback s).map m) ≫ cover s f := by
  ext
  change pullback.fst T.hom s ≫ m.left = pullback.lift (pullback.fst T.hom s ≫ m.left) (pullback.snd T.hom s) _ ≫
    pullback.fst f s
  exact (pullback.lift_fst _ _ _).symm

noncomputable abbrev leftHom {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') : pullback T.hom s ⟶ X' := n.left

theorem leftHom_comp {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    leftHom s x' n ≫ x' = pullback.snd T.hom s := Over.w n

noncomputable def nRel {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    pullback (pullback.snd T.hom s ≫ s) s ⟶ pullback (x' ≫ s) s :=
  pullback.map _ _ _ _ (leftHom s x' n) (𝟙 _) (𝟙 _)
    (by rw [Category.comp_id, ← Category.assoc, leftHom_comp s x' n]) (by rw [Category.comp_id, Category.id_comp])

@[reassoc] theorem nRel_fst {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    nRel s x' n ≫ pullback.fst _ _ = pullback.fst _ _ ≫ leftHom s x' n := pullback.lift_fst _ _ _
@[reassoc] theorem nRel_snd {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    nRel s x' n ≫ pullback.snd _ _ = pullback.snd _ _ := (pullback.lift_snd _ _ _).trans (Category.comp_id _)

@[reassoc] theorem flipMap_comp_leftHom {T : Over S} (z : G.obj (op T)) :
    flipMap s T.hom ≫ leftHom s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) =
      nRel s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) ≫ repAct s G x' hX' := by
  set n := hX'.homEquiv.symm (G.map (coverT s T).op z) with hn
  have hz : hX'.homEquiv n = G.map (coverT s T).op z := Equiv.apply_symm_apply _ _
  let ET : Over S' := Over.mk (pullback.snd (pullback.snd T.hom s ≫ s) s)
  let flipO : ET ⟶ (Over.pullback s).obj T := Over.homMk (flipMap s T.hom) (flipMap_snd s T.hom)
  let nRelO : ET ⟶ Over.mk (pullback.snd (x' ≫ s) s) := Over.homMk (nRel s x' n) (nRel_snd s x' n)
  let fstTS : (Over.map s).obj ET ⟶ (Over.map s).obj ((Over.pullback s).obj T) :=
    Over.homMk (pullback.fst _ _) pullback.condition
  have h₁ : (Over.map s).map flipO ≫ coverT s T = fstTS ≫ coverT s T := by
    ext
    change flipMap s T.hom ≫ pullback.fst T.hom s = pullback.fst _ _ ≫ pullback.fst T.hom s
    exact flipMap_fst s T.hom
  have h₂ : (Over.map s).map nRelO ≫ fstOver s x' = fstTS ≫ (Over.map s).map n := by
    ext
    change nRel s x' n ≫ pullback.fst _ _ = pullback.fst _ _ ≫ leftHom s x' n
    exact nRel_fst s x' n
  have key : flipO ≫ n = nRelO ≫ repActOver s G x' hX' := by
    apply hX'.homEquiv.injective
    rw [hX'.homEquiv_comp, hX'.homEquiv_comp, hz, repActOver, Equiv.apply_symm_apply]
    change G.map ((Over.map s).map flipO).op (G.map (coverT s T).op z) =
      G.map ((Over.map s).map nRelO).op (G.map (fstOver s x').op (univ s G x' hX'))
    rw [← types_comp_apply (G.map _) (G.map ((Over.map s).map flipO).op), ← G.map_comp, ← op_comp, h₁,
      ← types_comp_apply (G.map _) (G.map ((Over.map s).map nRelO).op), ← G.map_comp, ← op_comp, h₂,
      op_comp, op_comp, G.map_comp, G.map_comp, types_comp_apply, types_comp_apply, ← homEquiv_eq_map_univ, hz]
  exact congrArg (fun k => k.left) key

theorem desc_condition
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
    {T : Over S} (z : G.obj (op T)) {W : Scheme.{u}} (g₁ g₂ : W ⟶ pullback T.hom s)
    (hg : g₁ ≫ pullback.fst T.hom s = g₂ ≫ pullback.fst T.hom s) :
    g₁ ≫ (leftHom s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) ≫ e.inv ≫ pullback.fst f s) =
      g₂ ≫ (leftHom s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) ≫ e.inv ≫ pullback.fst f s) := by
  set n := hX'.homEquiv.symm (G.map (coverT s T).op z) with hn
  have w : g₁ ≫ pullback.snd T.hom s ≫ s = (g₂ ≫ pullback.snd T.hom s) ≫ s := by
    rw [Category.assoc, ← pullback.condition, reassoc_of% hg]
  let ρ : W ⟶ pullback (pullback.snd T.hom s ≫ s) s := pullback.lift g₁ (g₂ ≫ pullback.snd T.hom s) w
  have hρ₁ : g₁ = ρ ≫ pullback.fst _ _ := (pullback.lift_fst _ _ _).symm
  have hρ₂ : g₂ = ρ ≫ flipMap s T.hom := by
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, pullback.lift_fst_assoc]
      exact hg.symm
    · rw [Category.assoc, flipMap_snd]
      exact (pullback.lift_snd _ _ _).symm
  have heinv : e.inv ≫ pullback.snd f s = x' := by rw [← he, Iso.inv_hom_id_assoc]

  let N : pullback T.hom s ⟶ pullback f s := leftHom s x' n ≫ e.inv
  have hN₂ : N ≫ pullback.snd f s = pullback.snd T.hom s := by
    change (leftHom s x' n ≫ e.inv) ≫ pullback.snd f s = _
    rw [Category.assoc, heinv, leftHom_comp]
  let NS : pullback (pullback.snd T.hom s ≫ s) s ⟶ pullback (pullback.snd f s ≫ s) s :=
    pullback.map _ _ _ _ N (𝟙 _) (𝟙 _) (by rw [Category.comp_id, reassoc_of% hN₂])
      (by rw [Category.comp_id, Category.id_comp])
  have hNS₁ : NS ≫ pullback.fst _ _ = pullback.fst _ _ ≫ N := pullback.lift_fst _ _ _
  have hNS₂ : NS ≫ pullback.snd _ _ = pullback.snd _ _ := (pullback.lift_snd _ _ _).trans (Category.comp_id _)
  have hN : NS ≫ eRel s x' f e he = nRel s x' n := by
    apply pullback.hom_ext
    · rw [Category.assoc, eRel_fst, nRel_fst, ← Category.assoc, hNS₁, Category.assoc]
      change pullback.fst _ _ ≫ (leftHom s x' n ≫ e.inv) ≫ e.hom = _
      rw [Category.assoc, Iso.inv_hom_id, Category.comp_id]
    · rw [Category.assoc, eRel_snd, nRel_snd, hNS₂]
  rw [hρ₁, hρ₂, Category.assoc, Category.assoc]
  congr 1

  rw [flipMap_comp_leftHom_assoc, ← hN, Category.assoc, reassoc_of% hcompat, Iso.hom_inv_id_assoc]
  change _ = NS ≫ flipMap s f ≫ pullback.fst f s
  rw [flipMap_fst, reassoc_of% hNS₁]
  simp only [N, Category.assoc]

section withζ

variable (ζ : G.obj (op (Over.mk f))) (hζ : G.map (cover s f).op ζ = univBC s G x' hX' f e he)

include hζ in

theorem map_coverT_map_eq_homEquiv_bc {T : Over S} (m : T ⟶ Over.mk f) :
    G.map (coverT s T).op (G.map m.op ζ) = hX'.homEquiv (bc s x' f e he m) := by
  have h1 := coverT_comp s f m
  calc G.map (coverT s T).op (G.map m.op ζ)
      = G.map ((Over.map s).map ((Over.pullback s).map m)).op (G.map (cover s f).op ζ) := by
        rw [← types_comp_apply (G.map m.op) (G.map _), ← G.map_comp, ← op_comp, h1, op_comp, G.map_comp,
          types_comp_apply]
    _ = G.map ((Over.map s).map ((Over.pullback s).map m)).op (univBC s G x' hX' f e he) :=
        congrArg (fun y => G.map ((Over.map s).map ((Over.pullback s).map m)).op y) hζ
    _ = hX'.homEquiv (bc s x' f e he m) := by
        rw [univBC, homEquiv_eq_map_univ, bc, Functor.map_comp, op_comp, G.map_comp, types_comp_apply]

include hζ in

theorem map_ζ_injective {T : Over S} [Epi (pullback.fst T.hom s)] {m₁ m₂ : T ⟶ Over.mk f}
    (h : G.map m₁.op ζ = G.map m₂.op ζ) : m₁ = m₂ := by
  have h' : bc s x' f e he m₁ = bc s x' f e he m₂ := by
    apply hX'.homEquiv.injective
    rw [← map_coverT_map_eq_homEquiv_bc s G x' hX' f e he ζ hζ, ← map_coverT_map_eq_homEquiv_bc s G x' hX' f e he ζ hζ,
      h]
  have h'' := congrArg (fun k => k.left) h'
  change (bc s x' f e he m₁).left = (bc s x' f e he m₂).left at h''
  rw [bc_left, bc_left] at h''
  have h₃ := (cancel_mono e.hom).1 h''
  have h₄ := congrArg (fun k => k ≫ pullback.fst f s) h₃
  have h₅ : pullback.fst T.hom s ≫ m₁.left = pullback.fst T.hom s ≫ m₂.left :=
    ((pullback.lift_fst _ _ _).symm.trans h₄).trans (pullback.lift_fst _ _ _)
  ext
  exact (cancel_epi (pullback.fst T.hom s)).1 h₅

include hζ in

theorem map_ζ_surjective (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
    {T : Over S} (hsep : Presieve.IsSeparatedFor G (Presieve.singleton (coverT s T)))
    [EffectiveEpi (pullback.fst T.hom s)] (z : G.obj (op T)) :
    ∃ m : T ⟶ Over.mk f, G.map m.op ζ = z := by
  set n := hX'.homEquiv.symm (G.map (coverT s T).op z) with hn
  have hz : hX'.homEquiv n = G.map (coverT s T).op z := Equiv.apply_symm_apply _ _
  have heinv : e.inv ≫ pullback.snd f s = x' := by rw [← he, Iso.inv_hom_id_assoc]
  let N : pullback T.hom s ⟶ pullback f s := leftHom s x' n ≫ e.inv
  have hN₂ : N ≫ pullback.snd f s = pullback.snd T.hom s := by
    change (leftHom s x' n ≫ e.inv) ≫ pullback.snd f s = _
    rw [Category.assoc, heinv, leftHom_comp]
  let a : pullback T.hom s ⟶ X := leftHom s x' n ≫ e.inv ≫ pullback.fst f s
  let ml : T.left ⟶ X := EffectiveEpi.desc (pullback.fst T.hom s) a
    (fun g₁ g₂ hg => desc_condition s G x' hX' f e he hcompat z g₁ g₂ hg)
  have hml : pullback.fst T.hom s ≫ ml = a := EffectiveEpi.fac _ _ _
  have hmf : ml ≫ f = T.hom := by
    apply (cancel_epi (pullback.fst T.hom s)).1
    rw [← Category.assoc, hml]
    change ((leftHom s x' n ≫ e.inv) ≫ pullback.fst f s) ≫ f = _
    rw [Category.assoc, pullback.condition, ← Category.assoc, hN₂]
    exact pullback.condition.symm
  let m : T ⟶ Over.mk f := Over.homMk ml hmf
  have hlift : pullback.lift (pullback.fst T.hom s ≫ ml) (pullback.snd T.hom s)
      (by rw [Category.assoc, hmf]; exact pullback.condition) = N := by
    apply pullback.hom_ext
    · rw [pullback.lift_fst, hml]
      change (leftHom s x' n ≫ e.inv) ≫ pullback.fst f s = N ≫ pullback.fst f s
      rfl
    · rw [pullback.lift_snd, hN₂]
  have hbc : bc s x' f e he m = n := by
    ext
    change pullback.lift (pullback.fst T.hom s ≫ ml) (pullback.snd T.hom s) _ ≫ e.hom = leftHom s x' n
    rw [hlift]
    change (leftHom s x' n ≫ e.inv) ≫ e.hom = _
    rw [Category.assoc, Iso.inv_hom_id, Category.comp_id]
  refine ⟨m, ?_⟩
  apply Presieve.isSeparatedFor_singleton.1 hsep
  change G.map (coverT s T).op (G.map m.op ζ) = G.map (coverT s T).op z
  rw [map_coverT_map_eq_homEquiv_bc s G x' hX' f e he ζ hζ, hbc, hz]

end withζ

theorem representableBy_of_compatible
    (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
    [∀ T : Over S, EffectiveEpi (pullback.fst T.hom s)]
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom) :
    Nonempty (G.RepresentableBy (Over.mk f)) := by
  obtain ⟨ζ, hζ, -⟩ := existsUnique_univX s G x' hX' f e he (hG (Over.mk f)) hcompat
  have hbij : ∀ T : Over S, Function.Bijective (fun m : T ⟶ Over.mk f => G.map m.op ζ) := fun T =>
    ⟨fun m₁ m₂ h => map_ζ_injective s G x' hX' f e he ζ hζ h,
      fun z => map_ζ_surjective s G x' hX' f e he ζ hζ hcompat (hG T).isSeparatedFor z⟩
  refine ⟨{ homEquiv := fun {T} => Equiv.ofBijective _ (hbij T), homEquiv_comp := ?_ }⟩
  intro T T' g m
  change G.map (g ≫ m).op ζ = G.map g.op (G.map m.op ζ)
  rw [op_comp, G.map_comp, types_comp_apply]

end rep

end DescentAction

end AlgebraicGeometry