English
Under finite index J and filtered K, the canonical map colimitLimitToLimitColimit F is injective.
Русский
При конечном индексе J и фильтрованном K каноническое отображение colimitLimitToLimitColimit F инъективно.
LaTeX
$$HasFilteredColimitsOfSize.{max w' w₂', max w w₂} C ⟹ Injective (colimitLimitToLimitColimit F)$$
Lean4
/-- This follows this proof from
* Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
-/
theorem colimitLimitToLimitColimit_injective : Function.Injective (colimitLimitToLimitColimit F) := by
classical
cases nonempty_fintype J
intro x y h
obtain ⟨kx, x, rfl⟩ := jointly_surjective' x
obtain ⟨ky, y, rfl⟩ := jointly_surjective' y
dsimp at x y
replace h := fun j => congr_arg (limit.π (curry.obj F ⋙ colim) j) h
simp? [colimit_eq_iff] at h says
simp only [comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply, colimit_eq_iff, curry_obj_obj_obj,
curry_obj_obj_map] at h
let k j := (h j).choose
let f : ∀ j, kx ⟶ k j := fun j => (h j).choose_spec.choose
let g : ∀ j, ky ⟶ k j := fun j => (h j).choose_spec.choose_spec.choose
have w :
∀ j,
F.map (𝟙 j ×ₘ f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
F.map (𝟙 j ×ₘ g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y) :=
fun j => (h j).choose_spec.choose_spec.choose_spec
let O : Finset K := Finset.univ.image k ∪ { kx, ky }
have kxO : kx ∈ O := Finset.mem_union.mpr (Or.inr (by simp))
have kyO : ky ∈ O := Finset.mem_union.mpr (Or.inr (by simp))
have kjO : ∀ j, k j ∈ O := fun j => Finset.mem_union.mpr (Or.inl (by simp))
let H : Finset (Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
(Finset.univ.image fun j : J => ⟨kx, k j, kxO, Finset.mem_union.mpr (Or.inl (by simp)), f j⟩) ∪
Finset.univ.image fun j : J => ⟨ky, k j, kyO, Finset.mem_union.mpr (Or.inl (by simp)), g j⟩
obtain ⟨S, T, W⟩ := IsFiltered.sup_exists O H
have fH : ∀ j, (⟨kx, k j, kxO, kjO j, f j⟩ : Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H := fun j =>
Finset.mem_union.mpr
(Or.inl
(by
simp only [true_and, Finset.mem_univ, Finset.mem_image]
refine ⟨j, ?_⟩
simp only))
have gH : ∀ j, (⟨ky, k j, kyO, kjO j, g j⟩ : Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H := fun j =>
Finset.mem_union.mpr
(Or.inr
(by
simp only [true_and, Finset.mem_univ, Finset.mem_image]
refine ⟨j, ?_⟩
simp only))
-- Our goal is now an equation between equivalence classes of representatives of a colimit,
-- and so it suffices to show those representative become equal somewhere, in particular at `S`.
apply
colimit_sound' (T kxO)
(T kyO)
-- We can check if two elements of a limit (in `Type`)
-- are equal by comparing them componentwise.
ext j
simp only [Functor.comp_map]
rw [← W _ _ (fH j), ← W _ _ (gH j)]
simp [w]
