Limit.lean

import Mathlib
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Yoneda

open CategoryTheory
open Limits


#check Functor.cones
/-
@[simps!]
def cones : Cᵒᵖ ⥤ Type max u₁ v₃ :=
  (const J).op ⋙ yoneda.obj F
-/

#check cones
/-
@[simps!]
def cones : (J ⥤ C) ⥤ Cᵒᵖ ⥤ Type max u₁ v₃ where
  obj := Functor.cones
  map f := whiskerLeft (const J).op (yoneda.map f)
-/


abbrev cone [Category.{k, h} J] [Category.{u, v} 𝓒] (X : 𝓒) (D : J ⥤ 𝓒)
  := (Functor.const J).obj X ⟶ D

def mkCone [Category.{k, h} J] [Category.{u, v} 𝓒] (D : J ⥤ 𝓒) :
  𝓒ᵒᵖ ⥤ Type (max h u)
:= (cones _ _ ).obj D

structure Limit [Category.{v', u'} J] [Category.{v, u} 𝓒] (D : J ⥤ 𝓒) where
  limit : 𝓒
  repr : (mkCone D).RepresentableBy limit


class hasLimit [Category.{v', u'} J] [Category.{v, u} 𝓒] (D : J ⥤ 𝓒) where
  has_limit : Limit D

class hasFiniteLimit [SmallCategory J] [FinCategory J] [Category 𝓒] (D : J ⥤ 𝓒) extends hasLimit D


def Limit.homEquiv [Category J] [Category 𝓒] {D : J ⥤ 𝓒} (L : Limit D) :
  ∀ {X}, (X ⟶ L.limit) ≃ cone X D
:= L.repr.homEquiv

def Limit.homEquiv_comp [Category J] [Category 𝓒] {D : J ⥤ 𝓒} (L : Limit D) :
  ∀ {X Y : 𝓒} (f : X ⟶ Y) (g : Y ⟶ L.limit),
  L.repr.homEquiv (f ≫ g) = (Functor.const J).map f ≫ L.repr.homEquiv g
  -- (L.homEquiv (f ≫ g)).app j = f ≫ (L.homEquiv g).app j
:= λ _ _ => by rw [L.repr.homEquiv_comp ]; rfl


def Limit.limitCone [Category J] [Category 𝓒] {D : J ⥤ 𝓒} (L : Limit D) :
  cone L.limit D := L.repr.homEquiv (𝟙 L.limit)

def Limit.lift [Category J] [Category 𝓒] {D : J ⥤ 𝓒} (L : Limit D) {X : 𝓒} (c : cone X D) :
  X ⟶ L.limit := L.repr.homEquiv.symm c

lemma Limit.fac [Category J] [Category 𝓒] (D : J ⥤ 𝓒) (L : Limit D) :
  ∀ {X : 𝓒} (c : cone X D) (j : J), L.lift c ≫ L.limitCone.app j = c.app j
:= by
  intro X c j
  have E := L.homEquiv_comp (L.lift c) (𝟙 _); simp at E
  conv at E => arg 1; simp [Limit.lift]
  conv => arg 2; rw [E]; simp
  simp [Limit.limitCone]

lemma Limit.uniq [Category J] [Category 𝓒] {D : J ⥤ 𝓒} (L : Limit D) :
  ∀ {X} (c : cone X D) (m : X ⟶ L.limit) (_ : ∀ j, m ≫ L.limitCone.app j = c.app j), m = L.lift c
