# Documentation

Mathlib.CategoryTheory.Limits.ConcreteCategory

# Facts about (co)limits of functors into concrete categories #

theorem CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit {C : Type u} {J : Type w} (F : ) {D : } (hD : ) :
Function.Injective fun x j => ↑(D.app j) x
theorem CategoryTheory.Limits.Concrete.isLimit_ext {C : Type u} {J : Type w} (F : ) {D : } (hD : ) (x : ().obj D.pt) (y : ().obj D.pt) :
(∀ (j : J), ↑(D.app j) x = ↑(D.app j) y) → x = y
theorem CategoryTheory.Limits.Concrete.limit_ext {C : Type u} {J : Type w} (F : ) (x : ().obj ()) (y : ().obj ()) :
(∀ (j : J), ↑() x = ↑() y) → x = y
theorem CategoryTheory.Limits.Concrete.widePullback_ext {C : Type u} {B : C} {ι : Type w} {X : ιC} (f : (j : ι) → X j B) (x : ().obj ()) (y : ().obj ()) (h₀ : ) (h : ∀ (j : ι), ) :
x = y
theorem CategoryTheory.Limits.Concrete.widePullback_ext' {C : Type u} {B : C} {ι : Type w} [] {X : ιC} (f : (j : ι) → X j B) (x : ().obj ()) (y : ().obj ()) (h : ∀ (j : ι), ) :
x = y
theorem CategoryTheory.Limits.Concrete.multiequalizer_ext {C : Type u} (x : ) (y : ) (h : ∀ (t : I.L), ) :
x = y
def CategoryTheory.Limits.Concrete.multiequalizerEquivAux {C : Type u} :
{ x // ∀ (i : I.R), }

An auxiliary equivalence to be used in multiequalizerEquiv below.

Instances For
noncomputable def CategoryTheory.Limits.Concrete.multiequalizerEquiv {C : Type u} :
{ x // ∀ (i : I.R), }

The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.

Instances For
@[simp]
theorem CategoryTheory.Limits.cokernel_funext {C : Type u_1} [] {M : C} {N : C} {K : C} {f : M N} {g : } {h : } (w : ∀ (n : ().obj N), g () = h ()) :
g = h
theorem CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit {C : Type u} {J : Type v} (F : ) {D : } (hD : ) :
let ff := fun a => ↑(D.app a.fst) a.snd;
theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep {C : Type u} {J : Type v} (F : ) {D : } (hD : ) (x : ().obj D.pt) :
j y, ↑(D.app j) y = x
theorem CategoryTheory.Limits.Concrete.colimit_exists_rep {C : Type u} {J : Type v} (F : ) (x : ().obj ()) :
j y, ↑() y = x
theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists {C : Type u} {J : Type v} (F : ) {D : } {i : J} {j : J} (hD : ) (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) (h : k f g, ↑(F.map f) x = ↑(F.map g) y) :
↑(D.app i) x = ↑(D.app j) y
theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists {C : Type u} {J : Type v} (F : ) {i : J} {j : J} (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) (h : k f g, ↑(F.map f) x = ↑(F.map g) y) :
↑() x = ↑() y
theorem CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq {C : Type u} {J : Type v} (F : ) {D : } {i : J} {j : J} (hD : ) (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) (h : ↑(D.app i) x = ↑(D.app j) y) :
k f g, ↑(F.map f) x = ↑(F.map g) y
theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists {C : Type u} {J : Type v} (F : ) {D : } {i : J} {j : J} (hD : ) (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) :
↑(D.app i) x = ↑(D.app j) y k f g, ↑(F.map f) x = ↑(F.map g) y
theorem CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq {C : Type u} {J : Type v} (F : ) {i : J} {j : J} (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) (h : ↑() x = ↑() y) :
k f g, ↑(F.map f) x = ↑(F.map g) y
theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists {C : Type u} {J : Type v} (F : ) {i : J} {j : J} (x : ().obj (F.obj i)) (y : ().obj (F.obj j)) :
↑() x = ↑() y k f g, ↑(F.map f) x = ↑(F.map g) y
theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep {C : Type u} {B : C} {α : Type v} {X : αC} (f : (j : α) → B X j) (x : ().obj ()) :
(y, ) i y, = x
theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep' {C : Type u} {B : C} {α : Type v} [] {X : αC} (f : (j : α) → B X j) (x : ().obj ()) :
i y, = x