Connected limits in the over category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Shows that the forgetful functor over B ⥤ C creates connected limits, in particular over B has
any connected limit which C has.
def
category_theory.over.creates_connected.nat_trans_in_over
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{B : C}
(F : J ⥤ category_theory.over B) :
(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.
Equations
- category_theory.over.creates_connected.nat_trans_in_over F = {app := λ (j : J), (F.obj j).hom, naturality' := _}
noncomputable
def
category_theory.over.creates_connected.raise_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C}
{F : J ⥤ category_theory.over B}
(c : category_theory.limits.cone (F ⋙ category_theory.over.forget B)) :
(Impl) Given a cone in the base category, raise it to a cone in the over category. Note this is where the connected assumption is used.
Equations
- category_theory.over.creates_connected.raise_cone c = {X := category_theory.over.mk (c.π.app (classical.arbitrary J) ≫ (F.obj (classical.arbitrary J)).hom), π := {app := λ (j : J), category_theory.over.hom_mk (c.π.app j) _, naturality' := _}}
@[simp]
theorem
category_theory.over.creates_connected.raise_cone_π_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C}
{F : J ⥤ category_theory.over B}
(c : category_theory.limits.cone (F ⋙ category_theory.over.forget B))
(j : J) :
@[simp]
theorem
category_theory.over.creates_connected.raise_cone_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C}
{F : J ⥤ category_theory.over B}
(c : category_theory.limits.cone (F ⋙ category_theory.over.forget B)) :
theorem
category_theory.over.creates_connected.raised_cone_lowers_to_original
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C}
{F : J ⥤ category_theory.over B}
(c : category_theory.limits.cone (F ⋙ category_theory.over.forget B))
(t : category_theory.limits.is_limit c) :
noncomputable
def
category_theory.over.creates_connected.raised_cone_is_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C}
{F : J ⥤ category_theory.over B}
{c : category_theory.limits.cone (F ⋙ category_theory.over.forget B)}
(t : category_theory.limits.is_limit c) :
(Impl) Show that the raised cone is a limit.
Equations
- category_theory.over.creates_connected.raised_cone_is_limit t = {lift := λ (s : category_theory.limits.cone F), category_theory.over.hom_mk (t.lift ((category_theory.over.forget B).map_cone s)) _, fac' := _, uniq' := _}
@[protected, instance]
noncomputable
def
category_theory.over.forget_creates_connected_limits
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.is_connected J]
{B : C} :
The forgetful functor from the over category creates any connected limit.
Equations
- category_theory.over.forget_creates_connected_limits = {creates_limit := λ (K : J ⥤ category_theory.over B), category_theory.creates_limit_of_reflects_iso (λ (c : category_theory.limits.cone (K ⋙ category_theory.over.forget B)) (t : category_theory.limits.is_limit c), {to_liftable_cone := {lifted_cone := category_theory.over.creates_connected.raise_cone c, valid_lift := category_theory.eq_to_iso _}, makes_limit := category_theory.over.creates_connected.raised_cone_is_limit t})}
@[protected, instance]
def
category_theory.over.has_connected_limits
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{B : C}
[category_theory.is_connected J]
[category_theory.limits.has_limits_of_shape J C] :
The over category has any connected limit which the original category has.