Lean4
/-- This follows this proof from `Borceux, Handbook of categorical algebra 1, Theorem 2.13.4`
although with different names.
-/
theorem colimitLimitToLimitColimit_surjective : Function.Surjective (colimitLimitToLimitColimit F) := by
classical
-- We begin with some element `x` in the limit (over J) over the colimits (over K),
intro x
have z := fun j =>
jointly_surjective'
(limit.π (curry.obj F ⋙ Limits.colim) j x)
-- `k : J ⟶ K` records where the representative of the
-- element in the `j`-th element of `x` lives
let k : J → K := fun j => (z j).choose
let y : ∀ j, F.obj (j, k j) := fun j => (z j).choose_spec.choose
have e : ∀ j, colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ Limits.colim) j x := fun j =>
(z j).choose_spec.choose_spec
clear_value k y
clear z
let k' : K :=
IsFiltered.sup (Finset.univ.image k)
∅
-- and name the morphisms as `g j : k j ⟶ k'`.
have g : ∀ j, k j ⟶ k' := fun j => IsFiltered.toSup (Finset.univ.image k) ∅ (by simp)
clear_value k'
have w :
∀ {j j' : J} (f : j ⟶ j'),
colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j' ×ₘ g j') (y j')) =
colimit.ι ((curry.obj F).obj j') k' (F.map (f ×ₘ g j) (y j)) :=
by
intro j j' f
simp only [Colimit.w_apply, ← Bifunctor.diagonal', ← curry_obj_obj_map, ← curry_obj_map_app]
rw [types_comp_apply, Colimit.w_apply, e, ← Limit.w_apply.{u₁, v, u₁} f, ← e]
simp [Types.Colimit.ι_map_apply]
-- Because `K` is filtered, we can restate this as saying that
-- for each such `f`, there is some place to the right of `k'`
-- where these images of `y j` and `y j'` become equal.
simp_rw [colimit_eq_iff] at w
let kf : ∀ {j j'} (_ : j ⟶ j'), K := fun f => (w f).choose
let gf : ∀ {j j'} (f : j ⟶ j'), k' ⟶ kf f := fun f => (w f).choose_spec.choose
let hf : ∀ {j j'} (f : j ⟶ j'), k' ⟶ kf f := fun f => (w f).choose_spec.choose_spec.choose
have wf : ∀ {j j'} (f : j ⟶ j'), F.map (𝟙 j' ×ₘ (g j' ≫ gf f)) (y j') = F.map (f ×ₘ (g j ≫ hf f)) (y j) :=
fun {j j'} f =>
by
have q :
((curry.obj F).obj j').map (gf f) (F.map (𝟙 j' ×ₘ g j') (y j')) =
((curry.obj F).obj j').map (hf f) (F.map (f ×ₘ g j) (y j)) :=
(w f).choose_spec.choose_spec.choose_spec
dsimp only [curry_obj_obj_map, curry_obj_obj_map] at q
simp_rw [← FunctorToTypes.map_comp_apply, CategoryStruct.comp] at q
convert q <;> simp only [comp_id]
clear_value kf gf hf
clear w
let O := (Finset.univ.biUnion fun j => Finset.univ.biUnion fun j' => Finset.univ.image (@kf j j')) ∪ { k' }
have kfO : ∀ {j j'} (f : j ⟶ j'), kf f ∈ O := fun {j} {j'} f =>
Finset.mem_union.mpr
(Or.inl
(Finset.mem_biUnion.mpr
⟨j, Finset.mem_univ j,
Finset.mem_biUnion.mpr ⟨j', Finset.mem_univ j', Finset.mem_image.mpr ⟨f, Finset.mem_univ _, rfl⟩⟩⟩))
have k'O : k' ∈ O := Finset.mem_union.mpr (Or.inr (Finset.mem_singleton.mpr rfl))
let H : Finset (Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
Finset.univ.biUnion fun j : J =>
Finset.univ.biUnion fun j' : J =>
Finset.univ.biUnion fun f : j ⟶ j' => {⟨k', kf f, k'O, kfO f, gf f⟩, ⟨k', kf f, k'O, kfO f, hf f⟩}
obtain ⟨k'', i', s'⟩ := IsFiltered.sup_exists O H
let i : ∀ {j j'} (f : j ⟶ j'), kf f ⟶ k'' := fun {j} {j'} f => i' (kfO f)
have s : ∀ {j₁ j₂ j₃ j₄} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f' :=
by
intro j₁ j₂ j₃ j₄ f f'
rw [s', s']
· exact k'O
·
exact
Finset.mem_biUnion.mpr
⟨j₃, Finset.mem_univ _,
Finset.mem_biUnion.mpr
⟨j₄, Finset.mem_univ _,
Finset.mem_biUnion.mpr
⟨f', Finset.mem_univ _, by
-- This works by `simp`, but has very high variation in heartbeats.
rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq,
heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self, true_and, eq_self, true_and,
eq_self, true_and, Finset.mem_singleton, eq_self, or_true]
trivial⟩⟩⟩
·
exact
Finset.mem_biUnion.mpr
⟨j₁, Finset.mem_univ _,
Finset.mem_biUnion.mpr
⟨j₂, Finset.mem_univ _,
Finset.mem_biUnion.mpr
⟨f, Finset.mem_univ _, by
-- This works by `simp`, but has very high variation in heartbeats.
rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq,
heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self, true_and, eq_self, true_and,
eq_self, true_and, Finset.mem_singleton, eq_self, true_or]
trivial⟩⟩⟩
clear_value i
clear s' i' H kfO k'O O
fconstructor
· -- We construct the pre-image (which, recall is meant to be a point
-- in the colimit (over `K`) of the limits (over `J`)) via a representative at `k''`.
apply colimit.ι (curry.obj (swap K J ⋙ F) ⋙ Limits.lim) k'' _
dsimp
-- This representative is meant to be an element of a limit,
-- so we need to construct a family of elements in `F.obj (j, k'')` for varying `j`,
-- then show that are coherent with respect to morphisms in the `j` direction.
apply Limit.mk
swap
· -- We construct the elements as the images of the `y j`.
exact fun j => F.map (𝟙 j ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j)
· -- After which it's just a calculation, using `s` and `wf`, to see they are coherent.
dsimp
intro j j' f
simp only [← FunctorToTypes.map_comp_apply, prod_comp, id_comp, comp_id]
calc
F.map (f ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j) = F.map (f ×ₘ (g j ≫ hf f ≫ i f)) (y j) := by rw [s (𝟙 j) f]
_ = F.map (𝟙 j' ×ₘ i f) (F.map (f ×ₘ (g j ≫ hf f)) (y j)) := by
rw [← FunctorToTypes.map_comp_apply, prod_comp, comp_id, assoc]
_ = F.map (𝟙 j' ×ₘ i f) (F.map (𝟙 j' ×ₘ (g j' ≫ gf f)) (y j')) := by rw [← wf f]
_ = F.map (𝟙 j' ×ₘ (g j' ≫ gf f ≫ i f)) (y j') := by
rw [← FunctorToTypes.map_comp_apply, prod_comp, id_comp, assoc]
_ = F.map (𝟙 j' ×ₘ (g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) (y j') := by
rw [s f (𝟙 j'), ← s (𝟙 j') (𝟙 j')]
-- Finally we check that this maps to `x`.
· -- We can do this componentwise:
apply limit_ext
intro j
simp only [id, ← e, Limits.ι_colimitLimitToLimitColimit_π_apply, colimit_eq_iff, Bifunctor.map_id_comp,
types_comp_apply, curry_obj_obj_map, Functor.comp_obj, colim_obj, Limit.π_mk]
refine ⟨k'', 𝟙 k'', g j ≫ gf (𝟙 j) ≫ i (𝟙 j), ?_⟩
rw [Bifunctor.map_id_comp, Bifunctor.map_id_comp, types_comp_apply, types_comp_apply, Bifunctor.map_id,
types_id_apply]
