Facts about (co)limits of functors into concrete categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
category_theory.limits.concrete.to_product_injective_of_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F (category_theory.forget C)]
{D : category_theory.limits.cone F}
(hD : category_theory.limits.is_limit D) :
theorem
category_theory.limits.concrete.is_limit_ext
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F (category_theory.forget C)]
{D : category_theory.limits.cone F}
(hD : category_theory.limits.is_limit D)
(x y : ↥(D.X)) :
theorem
category_theory.limits.concrete.limit_ext
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type w}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F (category_theory.forget C)]
[category_theory.limits.has_limit F]
(x y : ↥(category_theory.limits.limit F)) :
(∀ (j : J), ⇑(category_theory.limits.limit.π F j) x = ⇑(category_theory.limits.limit.π F j) y) → x = y
theorem
category_theory.limits.concrete.wide_pullback_ext
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{B : C}
{ι : Type w}
{X : ι → C}
(f : Π (j : ι), X j ⟶ B)
[category_theory.limits.has_wide_pullback B X f]
[category_theory.limits.preserves_limit (category_theory.limits.wide_pullback_shape.wide_cospan B X f) (category_theory.forget C)]
(x y : ↥(category_theory.limits.wide_pullback B X f))
(h₀ : ⇑(category_theory.limits.wide_pullback.base f) x = ⇑(category_theory.limits.wide_pullback.base f) y)
(h : ∀ (j : ι), ⇑(category_theory.limits.wide_pullback.π f j) x = ⇑(category_theory.limits.wide_pullback.π f j) y) :
x = y
theorem
category_theory.limits.concrete.wide_pullback_ext'
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{B : C}
{ι : Type w}
[nonempty ι]
{X : ι → C}
(f : Π (j : ι), X j ⟶ B)
[category_theory.limits.has_wide_pullback B X f]
[category_theory.limits.preserves_limit (category_theory.limits.wide_pullback_shape.wide_cospan B X f) (category_theory.forget C)]
(x y : ↥(category_theory.limits.wide_pullback B X f))
(h : ∀ (j : ι), ⇑(category_theory.limits.wide_pullback.π f j) x = ⇑(category_theory.limits.wide_pullback.π f j) y) :
x = y
theorem
category_theory.limits.concrete.multiequalizer_ext
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{I : category_theory.limits.multicospan_index C}
[category_theory.limits.has_multiequalizer I]
[category_theory.limits.preserves_limit I.multicospan (category_theory.forget C)]
(x y : ↥(category_theory.limits.multiequalizer I))
(h : ∀ (t : I.L), ⇑(category_theory.limits.multiequalizer.ι I t) x = ⇑(category_theory.limits.multiequalizer.ι I t) y) :
x = y
def
category_theory.limits.concrete.multiequalizer_equiv_aux
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
(I : category_theory.limits.multicospan_index C) :
An auxiliary equivalence to be used in multiequalizer_equiv below.
Equations
- category_theory.limits.concrete.multiequalizer_equiv_aux I = {to_fun := λ (x : ↥((I.multicospan ⋙ category_theory.forget C).sections)), ⟨λ (i : I.L), x.val (category_theory.limits.walking_multicospan.left i), _⟩, inv_fun := λ (x : {x // ∀ (i : I.R), ⇑(I.fst i) (x (I.fst_to i)) = ⇑(I.snd i) (x (I.snd_to i))}), ⟨λ (j : category_theory.limits.walking_multicospan I.fst_to I.snd_to), category_theory.limits.concrete.multiequalizer_equiv_aux._match_1 I x j, _⟩, left_inv := _, right_inv := _}
- category_theory.limits.concrete.multiequalizer_equiv_aux._match_1 I x (category_theory.limits.walking_multicospan.right b) = ⇑(I.fst b) (x.val (I.fst_to b))
- category_theory.limits.concrete.multiequalizer_equiv_aux._match_1 I x (category_theory.limits.walking_multicospan.left a) = x.val a
noncomputable
def
category_theory.limits.concrete.multiequalizer_equiv
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
(I : category_theory.limits.multicospan_index C)
[category_theory.limits.has_multiequalizer I]
[category_theory.limits.preserves_limit I.multicospan (category_theory.forget C)] :
The equivalence between the noncomputable multiequalizer and and the concrete multiequalizer.
Equations
- category_theory.limits.concrete.multiequalizer_equiv I = let h1 : category_theory.limits.is_limit (category_theory.limits.limit.cone I.multicospan) := category_theory.limits.limit.is_limit I.multicospan, h2 : category_theory.limits.is_limit ((category_theory.forget C).map_cone (category_theory.limits.limit.cone I.multicospan)) := category_theory.limits.is_limit_of_preserves (category_theory.forget C) h1, E : ((category_theory.forget C).map_cone (category_theory.limits.limit.cone I.multicospan)).X ≅ (category_theory.limits.types.limit_cone (I.multicospan ⋙ category_theory.forget C)).X := h2.cone_point_unique_up_to_iso (category_theory.limits.types.limit_cone_is_limit (I.multicospan ⋙ category_theory.forget C)) in E.to_equiv.trans (category_theory.limits.concrete.multiequalizer_equiv_aux I)
@[simp]
theorem
category_theory.limits.concrete.multiequalizer_equiv_apply
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
(I : category_theory.limits.multicospan_index C)
[category_theory.limits.has_multiequalizer I]
[category_theory.limits.preserves_limit I.multicospan (category_theory.forget C)]
(x : ↥(category_theory.limits.multiequalizer I))
(i : I.L) :
theorem
category_theory.limits.cokernel_funext
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.concrete_category C]
{M N K : C}
{f : M ⟶ N}
[category_theory.limits.has_cokernel f]
{g h : category_theory.limits.cokernel f ⟶ K}
(w : ∀ (n : ↥N), ⇑g (⇑(category_theory.limits.cokernel.π f) n) = ⇑h (⇑(category_theory.limits.cokernel.π f) n)) :
g = h
theorem
category_theory.limits.concrete.from_union_surjective_of_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
{D : category_theory.limits.cocone F}
(hD : category_theory.limits.is_colimit D) :
theorem
category_theory.limits.concrete.is_colimit_exists_rep
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
{D : category_theory.limits.cocone F}
(hD : category_theory.limits.is_colimit D)
(x : ↥(D.X)) :
theorem
category_theory.limits.concrete.colimit_exists_rep
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.limits.has_colimit F]
(x : ↥(category_theory.limits.colimit F)) :
theorem
category_theory.limits.concrete.is_colimit_rep_eq_of_exists
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
{D : category_theory.limits.cocone F}
{i j : J}
(hD : category_theory.limits.is_colimit D)
(x : ↥(F.obj i))
(y : ↥(F.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), ⇑(F.map f) x = ⇑(F.map g) y) :
theorem
category_theory.limits.concrete.colimit_rep_eq_of_exists
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.limits.has_colimit F]
{i j : J}
(x : ↥(F.obj i))
(y : ↥(F.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), ⇑(F.map f) x = ⇑(F.map g) y) :
⇑(category_theory.limits.colimit.ι F i) x = ⇑(category_theory.limits.colimit.ι F j) y
theorem
category_theory.limits.concrete.is_colimit_exists_of_rep_eq
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.is_filtered J]
{D : category_theory.limits.cocone F}
{i j : J}
(hD : category_theory.limits.is_colimit D)
(x : ↥(F.obj i))
(y : ↥(F.obj j))
(h : ⇑(D.ι.app i) x = ⇑(D.ι.app j) y) :
theorem
category_theory.limits.concrete.is_colimit_rep_eq_iff_exists
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.is_filtered J]
{D : category_theory.limits.cocone F}
{i j : J}
(hD : category_theory.limits.is_colimit D)
(x : ↥(F.obj i))
(y : ↥(F.obj j)) :
theorem
category_theory.limits.concrete.colimit_exists_of_rep_eq
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.is_filtered J]
[category_theory.limits.has_colimit F]
{i j : J}
(x : ↥(F.obj i))
(y : ↥(F.obj j))
(h : ⇑(category_theory.limits.colimit.ι F i) x = ⇑(category_theory.limits.colimit.ι F j) y) :
theorem
category_theory.limits.concrete.colimit_rep_eq_iff_exists
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F (category_theory.forget C)]
[category_theory.is_filtered J]
[category_theory.limits.has_colimit F]
{i j : J}
(x : ↥(F.obj i))
(y : ↥(F.obj j)) :
theorem
category_theory.limits.concrete.wide_pushout_exists_rep
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{B : C}
{α : Type v}
{X : α → C}
(f : Π (j : α), B ⟶ X j)
[category_theory.limits.has_wide_pushout B X f]
[category_theory.limits.preserves_colimit (category_theory.limits.wide_pushout_shape.wide_span B X f) (category_theory.forget C)]
(x : ↥(category_theory.limits.wide_pushout B X f)) :
theorem
category_theory.limits.concrete.wide_pushout_exists_rep'
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
{B : C}
{α : Type v}
[nonempty α]
{X : α → C}
(f : Π (j : α), B ⟶ X j)
[category_theory.limits.has_wide_pushout B X f]
[category_theory.limits.preserves_colimit (category_theory.limits.wide_pushout_shape.wide_span B X f) (category_theory.forget C)]
(x : ↥(category_theory.limits.wide_pushout B X f)) :