Facts about (co)limits of functors into concrete categories #
theorem
CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cone F}
(hD : CategoryTheory.Limits.IsLimit D)
:
Function.Injective fun x j => ↑(D.π.app j) x
theorem
CategoryTheory.Limits.Concrete.isLimit_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cone F}
(hD : CategoryTheory.Limits.IsLimit D)
(x : (CategoryTheory.forget C).obj D.pt)
(y : (CategoryTheory.forget C).obj D.pt)
:
theorem
CategoryTheory.Limits.Concrete.limit_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimit F]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.limit F))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.limit F))
:
(∀ (j : J), ↑(CategoryTheory.Limits.limit.π F j) x = ↑(CategoryTheory.Limits.limit.π F j) y) → x = y
theorem
CategoryTheory.Limits.Concrete.widePullback_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{ι : Type w}
{X : ι → C}
(f : (j : ι) → X j ⟶ B)
[CategoryTheory.Limits.HasWidePullback B X f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
(CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(h₀ : ↑(CategoryTheory.Limits.WidePullback.base f) x = ↑(CategoryTheory.Limits.WidePullback.base f) y)
(h : ∀ (j : ι), ↑(CategoryTheory.Limits.WidePullback.π f j) x = ↑(CategoryTheory.Limits.WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.widePullback_ext'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{ι : Type w}
[Nonempty ι]
{X : ι → C}
(f : (j : ι) → X j ⟶ B)
[CategoryTheory.Limits.HasWidePullback B X f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
(CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePullback B X f))
(h : ∀ (j : ι), ↑(CategoryTheory.Limits.WidePullback.π f j) x = ↑(CategoryTheory.Limits.WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.multiequalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{I : CategoryTheory.Limits.MulticospanIndex C}
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(y : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(h : ∀ (t : I.L), ↑(CategoryTheory.Limits.Multiequalizer.ι I t) x = ↑(CategoryTheory.Limits.Multiequalizer.ι I t) y)
:
x = y
def
CategoryTheory.Limits.Concrete.multiequalizerEquivAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
:
↑(CategoryTheory.Functor.sections
(CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.forget C))) ≃ { x //
∀ (i : I.R),
↑(CategoryTheory.Limits.MulticospanIndex.fst I i) (x (CategoryTheory.Limits.MulticospanIndex.fstTo I i)) = ↑(CategoryTheory.Limits.MulticospanIndex.snd I i) (x (CategoryTheory.Limits.MulticospanIndex.sndTo I i)) }
An auxiliary equivalence to be used in multiequalizerEquiv below.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.multiequalizerEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.forget C)]
:
(CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I) ≃ { x //
∀ (i : I.R),
↑(CategoryTheory.Limits.MulticospanIndex.fst I i) (x (CategoryTheory.Limits.MulticospanIndex.fstTo I i)) = ↑(CategoryTheory.Limits.MulticospanIndex.snd I i) (x (CategoryTheory.Limits.MulticospanIndex.sndTo I i)) }
The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
(I : CategoryTheory.Limits.MulticospanIndex C)
[CategoryTheory.Limits.HasMultiequalizer I]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.multiequalizer I))
(i : I.L)
:
↑(↑(CategoryTheory.Limits.Concrete.multiequalizerEquiv I) x) i = ↑(CategoryTheory.Limits.Multiequalizer.ι I i) x
theorem
CategoryTheory.Limits.cokernel_funext
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.ConcreteCategory C]
{M : C}
{N : C}
{K : C}
{f : M ⟶ N}
[CategoryTheory.Limits.HasCokernel f]
{g : CategoryTheory.Limits.cokernel f ⟶ K}
{h : CategoryTheory.Limits.cokernel f ⟶ K}
(w : ∀ (n : (CategoryTheory.forget C).obj N),
↑g (↑(CategoryTheory.Limits.cokernel.π f) n) = ↑h (↑(CategoryTheory.Limits.cokernel.π f) n))
:
g = h
theorem
CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
(hD : CategoryTheory.Limits.IsColimit D)
:
let ff := fun a => ↑(D.ι.app a.fst) a.snd;
Function.Surjective ff
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).obj D.pt)
:
∃ j y, ↑(D.ι.app j) y = x
theorem
CategoryTheory.Limits.Concrete.colimit_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasColimit F]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.colimit F))
:
∃ j y, ↑(CategoryTheory.Limits.colimit.ι F j) y = x
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
(h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y)
:
↑(CategoryTheory.Limits.colimit.ι F i) x = ↑(CategoryTheory.Limits.colimit.ι F j) y
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
(h : ↑(CategoryTheory.Limits.colimit.ι F i) x = ↑(CategoryTheory.Limits.colimit.ι F j) y)
:
∃ k f g, ↑(F.map f) x = ↑(F.map g) y
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
:
↑(CategoryTheory.Limits.colimit.ι F i) x = ↑(CategoryTheory.Limits.colimit.ι F j) y ↔ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{α : Type v}
{X : α → C}
(f : (j : α) → B ⟶ X j)
[CategoryTheory.Limits.HasWidePushout B X f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f))
:
(∃ y, ↑(CategoryTheory.Limits.WidePushout.head f) y = x) ∨ ∃ i y, ↑(CategoryTheory.Limits.WidePushout.ι f i) y = x
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{B : C}
{α : Type v}
[Nonempty α]
{X : α → C}
(f : (j : α) → B ⟶ X j)
[CategoryTheory.Limits.HasWidePushout B X f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f) (CategoryTheory.forget C)]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.widePushout B X f))
:
∃ i y, ↑(CategoryTheory.Limits.WidePushout.ι f i) y = x