mathlib documentation

category_theory.limits.over

@[simp]

theorem category_theory.functor.to_cocone_ι_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) (j : J) :

F.to_cocone.ι.app j = (F.obj j).hom

@[simp]

theorem category_theory.functor.to_cocone_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) :

F.to_cocone.X = X

def category_theory.functor.to_cocone {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) :

category_theory.limits.cocone (F ⋙ category_theory.over.forget X)

Equations

F.to_cocone = {X := X, ι := {app := λ (j : J), (F.obj j).hom, naturality' := _}}

def category_theory.functor.to_cone {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) :

category_theory.limits.cone (F ⋙ category_theory.under.forget X)

Equations

F.to_cone = {X := X, π := {app := λ (j : J), (F.obj j).hom, naturality' := _}}

@[simp]

theorem category_theory.functor.to_cone_π_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) (j : J) :

F.to_cone.π.app j = (F.obj j).hom

@[simp]

theorem category_theory.functor.to_cone_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) :

F.to_cone.X = X

@[simp]

theorem category_theory.over.colimit_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) [category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] :

(category_theory.over.colimit F).X = category_theory.over.mk (category_theory.limits.colimit.desc (F ⋙ category_theory.over.forget X) F.to_cocone)

@[simp]

theorem category_theory.over.colimit_ι_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) [category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] (j : J) :

(category_theory.over.colimit F).ι.app j = category_theory.over.hom_mk (category_theory.limits.colimit.ι (F ⋙ category_theory.over.forget X) j) _

def category_theory.over.colimit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.over X) [category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] :

category_theory.limits.cocone F

Equations

category_theory.over.colimit F = {X := category_theory.over.mk (category_theory.limits.colimit.desc (F ⋙ category_theory.over.forget X) F.to_cocone), ι := {app := λ (j : J), category_theory.over.hom_mk (category_theory.limits.colimit.ι (F ⋙ category_theory.over.forget X) j) _, naturality' := _}}

@[instance]

def category_theory.over.category_theory.limits.reflects_colimits {C : Type u} [category_theory.category C] {X : C} :

category_theory.limits.reflects_colimits (category_theory.over.forget X)

Equations

category_theory.over.category_theory.limits.reflects_colimits = {reflects_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_colimit := λ (F : J ⥤ category_theory.over X), {reflects := λ (t : category_theory.limits.cocone F) (ht : category_theory.limits.is_colimit ((category_theory.over.forget X).map_cocone t)), {desc := λ (s : category_theory.limits.cocone F), category_theory.over.hom_mk (ht.desc ((category_theory.over.forget X).map_cocone s)) _, fac' := _, uniq' := _}}}}

@[instance]

def category_theory.over.has_colimit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} {F : J ⥤ category_theory.over X} [category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] :

category_theory.limits.has_colimit F

@[instance]

def category_theory.over.has_colimits_of_shape {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} [category_theory.limits.has_colimits_of_shape J C] :

category_theory.limits.has_colimits_of_shape J (category_theory.over X)

@[instance]

def category_theory.over.has_colimits {C : Type u} [category_theory.category C] {X : C} [category_theory.limits.has_colimits C] :

category_theory.limits.has_colimits (category_theory.over X)

@[instance]

def category_theory.over.forget_preserves_colimit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} {F : J ⥤ category_theory.over X} [category_theory.limits.has_colimit (F ⋙ category_theory.over.forget X)] :

category_theory.limits.preserves_colimit F (category_theory.over.forget X)

Equations

category_theory.over.forget_preserves_colimit = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.reflects_colimit.reflects (category_theory.over.forget_colimit_is_colimit F)) (category_theory.over.forget_colimit_is_colimit F)

@[instance]

def category_theory.over.forget_preserves_colimits_of_shape {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits_of_shape J C] {X : C} :

category_theory.limits.preserves_colimits_of_shape J (category_theory.over.forget X)

Equations

category_theory.over.forget_preserves_colimits_of_shape = {preserves_colimit := λ (F : J ⥤ category_theory.over X), category_theory.over.forget_preserves_colimit}

@[instance]

def category_theory.over.forget_preserves_colimits {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X : C} :

category_theory.limits.preserves_colimits (category_theory.over.forget X)

Equations

category_theory.over.forget_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), category_theory.over.forget_preserves_colimits_of_shape}

def category_theory.under.limit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) [category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] :

category_theory.limits.cone F

Equations

category_theory.under.limit F = {X := category_theory.under.mk (category_theory.limits.limit.lift (F ⋙ category_theory.under.forget X) F.to_cone), π := {app := λ (j : J), category_theory.under.hom_mk (category_theory.limits.limit.π (F ⋙ category_theory.under.forget X) j) _, naturality' := _}}

@[simp]

theorem category_theory.under.limit_X {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) [category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] :

(category_theory.under.limit F).X = category_theory.under.mk (category_theory.limits.limit.lift (F ⋙ category_theory.under.forget X) F.to_cone)

@[simp]

theorem category_theory.under.limit_π_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) [category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] (j : J) :

(category_theory.under.limit F).π.app j = category_theory.under.hom_mk (category_theory.limits.limit.π (F ⋙ category_theory.under.forget X) j) _

def category_theory.under.forget_limit_is_limit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J ⥤ category_theory.under X) [category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] :

category_theory.limits.is_limit ((category_theory.under.forget X).map_cone (category_theory.under.limit F))

Equations

category_theory.under.forget_limit_is_limit F = (category_theory.limits.limit.is_limit (F ⋙ category_theory.under.forget X)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl (category_theory.limits.limit.cone (F ⋙ category_theory.under.forget X)).X) _)

@[instance]

def category_theory.under.category_theory.limits.reflects_limits {C : Type u} [category_theory.category C] {X : C} :

category_theory.limits.reflects_limits (category_theory.under.forget X)

Equations

category_theory.under.category_theory.limits.reflects_limits = {reflects_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_limit := λ (F : J ⥤ category_theory.under X), {reflects := λ (t : category_theory.limits.cone F) (ht : category_theory.limits.is_limit ((category_theory.under.forget X).map_cone t)), {lift := λ (s : category_theory.limits.cone F), category_theory.under.hom_mk (ht.lift ((category_theory.under.forget X).map_cone s)) _, fac' := _, uniq' := _}}}}

@[instance]

def category_theory.under.has_limit {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} {F : J ⥤ category_theory.under X} [category_theory.limits.has_limit (F ⋙ category_theory.under.forget X)] :

category_theory.limits.has_limit F

@[instance]

def category_theory.under.has_limits_of_shape {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} [category_theory.limits.has_limits_of_shape J C] :

category_theory.limits.has_limits_of_shape J (category_theory.under X)

@[instance]

def category_theory.under.has_limits {C : Type u} [category_theory.category C] {X : C} [category_theory.limits.has_limits C] :

category_theory.limits.has_limits (category_theory.under X)

@[instance]

def category_theory.under.forget_preserves_limits {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] {X : C} :

category_theory.limits.preserves_limits (category_theory.under.forget X)

Equations

category_theory.under.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ category_theory.under X), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.reflects_limit.reflects (category_theory.under.forget_limit_is_limit F)) (category_theory.under.forget_limit_is_limit F)}}