connected.lean

import category_theory.category
import category_theory.functor
import data.equiv.basic

noncomputable theory

universes u v w

namespace category_theory


def components (C : Type u) [category.{u v} C] : Type u :=
quot (λ (a b : C), nonempty (a ⟶ b))

axiom connected (C : Type u) [category.{u v} C] : Type u

axiom connected.elim {C : Type u} [category.{u v} C] (h : connected C)
  {α : Sort w} (F : C → α) (hF : ∀ (a b : C) (f : a ⟶ b), F a = F b) : α

axiom connected.eq {C : Type u} [category.{u v} C] (h : connected C)
  {α : Sort w} (F : C → α) (hF : ∀ (a b : C) (f : a ⟶ b), F a = F b) : ∀ a, h.elim F hF = F a

def connected.nonempty {C : Type u} [category.{u v} C] (h : connected C) : nonempty C :=
h.elim (λ a, nonempty.intro a) (λ a b f, by simp)

def connected.eq₂ {C : Type u} [category.{u v} C] (h : connected C)
  {α : Sort w} (F : C → α) (hF : ∀ (a b : C) (f : a ⟶ b), F a = F b) : ∀ a b, F a = F b :=
assume a b, (h.eq F hF a).symm.trans (h.eq F hF b)

lemma connected_iff_components_trivial {C : Type u} [category.{u v} C] (h : connected C) :
  connected C ≃ (components C ≃ unit) :=
sorry


namespace limits
variables (C : Type u) [𝒞 : category.{u v} C]
include 𝒞
variables {J : Type v} [small_category J]

structure shape :=
(X : C)

variables {C}
structure cocone (F : J ⥤ C) extends shape.{u v} C :=
(ι : ∀ j : J, F j ⟶ X)
(w : ∀ {j j' : J} (f : j ⟶ j'), (F.map f) ≫ ι j' = ι j)

class is_colimit {F : J ⥤ C} (t : cocone F) :=
(desc : ∀ (s : cocone F), t.X ⟶ s.X)
(fac'  : ∀ (s : cocone F) (j : J), (t.ι j ≫ desc s) = s.ι j)
(uniq' : ∀ (s : cocone F) (m : t.X ⟶ s.X) (w : ∀ j : J, (t.ι j ≫ m) = s.ι j), m = desc s)
end limits
open category_theory.limits



section cofinal

variables {I : Type v} [small_category I]
variables {J : Type v} [small_category J]

variable (F : I ⥤ J)

def comma (j : J) := Σ i, j ⟶ F i

instance comma.category (j : J) : category (comma F j) :=
{ hom := λ X Y, {f : X.1 ⟶ Y.1 // X.2 ≫ F.map f = Y.2},
  id := λ X, ⟨𝟙 X.1, by obviously⟩,
  comp := λ X Y Z f g, ⟨f.val ≫ g.val, by obviously⟩ }

def cofinal := Π j, connected (comma F j)

section preserves_colimits

variables {C : Type u} [𝒞 : category.{u v} C]
include 𝒞

variables {A : J ⥤ C} (t : cocone A)

def induced_cocone : cocone (F ⋙ A) :=
{ X := t.X,
  ι := λ i, t.ι (F i),
  w := by intros j j' f; apply t.w }

-- When F is cofinal, there is a well-defined way to extend a given
-- cocone on F ⋙ A to a cocone on A...
variables (hF : cofinal F) (s : cocone (F ⋙ A))

def extended_cocone_ι (s : cocone (F ⋙ A)) (j : J) : A j ⟶ s.X :=
(hF j).elim (λ Y, A.map Y.2 ≫ s.ι Y.1)
  (by rintros Y Y' ⟨g, h⟩; rw [←h, ←s.w g]; simp)

lemma extended_cocone_ι_def (s : cocone (F ⋙ A)) (j : J) (i : I) (f : j ⟶ F i) :
  extended_cocone_ι F hF s j = A.map f ≫ s.ι i :=
(hF j).eq _ _ ⟨i, f⟩

def extended_cocone (s : cocone (F ⋙ A)) : cocone A :=
{ X := s.X,
  ι := extended_cocone_ι F hF s,
  w := begin
    intros j j' g,
    rcases (hF j).nonempty with ⟨⟨i, f⟩⟩,    rw extended_cocone_ι_def F hF s j i f,
    rcases (hF j').nonempty with ⟨⟨i', f'⟩⟩, rw extended_cocone_ι_def F hF s j' i' f',
    rw [←category.assoc, ←A.map_comp],
    rw [←extended_cocone_ι_def F hF, ←extended_cocone_ι_def F hF]
  end }

lemma extended_cocone_on_image (s : cocone (F ⋙ A)) (i : I) :
  (extended_cocone F hF s).ι (F i) = s.ι i :=
by convert extended_cocone_ι_def F hF s (F i) i (𝟙 (F i)); simp

-- ... and it takes colimit cocones to colimit cocones
local attribute [elab_simple] is_colimit.desc
def is_colimit_of_cofinal [ht : is_colimit t] : is_colimit (induced_cocone F t) :=
{ desc := λ s, is_colimit.desc t (extended_cocone F hF s),
  fac' := λ s i, by dsimp [induced_cocone]; simp [is_colimit.fac', extended_cocone_on_image],
  uniq' := λ s m hm, begin
    apply is_colimit.uniq' (extended_cocone F hF s),
    dsimp [induced_cocone] at hm,
    dsimp [extended_cocone],
    intro j,
    rcases (hF j).nonempty with ⟨⟨i, f⟩⟩, rw extended_cocone_ι_def F hF s j i f,
    rw [←hm i, ←category.assoc, t.w f]
  end }

end preserves_colimits

end cofinal

end category_theory