# mathlib3documentation

category_theory.limits.concrete_category

# 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} {J : Type w} (F : J C)  :
function.injective (λ (x : (D.X)) (j : J), (D.π.app j) x)
theorem category_theory.limits.concrete.is_limit_ext {C : Type u} {J : Type w} (F : J C) (x y : (D.X)) :
( (j : J), (D.π.app j) x = (D.π.app j) y) x = y
theorem category_theory.limits.concrete.limit_ext {C : Type u} {J : Type w} (F : J C) (x y : ) :
( (j : J), = y) x = y
theorem category_theory.limits.concrete.wide_pullback_ext {C : Type u} {B : C} {ι : Type w} {X : ι C} (f : Π (j : ι), X j B) (x y : ) (h : (j : ι), ) :
x = y
theorem category_theory.limits.concrete.wide_pullback_ext' {C : Type u} {B : C} {ι : Type w} [nonempty ι] {X : ι C} (f : Π (j : ι), X j B) (x y : ) (h : (j : ι), ) :
x = y
theorem category_theory.limits.concrete.multiequalizer_ext {C : Type u} (x y : ) (h : (t : I.L), ) :
x = y
def category_theory.limits.concrete.multiequalizer_equiv_aux {C : Type u}  :
.sections) {x // (i : I.R), (I.fst i) (x (I.fst_to i)) = (I.snd i) (x (I.snd_to i))}

An auxiliary equivalence to be used in multiequalizer_equiv below.

Equations
noncomputable def category_theory.limits.concrete.multiequalizer_equiv {C : Type u}  :
{x // (i : I.R), (I.fst i) (x (I.fst_to i)) = (I.snd i) (x (I.snd_to i))}

The equivalence between the noncomputable multiequalizer and and the concrete multiequalizer.

Equations
@[simp]
theorem category_theory.limits.cokernel_funext {C : Type u_1} {M N K : C} {f : M N} {g h : K} (w : (n : N), g = h ) :
g = h
theorem category_theory.limits.concrete.from_union_surjective_of_is_colimit {C : Type u} {J : Type v} (F : J C)  :
let ff : (Σ (j : J), (F.obj j)) (D.X) := λ (a : Σ (j : J), (F.obj j)), (D.ι.app a.fst) a.snd in
theorem category_theory.limits.concrete.is_colimit_exists_rep {C : Type u} {J : Type v} (F : J C) (x : (D.X)) :
(j : J) (y : (F.obj j)), (D.ι.app j) y = x
theorem category_theory.limits.concrete.colimit_exists_rep {C : Type u} {J : Type v} (F : J C) (x : ) :
(j : J) (y : (F.obj j)), = x
theorem category_theory.limits.concrete.is_colimit_rep_eq_of_exists {C : Type u} {J : Type v} (F : J C) {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) :
(D.ι.app i) x = (D.ι.app j) y
theorem category_theory.limits.concrete.colimit_rep_eq_of_exists {C : Type u} {J : Type v} (F : J C) {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) :
theorem category_theory.limits.concrete.is_colimit_exists_of_rep_eq {C : Type u} {J : Type v} (F : J C) {i j : J} (x : (F.obj i)) (y : (F.obj j)) (h : (D.ι.app i) x = (D.ι.app j) y) :
(k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem category_theory.limits.concrete.is_colimit_rep_eq_iff_exists {C : Type u} {J : Type v} (F : J C) {i j : J} (x : (F.obj i)) (y : (F.obj j)) :
(D.ι.app i) x = (D.ι.app j) y (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem category_theory.limits.concrete.colimit_exists_of_rep_eq {C : Type u} {J : Type v} (F : J C) {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
theorem category_theory.limits.concrete.colimit_rep_eq_iff_exists {C : Type u} {J : Type v} (F : J C) {i j : J} (x : (F.obj i)) (y : (F.obj j)) :
(k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem category_theory.limits.concrete.wide_pushout_exists_rep {C : Type u} {B : C} {α : Type v} {X : α C} (f : Π (j : α), B X j) (x : ) :
( (y : B), (i : α) (y : (X i)),
theorem category_theory.limits.concrete.wide_pushout_exists_rep' {C : Type u} {B : C} {α : Type v} [nonempty α] {X : α C} (f : Π (j : α), B X j) (x : ) :
(i : α) (y : (X i)),