PresheafColimit.lean

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits

open CategoryTheory
open Limits


structure Elm [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) where
  obj : 𝓐
  elm : X.obj (Opposite.op obj)

@[ext]
structure ElmHom [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) (A B : Elm X) where
  hom : A.obj ⟶ B.obj
  w : X.map (Quiver.Hom.op hom) B.elm = A.elm

instance Category [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) : Category (Elm X)
where
  Hom := ElmHom X
  id A := {
    hom := 𝟙 A.obj
    w := by rw [op_id, X.map_id, types_id_apply]
  }
  comp {A B C} f g := {
    hom := f.hom ≫ g.hom
    w := by
      rw [op_comp, X.map_comp, types_comp_apply]
      rw [g.w, f.w]
  }
  id_comp {A B} f := by ext; simp
  comp_id {A B} f := by ext; simp
  assoc {A B C D} f g h := by ext; simp

def ElmP [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) :
  Elm X ⥤ 𝓐
where
  obj A := A.obj
  map {A B} f := f.hom
  map_id f := by
    conv => arg 1; unfold CategoryStruct.id Category.toCategoryStruct _root_.Category; simp
  map_comp {A B C} f g := by
    conv => arg 1; unfold CategoryStruct.comp Category.toCategoryStruct _root_.Category; simp

def PresheafCocone [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type u) :
  Cocone (ElmP X ⋙ yoneda)
:= {
  pt := X
  ι := {
    app z := {
      app A' := λ F => X.map (Quiver.Hom.op F) z.elm
      naturality i j u := by simp [yoneda]; ext f; simp
    }
    naturality z z' f := by
      simp; ext A' g; simp at g; simp [ElmP]
      rw [f.w]
  }
}

def PresheafCocone_isColimit [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type u) :
  IsColimit (PresheafCocone X)
:= {
  desc C := {
    app A' := by
      simp [PresheafCocone]; intro XA'
      exact (C.ι.app ⟨A'.unop, XA'⟩).app A' (𝟙 A'.unop)
    naturality A' B' f := by
      simp [PresheafCocone]; ext XA'; simp
      set a : Elm X := ⟨A'.unop, XA'⟩
      set b : Elm X := ⟨B'.unop, X.map f XA'⟩
      change (C.ι.app b).app B' (𝟙 (Opposite.unop B')) = C.pt.map f ((C.ι.app a).app A' (𝟙 (Opposite.unop A')))

      let ab : b ⟶ a := {
        hom := f.unop
        w := by
          simp [a, b]
      }
      have EC := (C.ι.app a).naturality f
      conv at EC => arg 1; arg 1; simp [ElmP, yoneda]
      conv at EC => arg 2; simp
      have E := congr_fun EC (𝟙 _); simp at E

      have E' := C.ι.naturality ab
      injection E' with E'
      have EB' := congr_fun E' B'; simp [yoneda, ElmP, ab] at EB'
      have := congr_fun EB' (𝟙 B'.unop); simp at this

      rw [<- E, this]
  }
  fac C a := by
    simp; ext B' f; simp [ElmP] at f; simp [PresheafCocone]
    set b : Elm X := { obj := Opposite.unop B', elm := X.map f.op a.elm }
    change (C.ι.app b).app B' (𝟙 (Opposite.unop B')) = (C.ι.app a).app B' f

    let ab : b ⟶ a := {
      hom := f
      w := by
        simp [b]
    }
    have E' := C.ι.naturality ab
    injection E' with E'
    have EB' := congr_fun E' B'; simp [yoneda, ElmP, ab] at EB'
    have E' := congr_fun EB' (𝟙 B'.unop); simp at E'; clear EB'
    rw [E']
  uniq C m Hm := by
    ext A' XA'; simp [PresheafCocone] at XA'; simp
    have E := Hm ⟨A'.unop, XA'⟩
    rw [<- E]
    simp [PresheafCocone]
    rw [X.map_id A']; simp
}