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]
def
category_theory.over.has_colimit_of_has_colimit_comp_forget
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
[i : category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.over.creates_colimits
{C : Type u}
[category_theory.category C]
{X : C} :
theorem
category_theory.over.epi_left_of_epi
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_pushouts C]
{f g : category_theory.over X}
(h : f ⟶ g)
[category_theory.epi h] :
theorem
category_theory.over.epi_iff_epi_left
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_pushouts C]
{f g : category_theory.over X}
(h : f ⟶ g) :
@[simp]
theorem
category_theory.over.pullback_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : X ⟶ Y)
(g : category_theory.over Y) :
@[simp]
theorem
category_theory.over.pullback_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : X ⟶ Y)
(g h : category_theory.over Y)
(k : g ⟶ h) :
noncomputable
def
category_theory.over.pullback
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{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
- category_theory.over.pullback f = {obj := λ (g : category_theory.over Y), category_theory.over.mk category_theory.limits.pullback.snd, map := λ (g h : category_theory.over Y) (k : g ⟶ h), category_theory.over.hom_mk (category_theory.limits.pullback.lift (category_theory.limits.pullback.fst ≫ k.left) category_theory.limits.pullback.snd _) _, map_id' := _, map_comp' := _}
Instances for category_theory.over.pullback
noncomputable
def
category_theory.over.map_pullback_adj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
(f : A ⟶ B) :
over.map f is left adjoint to over.pullback f.
Equations
- category_theory.over.map_pullback_adj f = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (g : category_theory.over A) (h : category_theory.over B), {to_fun := λ (X : (category_theory.over.map f).obj g ⟶ h), category_theory.over.hom_mk (category_theory.limits.pullback.lift X.left g.hom _) _, inv_fun := λ (Y : g ⟶ (category_theory.over.pullback f).obj h), category_theory.over.hom_mk (Y.left ≫ category_theory.limits.pullback.fst) _, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
noncomputable
def
category_theory.over.pullback_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A : C} :
pullback (𝟙 A) : over A ⥤ over A is the identity functor.
noncomputable
def
category_theory.over.pullback_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
pullback commutes with composition (up to natural isomorphism).
@[protected, instance]
noncomputable
def
category_theory.over.pullback_is_right_adjoint
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{A B : C}
(f : A ⟶ B) :
Equations
@[protected, instance]
def
category_theory.under.has_limit_of_has_limit_comp_forget
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
[i : category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] :
@[protected, instance]
@[protected, instance]
theorem
category_theory.under.mono_right_of_mono
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_pullbacks C]
{f g : category_theory.under X}
(h : f ⟶ g)
[category_theory.mono h] :
theorem
category_theory.under.mono_iff_mono_right
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_pullbacks C]
{f g : category_theory.under X}
(h : f ⟶ g) :
@[protected, instance]
noncomputable
def
category_theory.under.creates_limits
{C : Type u}
[category_theory.category C]
{X : C} :
noncomputable
def
category_theory.under.pushout
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pushouts C]
{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
- category_theory.under.pushout f = {obj := λ (g : category_theory.under X), category_theory.under.mk category_theory.limits.pushout.inr, map := λ (g h : category_theory.under X) (k : g ⟶ h), category_theory.under.hom_mk (category_theory.limits.pushout.desc (k.right ≫ category_theory.limits.pushout.inl) category_theory.limits.pushout.inr _) _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.under.pushout_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pushouts C]
{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}
[category_theory.category C]
[category_theory.limits.has_pushouts C]
{X Y : C}
(f : X ⟶ Y)
(g : category_theory.under X) :