colimit_closure.lean

import category_theory.category
import category_theory.limits.limits
import data.set

open category_theory category_theory.limits set

universe u

section
variables {C : Type (u+1)} [large_category C]
variables {α : Type u} (I : α → Type u) [Π a, small_category (I a)]
variables [Π a, has_colimits_of_shape (I a) C]

variables {β : Type u} (G : β → C)

/- We define the closure of the family G under colimits of the shapes I
 and prove it is also parameterized by a set. -/

/-- Predicating that a class of objects of C is closed under I-colimits. -/
def closed_under_colimits (s : set C) : Prop :=
∀ a (F : I a ⥤ C), (∀ i, F.obj i ∈ s) → colimit F ∈ s

/-- "Impredicative" definition of the closure of G under I-colimits:
 the smallest class containing G which is closed under I-colimits. -/
def closure_under_colimits_impred : set C :=
⋂₀ {s | (∀ b, G b ∈ s) ∧ closed_under_colimits I s}

/-- Or we can build the closure as an inductive *proposition* -/
inductive closure_under_colimits_inductive_prop : set C
| base : ∀ b, closure_under_colimits_inductive_prop (G b)
| colimit : ∀ a (F : I a ⥤ C), (∀ i, closure_under_colimits_inductive_prop (F.obj i)) →
    closure_under_colimits_inductive_prop (colimit F)

lemma these_agree : closure_under_colimits_impred I G = closure_under_colimits_inductive_prop I G :=
begin
  apply subset.antisymm,
  { apply sInter_subset_of_mem,
    split,
    { exact λ b, closure_under_colimits_inductive_prop.base I G b },
    { intros a F h, exact closure_under_colimits_inductive_prop.colimit a F h } },
  { intros X hX,
    induction hX with _ a F h IH,
    { apply mem_sInter.mpr,
      rintros t ⟨ht₁, _⟩,
      apply ht₁ },
    { apply mem_sInter.mpr,
      rintros t ht,
      apply ht.2,
      have : closure_under_colimits_impred I G ⊆ t := sInter_subset_of_mem ht,
      exact λ i, this (IH i) } }
end

-- But `subtype (closure_under_colimits_inductive_prop I G) : Type (u+1)`
-- even though based on the definition of `closure_under_colimits_inductive_prop I G`
-- as an inductive prop, it's kind of obvious that it is really "set-sized",
-- that is, it is the image of a function from some Γ : Type u.
-- Let's try to prove this.

-- Commented-out failed attempts:

/-
inductive closure_under_colimits_construction : Type u
| base : Π (b : β), closure_under_colimits_construction
| colimit : Π (a : α) (F : I a ⥤ C)      -- Already a problem; this will live in Type (u+1) because C : Type (u+1).
.
-/

/-
inductive closure_under_colimits_construction : Type u
| base : Π (b : β), closure_under_colimits_construction
| colimit : Π (a : α) (F_obj : I a → closure_under_colimits_construction)
    (F_hom : Π (i j : I a), sorry ⟶ sorry)
-- F_hom is supposed to be a map from the object built by `F_obj i` to the object built by `F_obj j`
-- but what are these objects?
-/

/-
Try to add the objects as an additional type index?

inductive closure_under_colimits_construction : C → Type u
| base : Π (b : β), closure_under_colimits_construction (G b)
| colimit : Π (a : α) (F_obj : I a → closure_under_colimits_construction ?)

| colimit : Π (a : α) (o : I a → C) (F_obj : Π (i : I a), closure_under_colimits_construction (o i))
-- `o` lives in Type (u+1), because C : Type (u+1).
-- Anyways even if this worked, we would know that each `X : C` can be built up as a colimit
-- in a small set of ways, but this tells us nothing about how many such `X` there can be!
-/

/-
Use an inductive─recursive definition??
mutual inductive closure_ir, def closure_val
with closure_ir : Type u
with closure_val : closure_ir → C
Lean doesn't support these.
-/

inductive time {α : Type u} (I : α → Type u) : Type u
| start {} : time
| after : Π a, (I a → time) → time

set_option eqn_compiler.lemmas false -- Huh?! Otherwise Lean times out.
-- This is an irrelevant equation compiler bug, see
-- https://github.com/leanprover-community/lean/issues/102

