mathlib3documentation

category_theory.limits.over

Limits and colimits in the over and under categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Show that the forgetful functor forget X : over X ⥤ C creates colimits, and hence over X has any colimits that C has (as well as the dual that forget X : under X ⟶ C creates limits).

Note that the folder category_theory.limits.shapes.constructions.over further shows that forget X : over X ⥤ C creates connected limits (so over X has connected limits), and that over X has J-indexed products if C has J-indexed wide pullbacks.

TODO: If C has binary products, then forget X : over X ⥤ C has a right adjoint.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.over.creates_colimits {C : Type u} {X : C} :
Equations
theorem category_theory.over.epi_left_of_epi {C : Type u} {X : C} {f g : category_theory.over X} (h : f g)  :
theorem category_theory.over.epi_iff_epi_left {C : Type u} {X : C} {f g : category_theory.over X} (h : f g) :
@[simp]
theorem category_theory.over.pullback_obj {C : Type u} {X Y : C} (f : X Y) (g : category_theory.over Y) :
@[simp]
theorem category_theory.over.pullback_map {C : Type u} {X Y : C} (f : X Y) (g h : category_theory.over Y) (k : g h) :
noncomputable def category_theory.over.pullback {C : Type u} {X Y : C} (f : X Y) :

When C has pullbacks, a morphism f : X ⟶ Y induces a functor over Y ⥤ over X, by pulling back a morphism along f.

Equations
Instances for category_theory.over.pullback
noncomputable def category_theory.over.map_pullback_adj {C : Type u} {A B : C} (f : A B) :

over.map f is left adjoint to over.pullback f.

Equations
noncomputable def category_theory.over.pullback_id {C : Type u} {A : C} :

pullback (𝟙 A) : over A ⥤ over A is the identity functor.

Equations
noncomputable def category_theory.over.pullback_comp {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) :

pullback commutes with composition (up to natural isomorphism).

Equations
@[protected, instance]
noncomputable def category_theory.over.pullback_is_right_adjoint {C : Type u} {A B : C} (f : A B) :
Equations
@[protected, instance]
def category_theory.under.has_limit_of_has_limit_comp_forget {J : Type v} {C : Type u} {X : C} (F : J )  :
@[protected, instance]
@[protected, instance]
theorem category_theory.under.mono_right_of_mono {C : Type u} {X : C} {f g : category_theory.under X} (h : f g)  :
theorem category_theory.under.mono_iff_mono_right {C : Type u} {X : C} {f g : category_theory.under X} (h : f g) :
@[protected, instance]
noncomputable def category_theory.under.creates_limits {C : Type u} {X : C} :
Equations
noncomputable def category_theory.under.pushout {C : Type u} {X Y : C} (f : X Y) :

When C has pushouts, a morphism f : X ⟶ Y induces a functor under X ⥤ under Y, by pushing a morphism forward along f.

Equations
@[simp]
theorem category_theory.under.pushout_map {C : Type u} {X Y : C} (f : X Y) (g h : category_theory.under X) (k : g h) :
@[simp]
theorem category_theory.under.pushout_obj {C : Type u} {X Y : C} (f : X Y) (g : category_theory.under X) :