def
category_theory.limits.types.limit_cone
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type
def
category_theory.limits.types.limit_cone_is_limit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
(internal implementation) the fact that the proposed limit cone is the limit
@[instance]
def
category_theory.limits.types.category_theory.limits.has_limits
:
category_theory.limits.has_limits (Type u)
Equations
- category_theory.limits.types.category_theory.limits.has_limits = {has_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Type u), {cone := category_theory.limits.types.limit_cone F, is_limit := category_theory.limits.types.limit_cone_is_limit F}}}
def
category_theory.limits.types.limit_equiv_sections
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
The equivalence between the abstract limit of F in Type u
and the "concrete" definition as the sections of F.
@[simp]
theorem
category_theory.limits.types.limit_equiv_sections_apply
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u)
(x : category_theory.limits.limit F)
(j : J) :
@[simp]
theorem
category_theory.limits.types.limit_equiv_sections_symm_apply
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u)
(x : ↥(F.sections))
(j : J) :
theorem
category_theory.limits.types.limit_ext
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u)
(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
@[simp]
theorem
category_theory.limits.types.lift_π_apply
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u)
(s : category_theory.limits.cone F)
(j : J)
(x : s.X) :
category_theory.limits.limit.π F j (category_theory.limits.limit.lift F s x) = s.π.app j x
@[nolint]
def
category_theory.limits.types.quot
{J : Type u}
[category_theory.small_category J] :
J ⥤ Type u → Type u
A quotient type implementing the colimit of a functor F : J ⥤ Type u,
as pairs ⟨j, x⟩ where x : F.obj j, modulo the equivalence relation generated by
⟨j, x⟩ ~ ⟨j', x'⟩ whenever there is a morphism f : j ⟶ j' so F.map f x = x'.
def
category_theory.limits.types.colimit_cocone
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type
def
category_theory.limits.types.colimit_cocone_is_colimit
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
(internal implementation) the fact that the proposed colimit cocone is the colimit
@[instance]
def
category_theory.limits.types.category_theory.limits.has_colimits
:
category_theory.limits.has_colimits (Type u)
Equations
- category_theory.limits.types.category_theory.limits.has_colimits = {has_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ Type u), {cocone := category_theory.limits.types.colimit_cocone F, is_colimit := category_theory.limits.types.colimit_cocone_is_colimit F}}}
def
category_theory.limits.types.colimit_equiv_quot
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u) :
The equivalence between the abstract colimit of F in Type u
and the "concrete" definition as a quotient.
@[simp]
theorem
category_theory.limits.types.colimit_equiv_quot_symm_apply
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Type u)
(j : J)
(x : F.obj j) :
the image of a morphism in Type is just set.range f
Equations
@[instance]
Equations
- category_theory.limits.types.inhabited f = {default := ⟨f (inhabited.default α), _⟩}
the inclusion of image f into the target
Equations
@[instance]
Equations
- _ = _
def
category_theory.limits.types.image.lift
{α β : Type u}
{f : α ⟶ β}
(F' : category_theory.limits.mono_factorisation f) :
the universal property for the image factorisation
Equations
- category_theory.limits.types.image.lift F' = λ (x : category_theory.limits.types.image f), F'.e (classical.indefinite_description (λ (y : α), f y = x.val) _).val
theorem
category_theory.limits.types.image.lift_fac
{α β : Type u}
{f : α ⟶ β}
(F' : category_theory.limits.mono_factorisation f) :
the factorisation of any morphism in AddCommGroup through a mono.
Equations
- category_theory.limits.types.mono_factorisation f = {I := category_theory.limits.types.image f, m := category_theory.limits.types.image.ι f, m_mono := _, e := set.range_factorization f, fac' := _}
@[instance]
@[instance]
def
category_theory.limits.types.category_theory.limits.has_images
:
category_theory.limits.has_images (Type u)
Equations
- category_theory.limits.types.category_theory.limits.has_images = {has_image := infer_instance (λ {X Y : Type u} (f : X ⟶ Y), category_theory.limits.types.category_theory.limits.has_image f)}
@[instance]
Equations
- category_theory.limits.types.category_theory.limits.has_image_maps = {has_image_map := λ (f g : category_theory.arrow (Type u)) (st : f ⟶ g), {map := λ (x : category_theory.limits.image f.hom), ⟨st.right x.val, _⟩, map_ι' := _}}
@[simp]
theorem
category_theory.limits.types.image_map
{f g : category_theory.arrow (Type u)}
(st : f ⟶ g)
(x : category_theory.limits.types.image f.hom) :
(category_theory.limits.image.map st x).val = st.right x.val