ConstantRepresentable.lean

def cofanHomEquiv {C : Type*} [Category* C] {ι : Type*}
    {F : ι → C} {c : Cofan F} (hc : IsColimit c) (G : C) :
    (c.pt ⟶ G) ≃ (∀ i, F i ⟶ G) where
  toFun f i := c.inj i ≫ f
  invFun g := hc.desc (Cofan.mk G g)
  left_inv f := by
    apply hc.hom_ext
    intro i
    exact hc.fac (Cofan.mk G (fun j => c.inj j ≫ f)) i
  right_inv g := by
    funext i
    exact hc.fac (Cofan.mk G g) ⟨i⟩

def coprodConstantHomEquiv {C : Type v} [Category.{u} C]
    (J : GrothendieckTopology C) [J.Subcanonical] [HasWeakSheafify J (Type u)]
    {T : C} (hT : IsTerminal T) (ι : Type u)
    {D : C} (j : ι → (T ⟶ D))
    (hc : IsColimit (Cofan.mk (J.yoneda.obj D) (fun i => J.yoneda.map (j i))))
    (G : Sheaf J (Type u)) :
    (J.yoneda.obj D ⟶ G) ≃ ((constantSheaf J (Type u)).obj ι ⟶ G) :=
  (cofanHomEquiv hc G).trans
    ((Equiv.piCongrRight (fun _ => J.yonedaEquiv)).trans
      (TypeCat.homEquiv.symm.trans ((constantSheafAdj J (Type u) hT).homEquiv ι G).symm))

def coprodConstantIso {C : Type v} [Category.{u} C]
    (J : GrothendieckTopology C) [J.Subcanonical] [HasWeakSheafify J (Type u)]
    {T : C} (hT : IsTerminal T) (ι : Type u)
    {D : C} (j : ι → (T ⟶ D))
    (hc : IsColimit (Cofan.mk (J.yoneda.obj D) (fun i => J.yoneda.map (j i)))) :
    J.yoneda.obj D ≅ (constantSheaf J (Type u)).obj ι := by
  let e := coprodConstantHomEquiv J hT ι j hc
  refine (Coyoneda.ext _ _ (fun {G} a => (e G).symm a) (fun {G} a => e G a)
    (fun a => (e _).apply_symm_apply a) (fun a => (e _).symm_apply_apply a) ?_).symm
  intro G H f g
  change ((constantSheafAdj J (Type u) hT).homEquiv ι H).symm
      (↾fun i => J.yonedaEquiv (J.yoneda.map (j i) ≫ (f ≫ g))) =
    ((constantSheafAdj J (Type u) hT).homEquiv ι G).symm
      (↾fun i => J.yonedaEquiv (J.yoneda.map (j i) ≫ f)) ≫ g
  rw [← (constantSheafAdj J (Type u) hT).homEquiv_naturality_right_symm]
  congr 1

def etaleBaseObject (X : Scheme.{u}) : X.Etale

lemma etale_copies_projection (X : Scheme.{u}) (ι : Type u) :
    Etale (Sigma.desc (fun _ : ι => 𝟙 X)) := by
  let : IsZariskiLocalAtSource (show MorphismProperty Scheme.{u} from @Etale) :=
    HasRingHomProperty.instIsZariskiLocalAtSource
  exact IsZariskiLocalAtSource.sigmaDesc (fun _ => inferInstance)

def etaleCopies (X : Scheme.{u}) (ι : Type u) : X.Etale

def etaleCopiesInj (X : Scheme.{u}) (ι : Type u) (i : ι) :
    etaleBaseObject X ⟶ etaleCopies X ι

def etaleIsInitialOfIsEmpty {X : Scheme.{u}} (Y : X.Etale) [IsEmpty Y.left] :
    IsInitial Y

lemma empty_cover_of_initial {X : Scheme.{u}} (Y : X.Etale) (hY : IsInitial Y) :
    ⊥ ∈ X.smallEtaleTopology Y

def etaleCopiesSheafIsColimit (X : Scheme.{u}) (ι : Type u) :
    IsColimit (Cofan.mk (X.smallEtaleTopology.yoneda.obj (etaleCopies X ι))
      (fun i => X.smallEtaleTopology.yoneda.map (etaleCopiesInj X ι i))) := by
  have (i : ι) : Mono ((Cofan.mk (etaleCopies X ι) (etaleCopiesInj X ι)).inj i) := by
    constructor
    intro Y a b hab
    apply MorphismProperty.Over.Hom.ext
    exact (cancel_mono (Sigma.ι (fun _ : ι => X) i)).mp
      (congrArg (fun f => f.left) hab)
  apply X.smallEtaleTopology.isColimitCofanMkYoneda (fun _ : ι => etaleBaseObject X)
    (c := Cofan.mk (etaleCopies X ι) (etaleCopiesInj X ι))
  · rw [Scheme.ofArrows_mem_smallEtaleTopology_iff]
    ext x
    constructor
    · intro _
      trivial
    · intro _
      obtain ⟨i, y, hy⟩ := (sigmaOpenCover (fun _ : ι => X)).exists_eq x
      exact Set.mem_iUnion.mpr ⟨i, y, hy⟩
  · exact empty_cover_of_initial
  · intro i j hij Y a b hab
    have : IsEmpty Y.left := isEmpty_of_commSq_sigmaι_of_ne
      ⟨congrArg (fun f => f.left) hab⟩ hij
    exact ⟨etaleIsInitialOfIsEmpty Y⟩

def etaleCopiesSheafIso (X : Scheme.{u}) (ι : Type u) :
    X.smallEtaleTopology.yoneda.obj (etaleCopies X ι) ≅
      (constantSheaf X.smallEtaleTopology (Type u)).obj ι

lemma etaleCopiesSheafIso_inv_unit (X : Scheme.{u}) (ι : Type u) (i : ι) :
    (etaleCopiesSheafIso X ι).inv.hom.app (op (etaleBaseObject X))
      (((constantSheafAdj X.smallEtaleTopology (Type u)
        (MorphismProperty.Over.mkIdTerminal
          (show MorphismProperty Scheme.{u} from @Etale) X)).unit.app
          ι) i) = etaleCopiesInj X ι i := by
  let hT := MorphismProperty.Over.mkIdTerminal
    (show MorphismProperty Scheme.{u} from @Etale) X
  have he : (constantSheafAdj X.smallEtaleTopology (Type u) hT).homEquiv ι
      (X.smallEtaleTopology.yoneda.obj (etaleCopies X ι))
      (etaleCopiesSheafIso X ι).inv =
    ↾(fun j => X.smallEtaleTopology.yonedaEquiv
      (X.smallEtaleTopology.yoneda.map (etaleCopiesInj X ι j))) := by
    exact (Equiv.apply_symm_apply _ _)
  rw [Adjunction.homEquiv_unit] at he
  exact congrArg (fun f => f i) he