Existence of limits and colimits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In category_theory.limits.is_limit we defined is_limit c,
the data showing that a cone c is a limit cone.
The two main structures defined in this file are:
limit_cone F, which consists of a choice of cone forFand the fact it is a limit cone, andhas_limit F, asserting the mere existence of some limit cone forF.
has_limit is a propositional typeclass
(it's important that it is a proposition merely asserting the existence of a limit,
as otherwise we would have non-defeq problems from incompatible instances).
While has_limit only asserts the existence of a limit cone,
we happily use the axiom of choice in mathlib,
so there are convenience functions all depending on has_limit F:
limit F : C, producing some limit object (of course all such are isomorphic)limit.π F j : limit F ⟶ F.obj j, the morphisms out of the limit,limit.lift F c : c.X ⟶ limit F, the universal morphism from any otherc : cone F, etc.
Key to using the has_limit interface is that there is an @[ext] lemma stating that
to check f = g, for f g : Z ⟶ limit F, it suffices to check f ≫ limit.π F j = g ≫ limit.π F j
for every j.
This, combined with @[simp] lemmas, makes it possible to prove many easy facts about limits using
automation (e.g. tidy).
There are abbreviations has_limits_of_shape J C and has_limits C
asserting the existence of classes of limits.
Later more are introduced, for finite limits, special shapes of limits, etc.
Ideally, many results about limits should be stated first in terms of is_limit,
and then a result in terms of has_limit derived from this.
At this point, however, this is far from uniformly achieved in mathlib ---
often statements are only written in terms of has_limit.
Implementation #
At present we simply say everything twice, in order to handle both limits and colimits.
It would be highly desirable to have some automation support,
e.g. a @[dualize] attribute that behaves similarly to @[to_additive].
References #
@[nolint]
structure
category_theory.limits.limit_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u u₁ v)
- cone : category_theory.limits.cone F
- is_limit : category_theory.limits.is_limit self.cone
limit_cone F contains a cone over F together with the information that it is a limit.
Instances for category_theory.limits.limit_cone
- category_theory.limits.limit_cone.has_sizeof_inst
@[class]
structure
category_theory.limits.has_limit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Prop
- exists_limit : nonempty (category_theory.limits.limit_cone F)
has_limit F represents the mere existence of a limit for F.
Instances of this typeclass
- category_theory.limits.has_limit_of_has_limits_of_shape
- category_theory.limits.has_product_unique
- category_theory.limits.has_kernels.has_limit
- category_theory.limits.has_product_of_has_biproduct
- category_theory.limits.has_limit_equivalence_comp
- category_theory.limits.obj.has_limit
- category_theory.limits.has_pullback_of_comp_mono
- category_theory.limits.has_pullback_of_right_factors_mono
- category_theory.limits.has_pullback_of_left_factors_mono
- category_theory.limits.has_kernel_pair_of_mono
- category_theory.limits.has_equalizer_of_self
- category_theory.limits.has_equalizer_comp_mono
- category_theory.limits.has_kernel_comp_mono
- category_theory.limits.has_kernel_iso_comp
- category_theory.limits.biproduct.π.has_kernel
- category_theory.limits.biproduct.to_subtype.has_kernel
- category_theory.limits.has_binary_biproduct.has_limit_pair
- category_theory.limits.biprod.fst.has_kernel
- category_theory.limits.biprod.snd.has_kernel
theorem
category_theory.limits.has_limit.mk
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(d : category_theory.limits.limit_cone F) :
noncomputable
def
category_theory.limits.get_limit_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
Use the axiom of choice to extract explicit limit_cone F from has_limit F.
@[class]
structure
category_theory.limits.has_limits_of_shape
(J : Type u₁)
[category_theory.category J]
(C : Type u)
[category_theory.category C] :
Prop
- has_limit : (∀ (F : J ⥤ C), category_theory.limits.has_limit F) . "apply_instance"
C has limits of shape J if there exists a limit for every functor F : J ⥤ C.
Instances of this typeclass
- category_theory.limits.has_zero_object.has_terminal
- category_theory.limits.has_limits_of_shape_of_has_limits
- category_theory.limits.has_pullbacks_of_has_wide_pullbacks
- category_theory.limits.has_limits_of_shape_of_has_finite_limits
- category_theory.limits.has_binary_products_of_has_binary_biproducts
- category_theory.limits.has_terminal_op_of_has_initial
- category_theory.limits.has_limits_of_shape_wide_pullback_shape
- category_theory.limits.has_limits_of_shape_discrete
@[class]
structure
category_theory.limits.has_limits_of_size
(C : Type u)
[category_theory.category C] :
Prop
- has_limits_of_shape : (∀ (J : Type ?) [𝒥 : category_theory.category J], category_theory.limits.has_limits_of_shape J C) . "apply_instance"
C has all limits of size v₁ u₁ (has_limits_of_size.{v₁ u₁} C)
if it has limits of every shape J : Type u₁ with [category.{v₁} J].
Instances of this typeclass
@[reducible]
C has all (small) limits if it has limits of every shape that is as big as its hom-sets.
theorem
category_theory.limits.has_limits.has_limits_of_shape
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
(J : Type v)
[category_theory.category J] :
@[protected, instance]
def
category_theory.limits.has_limit_of_has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
[H : category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ C) :
@[protected, instance]
def
category_theory.limits.has_limits_of_shape_of_has_limits
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
[H : category_theory.limits.has_limits_of_size C] :
noncomputable
def
category_theory.limits.limit.cone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
An arbitrary choice of limit cone for a functor.
Equations
noncomputable
def
category_theory.limits.limit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
C
An arbitrary choice of limit object of a functor.
Equations
noncomputable
def
category_theory.limits.limit.π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(j : J) :
category_theory.limits.limit F ⟶ F.obj j
The projection from the limit object to a value of the functor.
Equations
Instances for category_theory.limits.limit.π
- category_theory.limits.is_iso_π_initial
- category_theory.limits.is_iso_π_terminal
- category_theory.limits.pullback.fst_of_mono
- category_theory.limits.pullback.snd_of_mono
- category_theory.limits.pullback_snd_iso_of_left_iso
- category_theory.limits.pullback_snd_iso_of_right_factors_mono
- category_theory.limits.pullback_snd_iso_of_right_iso
- category_theory.limits.pullback_snd_iso_of_left_factors_mono
- category_theory.limits.fst_iso_of_mono_eq
- category_theory.limits.snd_iso_of_mono_eq
- category_theory.limits.equalizer.ι_mono
- category_theory.limits.equalizer.ι_of_self
- category_theory.limits.is_split_epi_pi_π
- category_theory.limits.is_split_epi_prod_fst
- category_theory.limits.is_split_epi_prod_snd
- category_theory.limits.kernel.ι_zero_is_iso
- category_theory.limits.kernel.of_cokernel_of_epi
@[simp]
theorem
category_theory.limits.limit.cone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F] :
@[simp]
theorem
category_theory.limits.limit.cone_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F] :
@[simp]
theorem
category_theory.limits.limit.w
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{j j' : J}
(f : j ⟶ j') :
category_theory.limits.limit.π F j ≫ F.map f = category_theory.limits.limit.π F j'
@[simp]
theorem
category_theory.limits.limit.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{j j' : J}
(f : j ⟶ j')
{X' : C}
(f' : F.obj j' ⟶ X') :
category_theory.limits.limit.π F j ≫ F.map f ≫ f' = category_theory.limits.limit.π F j' ≫ f'
noncomputable
def
category_theory.limits.limit.is_limit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
Evidence that the arbitrary choice of cone provied by limit.cone F is a limit cone.
noncomputable
def
category_theory.limits.limit.lift
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
The morphism from the cone point of any other cone to the limit object.
Equations
@[simp]
theorem
category_theory.limits.limit.is_limit_lift
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.limit.lift_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.lift_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
category_theory.limits.limit.lift F c ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
noncomputable
def
category_theory.limits.lim_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G) :
Functoriality of limits.
Usually this morphism should be accessed through lim.map,
but may be needed separately when you have specified limits for the source and target functors,
but not necessarily for all functors of shape J.
Equations
Instances for category_theory.limits.lim_map
@[simp]
theorem
category_theory.limits.lim_map_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
category_theory.limits.lim_map α ≫ category_theory.limits.limit.π G j ≫ f' = category_theory.limits.limit.π F j ≫ α.app j ≫ f'
@[simp]
theorem
category_theory.limits.lim_map_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G)
(j : J) :
noncomputable
def
category_theory.limits.limit.cone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
The cone morphism from any cone to the arbitrary choice of limit cone.
@[simp]
theorem
category_theory.limits.limit.cone_morphism_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
theorem
category_theory.limits.limit.cone_morphism_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
(hc.cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit F)).hom ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
((category_theory.limits.limit.is_limit F).cone_point_unique_up_to_iso hc).inv ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J) :
theorem
category_theory.limits.limit.exists_unique
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.cone F) :
noncomputable
def
category_theory.limits.limit.iso_limit_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.limit_cone F) :
Given any other limit cone for F, the chosen limit F is isomorphic to the cone point.
@[simp]
theorem
category_theory.limits.limit.iso_limit_cone_hom_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.limit_cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.iso_limit_cone_hom_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.limit_cone F)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
(category_theory.limits.limit.iso_limit_cone t).hom ≫ t.cone.π.app j ≫ f' = category_theory.limits.limit.π F j ≫ f'
@[simp]
theorem
category_theory.limits.limit.iso_limit_cone_inv_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.limit_cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.iso_limit_cone_inv_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(t : category_theory.limits.limit_cone F)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
(category_theory.limits.limit.iso_limit_cone t).inv ≫ category_theory.limits.limit.π F j ≫ f' = t.cone.π.app j ≫ f'
@[ext]
theorem
category_theory.limits.limit.hom_ext
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{X : C}
{f f' : X ⟶ category_theory.limits.limit F}
(w : ∀ (j : J), f ≫ category_theory.limits.limit.π F j = f' ≫ category_theory.limits.limit.π F j) :
f = f'
@[simp]
theorem
category_theory.limits.limit.lift_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(c : category_theory.limits.cone F)
(α : F ⟶ G) :
@[simp]
theorem
category_theory.limits.limit.lift_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F] :
noncomputable
def
category_theory.limits.limit.hom_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(W : C) :
ulift (W ⟶ category_theory.limits.limit F) ≅ F.cones.obj (opposite.op W)
The isomorphism (in Type) between
morphisms from a specified object W to the limit object,
and cones with cone point W.
Equations
@[simp]
theorem
category_theory.limits.limit.hom_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{W : C}
(f : ulift (W ⟶ category_theory.limits.limit F)) :
noncomputable
def
category_theory.limits.limit.hom_iso'
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(W : C) :
The isomorphism (in Type) between
morphisms from a specified object W to the limit object,
and an explicit componentwise description of cones with cone point W.
Equations
theorem
category_theory.limits.limit.lift_extend
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
{X : C}
(f : X ⟶ c.X) :
theorem
category_theory.limits.has_limit_of_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
(α : F ≅ G) :
If a functor F has a limit, so does any naturally isomorphic functor.
theorem
category_theory.limits.has_limit.of_cones_iso
{C : Type u}
[category_theory.category C]
{J K : Type u₁}
[category_theory.category J]
[category_theory.category K]
(F : J ⥤ C)
(G : K ⥤ C)
(h : F.cones ≅ G.cones)
[category_theory.limits.has_limit F] :
If a functor G has the same collection of cones as a functor F
which has a limit, then G also has a limit.
noncomputable
def
category_theory.limits.has_limit.iso_of_nat_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G) :
The limits of F : J ⥤ C and G : J ⥤ C are isomorphic,
if the functors are naturally isomorphic.
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_hom_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J) :
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_hom_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
(category_theory.limits.has_limit.iso_of_nat_iso w).hom ≫ category_theory.limits.limit.π G j ≫ f' = category_theory.limits.limit.π F j ≫ w.hom.app j ≫ f'
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_inv_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J) :
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_inv_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
(category_theory.limits.has_limit.iso_of_nat_iso w).inv ≫ category_theory.limits.limit.π F j ≫ f' = category_theory.limits.limit.π G j ≫ w.inv.app j ≫ f'
@[simp]
theorem
category_theory.limits.has_limit.lift_iso_of_nat_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(t : category_theory.limits.cone F)
(w : F ≅ G) :
@[simp]
theorem
category_theory.limits.has_limit.lift_iso_of_nat_iso_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(t : category_theory.limits.cone F)
(w : F ≅ G)
{X' : C}
(f' : category_theory.limits.limit G ⟶ X') :
@[simp]
theorem
category_theory.limits.has_limit.lift_iso_of_nat_iso_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(t : category_theory.limits.cone G)
(w : F ≅ G) :
@[simp]
theorem
category_theory.limits.has_limit.lift_iso_of_nat_iso_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(t : category_theory.limits.cone G)
(w : F ≅ G)
{X' : C}
(f' : category_theory.limits.limit F ⟶ X') :
noncomputable
def
category_theory.limits.has_limit.iso_of_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{G : K ⥤ C}
[category_theory.limits.has_limit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
The limits of F : J ⥤ C and G : K ⥤ C are isomorphic,
if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.
@[simp]
theorem
category_theory.limits.has_limit.iso_of_equivalence_hom_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{G : K ⥤ C}
[category_theory.limits.has_limit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(k : K) :
@[simp]
theorem
category_theory.limits.has_limit.iso_of_equivalence_inv_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{G : K ⥤ C}
[category_theory.limits.has_limit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(j : J) :
noncomputable
def
category_theory.limits.limit.pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)] :
The canonical morphism from the limit of F to the limit of E ⋙ F.
@[simp]
theorem
category_theory.limits.limit.pre_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
(k : K) :
category_theory.limits.limit.pre F E ≫ category_theory.limits.limit.π (E ⋙ F) k = category_theory.limits.limit.π F (E.obj k)
@[simp]
theorem
category_theory.limits.limit.pre_π_assoc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
(k : K)
{X' : C}
(f' : (E ⋙ F).obj k ⟶ X') :
category_theory.limits.limit.pre F E ≫ category_theory.limits.limit.π (E ⋙ F) k ≫ f' = category_theory.limits.limit.π F (E.obj k) ≫ f'
@[simp]
theorem
category_theory.limits.limit.lift_pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.limit.pre_pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
{L : Type u₃}
[category_theory.category L]
(D : L ⥤ K)
[category_theory.limits.has_limit (D ⋙ E ⋙ F)] :
category_theory.limits.limit.pre F E ≫ category_theory.limits.limit.pre (E ⋙ F) D = category_theory.limits.limit.pre F (D ⋙ E)
theorem
category_theory.limits.limit.pre_eq
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{E : K ⥤ J}
[category_theory.limits.has_limit (E ⋙ F)]
(s : category_theory.limits.limit_cone (E ⋙ F))
(t : category_theory.limits.limit_cone F) :
- If we have particular limit cones available for
E ⋙ Fand forF, we obtain a formula forlimit.pre F E.
noncomputable
def
category_theory.limits.limit.post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)] :
G.obj (category_theory.limits.limit F) ⟶ category_theory.limits.limit (F ⋙ G)
The canonical morphism from G applied to the limit of F to the limit of F ⋙ G.
Equations
@[simp]
theorem
category_theory.limits.limit.post_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
(j : J)
{X' : D}
(f' : (F ⋙ G).obj j ⟶ X') :
category_theory.limits.limit.post F G ≫ category_theory.limits.limit.π (F ⋙ G) j ≫ f' = G.map (category_theory.limits.limit.π F j) ≫ f'
@[simp]
theorem
category_theory.limits.limit.post_π
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
(j : J) :
category_theory.limits.limit.post F G ≫ category_theory.limits.limit.π (F ⋙ G) j = G.map (category_theory.limits.limit.π F j)
@[simp]
theorem
category_theory.limits.limit.lift_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
(c : category_theory.limits.cone F) :
G.map (category_theory.limits.limit.lift F c) ≫ category_theory.limits.limit.post F G = category_theory.limits.limit.lift (F ⋙ G) (G.map_cone c)
@[simp]
theorem
category_theory.limits.limit.post_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
{E : Type u''}
[category_theory.category E]
(H : D ⥤ E)
[category_theory.limits.has_limit ((F ⋙ G) ⋙ H)] :
H.map (category_theory.limits.limit.post F G) ≫ category_theory.limits.limit.post (F ⋙ G) H = category_theory.limits.limit.post F (G ⋙ H)
theorem
category_theory.limits.limit.pre_post
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(E : K ⥤ J)
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (E ⋙ F)]
[category_theory.limits.has_limit (F ⋙ G)]
[category_theory.limits.has_limit ((E ⋙ F) ⋙ G)] :
G.map (category_theory.limits.limit.pre F E) ≫ category_theory.limits.limit.post (E ⋙ F) G = category_theory.limits.limit.post F G ≫ category_theory.limits.limit.pre (F ⋙ G) E
@[protected, instance]
def
category_theory.limits.has_limit_equivalence_comp
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_limit F] :
theorem
category_theory.limits.has_limit_of_equivalence_comp
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_limit (e.functor ⋙ F)] :
If a E ⋙ F has a limit, and E is an equivalence, we can construct a limit of F.
noncomputable
def
category_theory.limits.lim
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
limit F is functorial in F, when C has all limits of shape J.
Equations
- category_theory.limits.lim = {obj := λ (F : J ⥤ C), category_theory.limits.limit F, map := λ (F G : J ⥤ C) (α : F ⟶ G), category_theory.limits.lim_map α, map_id' := _, map_comp' := _}
Instances for category_theory.limits.lim
@[simp]
theorem
category_theory.limits.lim_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ C) :
@[simp]
theorem
category_theory.limits.lim_map_eq_lim_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G) :
theorem
category_theory.limits.limit.map_pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
[category_theory.limits.has_limits_of_shape K C]
(E : K ⥤ J) :
theorem
category_theory.limits.limit.map_pre'
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_limits_of_shape K C]
(F : J ⥤ C)
{E₁ E₂ : K ⥤ J}
(α : E₁ ⟶ E₂) :
theorem
category_theory.limits.limit.id_pre
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ C) :
theorem
category_theory.limits.limit.map_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limits_of_shape J D]
(H : C ⥤ D) :
noncomputable
def
category_theory.limits.lim_yoneda
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
The isomorphism between
morphisms from W to the cone point of the limit cone for F
and cones over F with cone point W
is natural in F.
Equations
- category_theory.limits.lim_yoneda = category_theory.nat_iso.of_components (λ (F : J ⥤ C), category_theory.nat_iso.of_components (λ (W : Cᵒᵖ), category_theory.limits.limit.hom_iso F (opposite.unop W)) _) category_theory.limits.lim_yoneda._proof_2
noncomputable
def
category_theory.limits.const_lim_adj
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
The constant functor and limit functor are adjoint to each other
Equations
- category_theory.limits.const_lim_adj = {hom_equiv := λ (c : C) (g : J ⥤ C), {to_fun := λ (f : (category_theory.functor.const J).obj c ⟶ g), category_theory.limits.limit.lift g {X := c, π := f}, inv_fun := λ (f : c ⟶ category_theory.limits.lim.obj g), {app := λ (j : J), f ≫ category_theory.limits.limit.π g j, naturality' := _}, left_inv := _, right_inv := _}, unit := {app := λ (c : C), category_theory.limits.limit.lift ((category_theory.functor.const J).obj ((λ (X : C), X) c)) {X := (λ (X : C), X) c, π := 𝟙 ((category_theory.functor.const J).obj ((λ (X : C), X) c))}, naturality' := _}, counit := {app := λ (g : J ⥤ C), {app := category_theory.limits.limit.π g _, naturality' := _}, naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
noncomputable
def
category_theory.limits.lim.category_theory.is_right_adjoint
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
Equations
@[protected, instance]
def
category_theory.limits.lim_map_mono'
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
(α : F ⟶ G)
[category_theory.mono α] :
@[protected, instance]
def
category_theory.limits.lim_map_mono
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G)
[∀ (j : J), category_theory.mono (α.app j)] :
theorem
category_theory.limits.has_limits_of_shape_of_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{J' : Type u₂}
[category_theory.category J']
(e : J ≌ J')
[category_theory.limits.has_limits_of_shape J C] :
We can transport limits of shape J along an equivalence J ≌ J'.
theorem
category_theory.limits.has_limits_of_size_shrink
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_limits_of_size C] :
has_limits_of_size_shrink.{v u} C tries to obtain has_limits_of_size.{v u} C
from some other has_limits_of_size C.
@[protected, instance]
@[nolint]
structure
category_theory.limits.colimit_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Type (max u u₁ v)
- cocone : category_theory.limits.cocone F
- is_colimit : category_theory.limits.is_colimit self.cocone
colimit_cocone F contains a cocone over F together with the information that it is a
colimit.
Instances for category_theory.limits.colimit_cocone
- category_theory.limits.colimit_cocone.has_sizeof_inst
@[class]
structure
category_theory.limits.has_colimit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C) :
Prop
- exists_colimit : nonempty (category_theory.limits.colimit_cocone F)
has_colimit F represents the mere existence of a colimit for F.
Instances of this typeclass
- category_theory.limits.has_colimit_of_has_colimits_of_shape
- category_theory.limits.has_coproduct_unique
- category_theory.limits.has_cokernels.has_colimit
- category_theory.limits.has_coproduct_of_has_biproduct
- category_theory.limits.has_colimit_equivalence_comp
- category_theory.limits.obj.has_colimit
- category_theory.limits.has_pushout_of_epi_comp
- category_theory.limits.has_pushout_of_right_factors_epi
- category_theory.limits.has_pushout_of_left_factors_epi
- category_theory.limits.has_cokernel_pair_of_epi
- category_theory.limits.has_coequalizer_of_self
- category_theory.limits.has_cokernel_comp_iso
- category_theory.limits.has_cokernel_epi_comp
- category_theory.limits.biproduct.ι.has_cokernel
- category_theory.limits.biproduct.from_subtype.has_cokernel
- category_theory.limits.has_binary_biproduct.has_colimit_pair
- category_theory.limits.biprod.inl.has_cokernel
- category_theory.limits.biprod.inr.has_cokernel
theorem
category_theory.limits.has_colimit.mk
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(d : category_theory.limits.colimit_cocone F) :
noncomputable
def
category_theory.limits.get_colimit_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
Use the axiom of choice to extract explicit colimit_cocone F from has_colimit F.
@[class]
structure
category_theory.limits.has_colimits_of_shape
(J : Type u₁)
[category_theory.category J]
(C : Type u)
[category_theory.category C] :
Prop
- has_colimit : (∀ (F : J ⥤ C), category_theory.limits.has_colimit F) . "apply_instance"
C has colimits of shape J if there exists a colimit for every functor F : J ⥤ C.
Instances of this typeclass
- category_theory.limits.has_zero_object.has_initial
- category_theory.limits.has_colimits_of_shape_of_has_colimits_of_size
- category_theory.limits.has_colimits_of_shape_of_has_finite_colimits
- category_theory.limits.has_binary_coproducts_of_has_binary_biproducts
- category_theory.limits.has_initial_op_of_has_terminal
- category_theory.limits.has_colimits_of_shape_wide_pushout_shape
- category_theory.limits.has_colimits_of_shape_discrete
@[class]
structure
category_theory.limits.has_colimits_of_size
(C : Type u)
[category_theory.category C] :
Prop
- has_colimits_of_shape : (∀ (J : Type ?) [𝒥 : category_theory.category J], category_theory.limits.has_colimits_of_shape J C) . "apply_instance"
C has all colimits of size v₁ u₁ (has_colimits_of_size.{v₁ u₁} C)
if it has colimits of every shape J : Type u₁ with [category.{v₁} J].
Instances of this typeclass
@[reducible]
C has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.
@[protected, instance]
def
category_theory.limits.has_colimit_of_has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
[H : category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ C) :
@[protected, instance]
noncomputable
def
category_theory.limits.colimit.cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
An arbitrary choice of colimit cocone of a functor.
noncomputable
def
category_theory.limits.colimit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
C
An arbitrary choice of colimit object of a functor.
Equations
noncomputable
def
category_theory.limits.colimit.ι
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(j : J) :
The coprojection from a value of the functor to the colimit object.
Equations
Instances for category_theory.limits.colimit.ι
- category_theory.limits.is_iso_ι_terminal
- category_theory.limits.is_iso_ι_initial
- category_theory.limits.pushout.inl_of_epi
- category_theory.limits.pushout.inr_of_epi
- category_theory.limits.pushout_inr_iso_of_left_iso
- category_theory.limits.pushout_inr_iso_of_right_factors_epi
- category_theory.limits.pushout_inl_iso_of_right_iso
- category_theory.limits.pushout_inl_iso_of_left_factors_epi
- category_theory.limits.inl_iso_of_epi_eq
- category_theory.limits.inr_iso_of_epi_eq
- category_theory.limits.coequalizer.π_epi
- category_theory.limits.coequalizer.π_of_self
- category_theory.limits.is_split_mono_sigma_ι
- category_theory.limits.is_split_mono_coprod_inl
- category_theory.limits.is_split_mono_coprod_inr
- category_theory.limits.cokernel.π_zero_is_iso
- category_theory.limits.cokernel.of_kernel_of_mono
@[simp]
theorem
category_theory.limits.colimit.cocone_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.cocone_X
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F] :
@[simp]
theorem
category_theory.limits.colimit.w
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{j j' : J}
(f : j ⟶ j') :
@[simp]
theorem
category_theory.limits.colimit.w_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{j j' : J}
(f : j ⟶ j')
{X' : C}
(f' : category_theory.limits.colimit F ⟶ X') :
F.map f ≫ category_theory.limits.colimit.ι F j' ≫ f' = category_theory.limits.colimit.ι F j ≫ f'
noncomputable
def
category_theory.limits.colimit.is_colimit
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
Evidence that the arbitrary choice of cocone is a colimit cocone.
noncomputable
def
category_theory.limits.colimit.desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
The morphism from the colimit object to the cone point of any other cocone.
Equations
Instances for category_theory.limits.colimit.desc
@[simp]
theorem
category_theory.limits.colimit.is_colimit_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.colimit.ι_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colimit.desc F c ≫ f' = c.ι.app j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.ι_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J) :
We have lots of lemmas describing how to simplify colimit.ι F j ≫ _,
and combined with colimit.ext we rely on these lemmas for many calculations.
However, since category.assoc is a @[simp] lemma, often expressions are
right associated, and it's hard to apply these lemmas about colimit.ι.
We thus use reassoc to define additional @[simp] lemmas, with an arbitrary extra morphism.
(see tactic/reassoc_axiom.lean)
noncomputable
def
category_theory.limits.colim_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G) :
Functoriality of colimits.
Usually this morphism should be accessed through colim.map,
but may be needed separately when you have specified colimits for the source and target functors,
but not necessarily for all functors of shape J.
Equations
Instances for category_theory.limits.colim_map
@[simp]
theorem
category_theory.limits.ι_colim_map_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colim_map α ≫ f' = α.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.ι_colim_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G)
(j : J) :
noncomputable
def
category_theory.limits.colimit.cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
The cocone morphism from the arbitrary choice of colimit cocone to any cocone.
@[simp]
theorem
category_theory.limits.colimit.cocone_morphism_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
theorem
category_theory.limits.colimit.ι_cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ ((category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso hc).hom ≫ f' = c.ι.app j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ (hc.cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit F)).inv ≫ f' = c.ι.app j ≫ f'
theorem
category_theory.limits.colimit.exists_unique
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.cocone F) :
noncomputable
def
category_theory.limits.colimit.iso_colimit_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.colimit_cocone F) :
Given any other colimit cocone for F, the chosen colimit F is isomorphic to the cocone point.
@[simp]
theorem
category_theory.limits.colimit.iso_colimit_cocone_ι_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.colimit_cocone F)
(j : J)
{X' : C}
(f' : t.cocone.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ (category_theory.limits.colimit.iso_colimit_cocone t).hom ≫ f' = t.cocone.ι.app j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.iso_colimit_cocone_ι_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.colimit_cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.iso_colimit_cocone_ι_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.colimit_cocone F)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit F ⟶ X') :
t.cocone.ι.app j ≫ (category_theory.limits.colimit.iso_colimit_cocone t).inv ≫ f' = category_theory.limits.colimit.ι F j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.iso_colimit_cocone_ι_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(t : category_theory.limits.colimit_cocone F)
(j : J) :
@[ext]
theorem
category_theory.limits.colimit.hom_ext
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{X : C}
{f f' : category_theory.limits.colimit F ⟶ X}
(w : ∀ (j : J), category_theory.limits.colimit.ι F j ≫ f = category_theory.limits.colimit.ι F j ≫ f') :
f = f'
@[simp]
theorem
category_theory.limits.colimit.desc_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F] :
noncomputable
def
category_theory.limits.colimit.hom_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(W : C) :
The isomorphism (in Type) between
morphisms from the colimit object to a specified object W,
and cocones with cone point W.
Equations
@[simp]
theorem
category_theory.limits.colimit.hom_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{W : C}
(f : ulift (category_theory.limits.colimit F ⟶ W)) :
noncomputable
def
category_theory.limits.colimit.hom_iso'
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(W : C) :
The isomorphism (in Type) between
morphisms from the colimit object to a specified object W,
and an explicit componentwise description of cocones with cone point W.
Equations
theorem
category_theory.limits.colimit.desc_extend
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
theorem
category_theory.limits.has_colimit_of_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
(α : G ≅ F) :
If F has a colimit, so does any naturally isomorphic functor.
theorem
category_theory.limits.has_colimit.of_cocones_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{K : Type u₁}
[category_theory.category K]
(F : J ⥤ C)
(G : K ⥤ C)
(h : F.cocones ≅ G.cocones)
[category_theory.limits.has_colimit F] :
If a functor G has the same collection of cocones as a functor F
which has a colimit, then G also has a colimit.
noncomputable
def
category_theory.limits.has_colimit.iso_of_nat_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G) :
The colimits of F : J ⥤ C and G : J ⥤ C are isomorphic,
if the functors are naturally isomorphic.
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ (category_theory.limits.has_colimit.iso_of_nat_iso w).hom ≫ f' = w.hom.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J) :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit F ⟶ X') :
category_theory.limits.colimit.ι G j ≫ (category_theory.limits.has_colimit.iso_of_nat_iso w).inv ≫ f' = w.inv.app j ≫ category_theory.limits.colimit.ι F j ≫ f'
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J) :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_hom_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(t : category_theory.limits.cocone G)
(w : F ≅ G) :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_hom_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(t : category_theory.limits.cocone G)
(w : F ≅ G)
{X' : C}
(f' : t.X ⟶ X') :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_inv_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(t : category_theory.limits.cocone F)
(w : F ≅ G) :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_inv_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(t : category_theory.limits.cocone F)
(w : F ≅ G)
{X' : C}
(f' : t.X ⟶ X') :
noncomputable
def
category_theory.limits.has_colimit.iso_of_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{G : K ⥤ C}
[category_theory.limits.has_colimit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
The colimits of F : J ⥤ C and G : K ⥤ C are isomorphic,
if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_equivalence_hom_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{G : K ⥤ C}
[category_theory.limits.has_colimit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(j : J) :
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_equivalence_inv_π
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{G : K ⥤ C}
[category_theory.limits.has_colimit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(k : K) :
category_theory.limits.colimit.ι G k ≫ (category_theory.limits.has_colimit.iso_of_equivalence e w).inv = G.map (e.counit_inv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ category_theory.limits.colimit.ι F (e.inverse.obj k)
noncomputable
def
category_theory.limits.colimit.pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)] :
The canonical morphism from the colimit of E ⋙ F to the colimit of F.
@[simp]
theorem
category_theory.limits.colimit.ι_pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(k : K) :
category_theory.limits.colimit.ι (E ⋙ F) k ≫ category_theory.limits.colimit.pre F E = category_theory.limits.colimit.ι F (E.obj k)
@[simp]
theorem
category_theory.limits.colimit.ι_pre_assoc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(k : K)
{X' : C}
(f' : category_theory.limits.colimit F ⟶ X') :
category_theory.limits.colimit.ι (E ⋙ F) k ≫ category_theory.limits.colimit.pre F E ≫ f' = category_theory.limits.colimit.ι F (E.obj k) ≫ f'
@[simp]
theorem
category_theory.limits.colimit.pre_desc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.colimit.pre_desc_assoc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(c : category_theory.limits.cocone F)
{X' : C}
(f' : c.X ⟶ X') :
@[simp]
theorem
category_theory.limits.colimit.pre_pre
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
{L : Type u₃}
[category_theory.category L]
(D : L ⥤ K)
[category_theory.limits.has_colimit (D ⋙ E ⋙ F)] :
theorem
category_theory.limits.colimit.pre_eq
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{E : K ⥤ J}
[category_theory.limits.has_colimit (E ⋙ F)]
(s : category_theory.limits.colimit_cocone (E ⋙ F))
(t : category_theory.limits.colimit_cocone F) :
- If we have particular colimit cocones available for
E ⋙ Fand forF, we obtain a formula forcolimit.pre F E.
noncomputable
def
category_theory.limits.colimit.post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)] :
The canonical morphism from G applied to the colimit of F ⋙ G
to G applied to the colimit of F.
Equations
@[simp]
theorem
category_theory.limits.colimit.ι_post_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J)
{X' : D}
(f' : G.obj (category_theory.limits.colimit F) ⟶ X') :
category_theory.limits.colimit.ι (F ⋙ G) j ≫ category_theory.limits.colimit.post F G ≫ f' = G.map (category_theory.limits.colimit.ι F j) ≫ f'
@[simp]
theorem
category_theory.limits.colimit.ι_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.post_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(c : category_theory.limits.cocone F) :
category_theory.limits.colimit.post F G ≫ G.map (category_theory.limits.colimit.desc F c) = category_theory.limits.colimit.desc (F ⋙ G) (G.map_cocone c)
@[simp]
theorem
category_theory.limits.colimit.post_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
{E : Type u''}
[category_theory.category E]
(H : D ⥤ E)
[category_theory.limits.has_colimit ((F ⋙ G) ⋙ H)] :
category_theory.limits.colimit.post (F ⋙ G) H ≫ H.map (category_theory.limits.colimit.post F G) = category_theory.limits.colimit.post F (G ⋙ H)
theorem
category_theory.limits.colimit.pre_post
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(E : K ⥤ J)
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (E ⋙ F)]
[category_theory.limits.has_colimit (F ⋙ G)]
[H : category_theory.limits.has_colimit ((E ⋙ F) ⋙ G)] :
category_theory.limits.colimit.post (E ⋙ F) G ≫ G.map (category_theory.limits.colimit.pre F E) = category_theory.limits.colimit.pre (F ⋙ G) E ≫ category_theory.limits.colimit.post F G
@[protected, instance]
def
category_theory.limits.has_colimit_equivalence_comp
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_colimit F] :
theorem
category_theory.limits.has_colimit_of_equivalence_comp
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_colimit (e.functor ⋙ F)] :
If a E ⋙ F has a colimit, and E is an equivalence, we can construct a colimit of F.
noncomputable
def
category_theory.limits.colim
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
colimit F is functorial in F, when C has all colimits of shape J.
Equations
- category_theory.limits.colim = {obj := λ (F : J ⥤ C), category_theory.limits.colimit F, map := λ (F G : J ⥤ C) (α : F ⟶ G), category_theory.limits.colim_map α, map_id' := _, map_comp' := _}
Instances for category_theory.limits.colim
@[simp]
theorem
category_theory.limits.colim_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ C) :
@[simp]
theorem
category_theory.limits.colimit.ι_map
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.ι_map_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colim.obj G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colim.map α ≫ f' = α.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.map_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(c : category_theory.limits.cocone G) :
theorem
category_theory.limits.colimit.pre_map
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
[category_theory.limits.has_colimits_of_shape K C]
(E : K ⥤ J) :
theorem
category_theory.limits.colimit.pre_map'
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
(F : J ⥤ C)
{E₁ E₂ : K ⥤ J}
(α : E₁ ⟶ E₂) :
theorem
category_theory.limits.colimit.pre_id
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ C) :
theorem
category_theory.limits.colimit.map_post
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimits_of_shape J D]
(H : C ⥤ D) :
noncomputable
def
category_theory.limits.colim_coyoneda
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
The isomorphism between
morphisms from the cone point of the colimit cocone for F to W
and cocones over F with cone point W
is natural in F.
Equations
- category_theory.limits.colim_coyoneda = category_theory.nat_iso.of_components (λ (F : (J ⥤ C)ᵒᵖ), category_theory.nat_iso.of_components (category_theory.limits.colimit.hom_iso (opposite.unop F)) _) category_theory.limits.colim_coyoneda._proof_3
noncomputable
def
category_theory.limits.colim_const_adj
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
The colimit functor and constant functor are adjoint to each other
Equations
- category_theory.limits.colim_const_adj = {hom_equiv := λ (f : J ⥤ C) (c : C), {to_fun := λ (g : category_theory.limits.colim.obj f ⟶ c), {app := λ (_x : J), category_theory.limits.colimit.ι f _x ≫ g, naturality' := _}, inv_fun := λ (g : f ⟶ (category_theory.functor.const J).obj c), category_theory.limits.colimit.desc f {X := c, ι := g}, left_inv := _, right_inv := _}, unit := {app := λ (g : J ⥤ C), {app := category_theory.limits.colimit.ι ((𝟭 (J ⥤ C)).obj g) _, naturality' := _}, naturality' := _}, counit := {app := λ (c : C), category_theory.limits.colimit.desc ((category_theory.functor.const J).obj c) {X := c, ι := 𝟙 ((category_theory.functor.const J).obj c)}, naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
noncomputable
def
category_theory.limits.colim.category_theory.is_left_adjoint
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
Equations
@[protected, instance]
def
category_theory.limits.colim_map_epi'
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
(α : F ⟶ G)
[category_theory.epi α] :
@[protected, instance]
def
category_theory.limits.colim_map_epi
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G)
[∀ (j : J), category_theory.epi (α.app j)] :
theorem
category_theory.limits.has_colimits_of_shape_of_equivalence
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{J' : Type u₂}
[category_theory.category J']
(e : J ≌ J')
[category_theory.limits.has_colimits_of_shape J C] :
We can transport colimits of shape J along an equivalence J ≌ J'.
theorem
category_theory.limits.has_colimits_of_size_shrink
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits_of_size C] :
has_colimits_of_size_shrink.{v u} C tries to obtain has_colimits_of_size.{v u} C
from some other has_colimits_of_size C.
@[protected, instance]
def
category_theory.limits.is_limit.op
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit t) :
If t : cone F is a limit cone, then t.op : cocone F.op is a colimit cocone.
def
category_theory.limits.is_colimit.op
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit t) :
If t : cocone F is a colimit cocone, then t.op : cone F.op is a limit cone.
def
category_theory.limits.is_limit.unop
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F.op}
(P : category_theory.limits.is_limit t) :
If t : cone F.op is a limit cone, then t.unop : cocone F is a colimit cocone.
def
category_theory.limits.is_colimit.unop
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F.op}
(P : category_theory.limits.is_colimit t) :
If t : cocone F.op is a colimit cocone, then t.unop : cone F. is a limit cone.
def
category_theory.limits.is_limit_equiv_is_colimit_op
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F} :
t : cone F is a limit cone if and only is t.op : cocone F.op is a colimit cocone.
def
category_theory.limits.is_colimit_equiv_is_limit_op
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F} :
t : cocone F is a colimit cocone if and only is t.op : cone F.op is a limit cone.