-- For each time t, we define
-- the type of "ways to build objects as colimits at time t",
-- together with the "interpretation" of such a thing as a particular object.
-- These need to be defined simultaneously by recursion on t
-- because they are mutually dependent
-- (obviously the interpretation of an object depends on how it was built
-- but also the possible ways to build objects depends on the interpretations at previous times
-- because we need to know what the homsets between the objects are).
def Γ₀ : time I → Σ (γ : Type u), γ → C
| time.start := ⟨β, G⟩
| (time.after a ts) :=
/-
  `time.after a ts` classifies those objects
  which are built using index diagram `a` (which has object set `I a`)
  and for which, for each `i : I a`,
  the object in the diagram at `i` was built at time `ts i`.
  We need to specify
  `o`: the constructions of these objects;
  `h`: the maps between the interpretations of these constructions;
  `h_id`, `h_comp`: verification that these maps really form a functor.
  We interpret such a construction by the colimit of that functor.
-/
  ⟨Σ' (o : Π (i : I a), (Γ₀ (ts i)).1)
      (h : Π {i j : I a} (f : i ⟶ j), (Γ₀ (ts i)).2 (o i) ⟶ (Γ₀ (ts j)).2 (o j))
      (h_id : ∀ (i : I a), h (𝟙 i) = 𝟙 _)
      (h_comp : ∀ {i j k : I a} (f : i ⟶ j) (g : j ⟶ k), h (f ≫ g) = h f ≫ h g), true,
   λ p, colimit
     { obj := λ i, (Γ₀ (ts i)).2 (p.1 i),
       map := λ i j f, p.2.1 f,
       map_id' := λ i, p.2.2.1 i,
       map_comp' := λ i j k f g, p.2.2.2.1 f g }⟩

-- All ways to build objects as colimits. Note it's in the original universe!
def Γ : Type u := Σ t, (Γ₀ I G t).1

-- Interpret one of the above as an object of C
def eval : Γ I G → C :=
λ p, (Γ₀ I G p.1).2 p.2

-- I don't know what these are for
/-
lemma eval_start (b : β) : eval I G ⟨time.start, b⟩ = G b :=
rfl

lemma eval_after (a : α) (o : I a → Γ I G) (h : Π {i j : I a} (f : i ⟶ j), eval I G (o i) ⟶ eval I G (o j))
  (h_id : ∀ (i : I a), h (𝟙 i) = 𝟙 _) (h_comp : ∀ {i j k : I a} (f : i ⟶ j) (g : j ⟶ k), h (f ≫ g) = h f ≫ h g) :
  eval I G ⟨time.after a (λ i, (o i).1), λ i, (o i).2, @h, @h_id, @h_comp, trivial⟩ =
  colimit { obj := _, map := @h, map_id' := @h_id, map_comp' := @h_comp } :=
rfl
-/

def im_eval : set C := range (eval I G)

lemma im_eval_contains_G (b : β) : G b ∈ im_eval I G :=
show _ ∈ range (eval I G), from mem_range_self ⟨time.start, b⟩

lemma closed_im_eval : closed_under_colimits I (im_eval I G) :=
begin
  rintros a ⟨F_obj, F_map, F_map_id, F_map_comp⟩ h,
  dunfold im_eval at ⊢ h,
  simp only [mem_range] at ⊢ h,
  choose o ho using h,
  replace ho : F_obj = _ := (funext ho).symm,
  cases ho,
  refine ⟨⟨time.after a _, _, _, _, _, trivial⟩, rfl⟩
end

lemma impred_sub_im_eval : closure_under_colimits_impred I G ⊆ im_eval I G :=
sInter_subset_of_mem ⟨im_eval_contains_G I G, closed_im_eval I G⟩

lemma im_eval_sub_impred : im_eval I G ⊆ closure_under_colimits_inductive_prop I G :=
begin
  rintros _ ⟨⟨t, o⟩, rfl⟩,
  induction t with _ _ IH,
  { apply closure_under_colimits_inductive_prop.base },
  { apply closure_under_colimits_inductive_prop.colimit, intro i, apply IH },
end

-- The closure of G under the specified colimits
-- is exactly the image of the map "eval";
-- in particular it's isomorphic to a type in the original universe.
theorem closure_small : closure_under_colimits_inductive_prop I G = range (eval I G) :=
subset.antisymm begin convert impred_sub_im_eval I G, rw these_agree end (im_eval_sub_impred I G)

end