:= by
  intro X c m Hm
  apply (L.homEquiv (X := X)).injective
  have E := L.repr.homEquiv.right_inv c
  change _ =  L.repr.homEquiv.toFun (L.repr.homEquiv.invFun c)
  rw [E]
  apply NatTrans.ext; ext i
  rw [<- Hm i]
  have E := L.homEquiv_comp m (𝟙 _); simp at E
  have E' : (L.repr.homEquiv m).app i = ((Functor.const J).map m ≫ L.repr.homEquiv (𝟙 L.limit)).app i := by rw [E]
  change (L.repr.homEquiv m).app i = _
  rw [E']; rfl


section pullback

inductive vertical where
  | left | right | cod

-- abbrev hasPullback.Pair := Discrete hasPullback.Pair'


inductive vertical.Hom : vertical → vertical → Type where
  | left : Hom .left .cod
  | right : Hom .right .cod
  | id p : Hom p p

instance vertical.category : Category vertical where
  Hom := vertical.Hom
  id := vertical.Hom.id
  comp {p p' p''} f g := by
    rcases f<;> rcases g<;> try constructor
  id_comp {X Y} f := by rcases f<;> simp
  comp_id {X Y} f := by rcases f<;> simp
  assoc {X Y Z W} f g h := by
    rcases f<;> rcases g<;> rcases h<;> simp


def hasPullback.functor [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) :
  vertical ⥤ 𝓒
where
  obj p := match p with
    | .left => X
    | .right => Y
    | .cod => Z
  map {p p'} h := match h with
    | vertical.Hom.left => f
    | vertical.Hom.right => g
    | vertical.Hom.id p => match p with
      | .left => 𝟙 X
      | .right => 𝟙 Y
      | .cod => 𝟙 Z
  map_id p := by rcases p<;> simp
  map_comp {p₁ p₂ p₃} f g := by
    rcases f<;> rcases g<;> try simp
    rcases p₁<;> simp

class hasPullback [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) where
  has_pullback : hasLimit (hasPullback.functor f g)

def hasPullback.pullback [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) [P : hasPullback f g] :
  𝓒 := P.has_pullback.has_limit.limit

def hasPullback.fst [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) [P : hasPullback f g] :
  pullback f g ⟶ X := P.has_pullback.has_limit.limitCone.app vertical.left

def hasPullback.snd [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) [P : hasPullback f g] :
  pullback f g ⟶ Y := P.has_pullback.has_limit.limitCone.app vertical.right

lemma hasPullback.condition [Category 𝓒] {X Y Z : 𝓒} (f : X ⟶ Z) (g : Y ⟶ Z) [P : hasPullback f g] :
  fst f g ≫ f = snd f g ≫ g
:= by
  have H := P.has_pullback.has_limit.limitCone.naturality
  have H1 : _ = fst f g ≫ f := H (vertical.Hom.left); simp at H1
  have H2 : _ = snd f g ≫ g := H (vertical.Hom.right); simp at H2
  rw [<- H2, <- H1]


def hasPullback.mkCone [Category 𝓒] {X Y Z W : 𝓒} {f : X ⟶ Z} {g : Y ⟶ Z} [P : hasPullback f g] (h : W ⟶ pullback f g) :
  cone W (hasPullback.functor f g) := {
    app := λ p => match p with
      | .left => h ≫ fst f g
      | .right => h ≫ snd f g
      | .cod => h ≫ fst f g ≫ f
    naturality {p p'} k := match k with
      | vertical.Hom.left => by simp [functor]
      | vertical.Hom.right => by simp [functor]; rw [condition f g]
      |  vertical.Hom.id p => match p with
        | .left => by simp [functor]
        | .right => by simp [functor]
        | .cod => by simp [functor]
  }

def hasPullback.lift [Category 𝓒] {X Y Z : 𝓒} {f : X ⟶ Z} {g : Y ⟶ Z} [P : hasPullback f g] {W : 𝓒} (h : W ⟶ pullback f g) :
  W ⟶ pullback f g := P.has_pullback.has_limit.lift (mkCone h)

lemma hasPullback.lift_fst [Category 𝓒] {X Y Z : 𝓒} {f : X ⟶ Z} {g : Y ⟶ Z} [P : hasPullback f g] {W : 𝓒} (h : W ⟶ pullback f g) :
  lift h ≫ fst f g = h ≫ fst f g  := P.has_pullback.has_limit.fac (c := mkCone h) (j := vertical.left)

lemma hasPullback.lift_snd [Category 𝓒] {X Y Z : 𝓒} {f : X ⟶ Z} {g : Y ⟶ Z} [P : hasPullback f g] {W : 𝓒} (h : W ⟶ pullback f g) :
  lift h ≫ snd f g = h ≫ snd f g := P.has_pullback.has_limit.fac (c := mkCone h) (j := vertical.right)

lemma hasPullback.uniq [Category 𝓒] {X Y Z : 𝓒} {f : X ⟶ Z} {g : Y ⟶ Z} [P : hasPullback f g] {W : 𝓒} (h : W ⟶ pullback f g)
  (m : W ⟶ pullback f g) (H1 : m ≫ fst f g = h ≫ fst f g) (H2 : m ≫ snd f g = h ≫ snd f g) :
  m = lift h
:= by
  apply P.has_pullback.has_limit.uniq (c := mkCone h) m
  intro j; rcases j<;> try simp [mkCone]
  · rw [<- H1]; rfl
  · rw [<- H2]; rfl
  · have E := P.has_pullback.has_limit.limitCone.naturality
    have E' : _ = fst f g ≫ f := E (vertical.Hom.left); simp at E'
    rw [E', <- Category.assoc, H1, Category.assoc]


end pullback











section product



inductive Pair : Type   where | left | right
inductive  Pair.Hom : Pair → Pair → Type u where | id p : Hom p p
instance Pair.cateogry : Category.{0, 0} Pair where
  Hom := Hom
  id := Hom.id
  comp {p p' p''} f g := by
    cases f; cases g; exact Hom.id p
  id_comp f := by cases f; simp
  comp_id f := by cases f; simp
  assoc {p₁ p₂ p₃ p₄} f g h := by
    cases f; cases g; cases h; simp

def Pair.functor [Category.{v, u} 𝓒] (X Y : 𝓒) :
  Pair ⥤ 𝓒
where
  obj p := match p with
    | Pair.left => X
    | Pair.right => Y
  map {p p'} f := by
    rcases f with ⟨p⟩
    cases p<;> simp
    · exact 𝟙 X
    · exact 𝟙 Y
  map_id p := by
    cases p<;> simp [CategoryStruct.id]
  map_comp {p₁ p₂ p₃} f g := by
    rcases f with ⟨p₁⟩
    rcases g with ⟨p₂⟩
    simp [CategoryStruct.comp]
    rcases p₁<;> simp

class hasProd [Category.{v, u} 𝓒] (X Y : 𝓒) where
  has_prod : hasLimit (Pair.functor X Y)

def hasProd.prod [Category.{v, u} 𝓒] (X Y : 𝓒) [P : hasProd X Y] :
  𝓒 := P.has_prod.has_limit.limit
def hasProd.fst [Category.{v, u} 𝓒] (X Y : 𝓒) [P : hasProd X Y] :
  prod X Y ⟶ X := P.has_prod.has_limit.limitCone.app (Pair.left)
def hasProd.snd [Category.{v, u} 𝓒] (X Y : 𝓒) [P : hasProd X Y] :
  prod X Y ⟶ Y := P.has_prod.has_limit.limitCone.app (Pair.right)

def hasProd.mkCone [Category.{v, u} 𝓒] {X Y : 𝓒}  {Z : 𝓒} (f : Z ⟶ X) (g : Z ⟶ Y) :
  cone Z (Pair.functor X Y) := {
    app := λ p => match p with
      | Pair.left => f
      | Pair.right => g
    naturality {p p'} f := by
      rcases f; simp
      rcases p<;> simp [Pair.functor]
  }

def hasProd.lift [Category.{v, u} 𝓒] {X Y : 𝓒} [P : hasProd X Y] {Z : 𝓒} (f : Z ⟶ X) (g : Z ⟶ Y) :
  Z ⟶ prod X Y := P.has_prod.has_limit.lift (mkCone f g)


lemma hasProd.lift_fst [Category.{v, u} 𝓒] (X Y : 𝓒) [P : hasProd X Y] {Z : 𝓒} (f : Z ⟶ X) (g : Z ⟶ Y) :
  lift f g ≫ fst X Y = f := P.has_prod.has_limit.fac (c := mkCone f g) (j := Pair.left)

lemma hasProd.lift_snd [Category.{v, u} 𝓒] (X Y : 𝓒) [P : hasProd X Y] {Z : 𝓒} (f : Z ⟶ X) (g : Z ⟶ Y) :
  lift f g ≫ snd X Y = g := P.has_prod.has_limit.fac (c := mkCone f g) (j := Pair.right)

lemma hasProd.uniq [Category.{v, u} 𝓒] {X Y : 𝓒} [P : hasProd X Y] {Z : 𝓒} (f : Z ⟶ X) (g : Z ⟶ Y)
  (m : Z ⟶ prod X Y) (Hf : m ≫ fst X Y = f) (Hg : m ≫ snd X Y = g) :
  m = lift f g
:= by
  apply P.has_prod.has_limit.uniq (c := mkCone f g) m
  intro j; rcases j<;> simp [mkCone]<;> assumption

end product


section equalizer

inductive parallel where | dom | cod
inductive parallel.Hom : parallel → parallel → Type
  | left : Hom dom cod
  | right : Hom dom cod
  | id p : Hom p p

instance parallel.category : Category.{0, 0} parallel where
  Hom := parallel.Hom
  id := parallel.Hom.id
  comp {p p' p''} f g := by
    rcases f<;> rcases g
    · apply Hom.left
    · apply Hom.right
    · apply Hom.left
    · apply Hom.right
    · apply Hom.id
  id_comp {X Y} f := by rcases f<;> simp
  comp_id {X Y} f := by rcases f<;> simp
  assoc {X Y Z W} f g h := by
    rcases f<;> rcases g<;> rcases h<;> simp

def parallel.functor [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) :
  parallel ⥤ 𝓒
where
  obj p := match p with
    | dom => X
    | cod => Y
  map {p p'} h := match h with
    | Hom.left => f
    | Hom.right => g
    | Hom.id p => match p with
      | dom => 𝟙 X
      | cod => 𝟙 Y
  map_id p := by rcases p<;> simp
  map_comp {p₁ p₂ p₃} f g := by
    rcases f<;> rcases g<;> simp
    rcases p₁<;> simp

class hasEqualizer [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) where
  has_equalizer : hasLimit (parallel.functor f g)

def hasEqualizer.equalizer [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  𝓒 := P.has_equalizer.has_limit.limit

def hasEqualizer.mkCone [Category.{v, u} 𝓒] {X Y Z : 𝓒}  {f g : X ⟶ Y} (h : Z ⟶ X) (H : h ≫ f = h ≫ g) :
  cone Z (parallel.functor f g) := {
    app := λ p => match p with
      | parallel.dom => h
      | parallel.cod => h ≫ f
    naturality {p p'} h := by
      rcases h<;> simp [parallel.functor]; assumption
      rcases p<;> simp
  }

def hasEqualizer.lift [Category.{v, u} 𝓒] {X Y : 𝓒} {f g : X ⟶ Y} [P : hasEqualizer f g] {Z : 𝓒} (h : Z ⟶ X) (H : h ≫ f = h ≫ g) :
  Z ⟶ equalizer f g := P.has_equalizer.has_limit.lift (mkCone h H)

def hasEqualizer.ι [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  equalizer f g ⟶ X := P.has_equalizer.has_limit.limitCone.app (parallel.dom)

def hasEqualizer.ι' [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  equalizer f g ⟶ Y := P.has_equalizer.has_limit.limitCone.app (parallel.cod)

lemma hasEqualizer.ι_comp1 [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  ι' f g = ι f g ≫ f := by
  simp [ι']
  have : _ = ι f g ≫ f:= P.has_equalizer.has_limit.limitCone.naturality parallel.Hom.left; simp at this
  rw [this]

lemma hasEqualizer.ι_comp2 [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  ι' f g = ι f g ≫ g := by
  simp [ι']
  have : _ = ι f g ≫ g:= P.has_equalizer.has_limit.limitCone.naturality parallel.Hom.right; simp at this
  rw [this]


lemma hasEqualizer.lift_ι [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] {Z : 𝓒} (h : Z ⟶ X) (H : h ≫ f = h ≫ g) :
  lift h H ≫ ι f g = h := P.has_equalizer.has_limit.fac (c := mkCone h H) (j := parallel.dom)




lemma hasEqualizer.ι_condition [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] :
  ι f g ≫ f = ι f g ≫ g
:= by
  have El : _ = ι f g ≫ f := P.has_equalizer.has_limit.limitCone.naturality parallel.Hom.left; simp at El
  have Er : _ = ι f g ≫ g := P.has_equalizer.has_limit.limitCone.naturality parallel.Hom.right; simp at Er
  rw [<- El, <- Er]

lemma hasEqualizer.uniq [Category.{v, u} 𝓒] {X Y : 𝓒} (f g : X ⟶ Y) [P : hasEqualizer f g] {Z : 𝓒} (h : Z ⟶ X) (H : h ≫ f = h ≫ g)
  (m : Z ⟶ equalizer f g) (Hm : m ≫ ι f g = h) :
  m = lift h H
:= by
  apply P.has_equalizer.has_limit.uniq (c := mkCone h H) m
  intro i; rcases i<;> simp [mkCone]
  · simp [ι] at Hm; rw [Hm]
  · have El :  _ = ι f g ≫ f :=  P.has_equalizer.has_limit.limitCone.naturality parallel.Hom.left; simp at El
    rw [El, <- Category.assoc, Hm]

end equalizer

section terminal


#check (Discrete PEmpty)
#check Functor.empty
example [Category 𝓒] : Discrete PEmpty ⥤ 𝓒
where
  obj e := e.as.elim
  map {e e'} f := by
    rcases f with ⟨⟨E⟩⟩
    rw [E]
    exact 𝟙 (e'.as.elim )
  map_id e := by simp
  map_comp {e₁ e₂ e₃} f g := by
    rcases f with ⟨⟨E₁⟩⟩
    rcases g with ⟨⟨E₂⟩⟩
    rcases e₁ with ⟨e₁⟩; rcases e₂ with ⟨e₂⟩; rcases e₃ with ⟨e₃⟩
    simp at *; simp at E₁ E₂
    subst e₁ e₃; simp

structure hasTerminal (𝓒) [Category 𝓒] where
  has_terminal : hasLimit (Functor.empty 𝓒)

def hasTerminal.terminal [Category 𝓒] {P : hasTerminal 𝓒} : 𝓒 := P.has_terminal.has_limit.limit

def hasTerminal.mkCone [Category 𝓒] (X : 𝓒) :
  cone X (Functor.empty 𝓒) := {
    app := λ e => by
      simp [Functor.empty]
      exact e.as.elim
    naturality {e e'} h := by
      simp [Functor.empty, Discrete.functor]
      rcases h with ⟨E⟩
      rcases E with ⟨E⟩
      simp
      apply eq_of_heq
      rw [(heq_comp_eqToHom_iff e.as.elim e'.as.elim)]
      rw [E]
  }

def hasTerminal.from [Category 𝓒] (P : hasTerminal 𝓒) (X : 𝓒) :
  X ⟶ P.terminal := P.has_terminal.has_limit.lift (mkCone X)

lemma hasTerminal.uniq [Category 𝓒] {P : hasTerminal 𝓒} (X : 𝓒) (m : X ⟶ P.terminal) :
  m = P.from X
:= by
  have := P.has_terminal.has_limit.uniq (c := mkCone X); simp at this
  rw [this m]; rfl

end terminal