structure CategoryTheory.IsSLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : Type (max (max u u₁) (v + 1))

A limit cone c in a simplicial category A is a simplicially enriched limit if for every X : C, the cone obtained by applying the simplicial coyoneda functor (X ⟶[A] -) to c is a limit cone in SSet.

• isLimit : CategoryTheory.Limits.IsLimit c
• isSLimit : (X : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)).mapCone c)

def CategoryTheory.IsSLimit_islimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (slim : CategoryTheory.IsSLimit c) : CategoryTheory.Limits.IsLimit c

Conical simplicial limits are also limits in the unenriched sense.

Equations

• CategoryTheory.IsSLimit_islimit c slim = slim.isLimit

Characterization in terms of the comparison map.

There is a canonical comparison map with the limit in SSet, the following proves that a limit cone in A is a simplicially enriched limit if and only if the comparison map is an isomorphism for every X : A.

noncomputable def CategoryTheory.SimplicialCategory.limitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) : CategoryTheory.SimplicialCategory.sHom X c.pt ⟶ CategoryTheory.Limits.limit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.SimplicialCategory.limitComparison_eq_conePointUniqueUpToIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) [CategoryTheory.Limits.HasLimit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))] : CategoryTheory.SimplicialCategory.limitComparison c X = ((h.isSLimit X).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X))))).hom

theorem CategoryTheory.SimplicialCategory.isIso_limitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) : CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.limitComparison c X)

noncomputable def CategoryTheory.SimplicialCategory.limitComparisonIso {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] (X : C) (h : CategoryTheory.IsSLimit c) : CategoryTheory.SimplicialCategory.sHom X c.pt ≅ CategoryTheory.Limits.limit (F.comp ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj (Opposite.op X)))

Equations

• CategoryTheory.SimplicialCategory.limitComparisonIso c X h = CategoryTheory.asIso (CategoryTheory.SimplicialCategory.limitComparison c X)

noncomputable def CategoryTheory.SimplicialCategory.isSLimitOfIsIsoLimitComparison {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [CategoryTheory.Limits.HasLimitsOfShape J SSet] [∀ (X : C), CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.limitComparison c X)] (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsSLimit c

Equations

• One or more equations did not get rendered due to their size.

structure CategoryTheory.ConicalLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) : Type (max (max u u₁) (v + 1))

ConicalLimitCone F contains a cone over F together with the information that it is a conical limit.

• cone : CategoryTheory.Limits.Cone F

  The cone itself

• isSLimit : CategoryTheory.IsSLimit self.cone

  The proof that is the limit cone

def CategoryTheory.ConicalLimitCone_isLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (cone : CategoryTheory.Limits.Cone F) (slim : CategoryTheory.IsSLimit cone) : CategoryTheory.Limits.IsLimit cone

A conical limit cone is a limit cone.

Equations

• CategoryTheory.ConicalLimitCone_isLimitCone cone slim = slim.isLimit

class CategoryTheory.HasConicalLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) : Prop

HasConicalLimit F represents the mere existence of a limit for F.

• mk' :: (
• exists_limit : Nonempty (CategoryTheory.ConicalLimitCone F)

  There is some limit cone for F

• )

theorem CategoryTheory.HasConicalLimit.exists_limit {J : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.SimplicialCategory C} {F : CategoryTheory.Functor J C} [self : CategoryTheory.HasConicalLimit F], Nonempty (CategoryTheory.ConicalLimitCone F)

There is some limit cone for F

theorem CategoryTheory.HasConicalLimit.mk {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (d : CategoryTheory.ConicalLimitCone F) : CategoryTheory.HasConicalLimit F

noncomputable def CategoryTheory.getConicalLimitCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.ConicalLimitCone F

Use the axiom of choice to extract explicit ConicalLimitCone F from HasConicalLimit F.

Equations

• CategoryTheory.getConicalLimitCone F = Classical.choice ⋯

theorem CategoryTheory.HasConicalLimit_hasLimit {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] (F : CategoryTheory.Functor J C) [CategoryTheory.HasConicalLimit F] : CategoryTheory.Limits.HasLimit F

class CategoryTheory.HasConicalLimitsOfShape (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has conical limits of shape J if there exists a conical limit for every functor F : J ⥤ C.

• has_conical_limit : ∀ (F : CategoryTheory.Functor J C), CategoryTheory.HasConicalLimit F

  All functors F : J ⥤ C from J have limits

theorem CategoryTheory.HasConicalLimitsOfShape.has_conical_limit {J : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.SimplicialCategory C} [self : CategoryTheory.HasConicalLimitsOfShape J C] (F : CategoryTheory.Functor J C), CategoryTheory.HasConicalLimit F

All functors F : J ⥤ C from J have limits

instance CategoryTheory.HasConicalLimitsOfShape_hasLimitsOfShape (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J C

Equations

• ⋯ = ⋯

class CategoryTheory.HasConicalLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has all conical limits of size v₁ u₁ (HasLimitsOfSize.{v₁ u₁} C) if it has conical limits of every shape J : Type u₁ with [Category.{v₁} J].

• has_conical_limits_of_shape : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.HasConicalLimitsOfShape J C

  All functors F : J ⥤ C from all small J have conical limits

theorem CategoryTheory.HasConicalLimitsOfSize.has_conical_limits_of_shape {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.SimplicialCategory C} [self : CategoryTheory.HasConicalLimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.HasConicalLimitsOfShape J C

All functors F : J ⥤ C from all small J have conical limits

instance CategoryTheory.HasConicalLimitsOfSize_hasLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfSize.{u_1, u_2, v, u} C] : CategoryTheory.Limits.HasLimitsOfSize.{u_3, u_4, v, u} C

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.HasConicalLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

C has all (small) conical limits if it has limits of every shape that is as big as its hom-sets.

Equations

• CategoryTheory.HasConicalLimits C = CategoryTheory.HasConicalLimitsOfSize.{?u.23, ?u.23, ?u.23, ?u.22} C

instance CategoryTheory.HasConicalLimits_hasLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimits C] : CategoryTheory.Limits.HasLimits C

Equations

• ⋯ = ⋯

instance CategoryTheory.HasConicalLimits.has_conical_limits_of_shape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimits C] (J : Type v) [CategoryTheory.Category.{v, v} J] : CategoryTheory.HasConicalLimitsOfShape J C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.hasConicalLimitOfHasConicalLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.HasConicalLimit F

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.hasConicalLimitsOfShapeOfHasLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalLimitsOfSize.{v₁, u₁, v, u} C] : CategoryTheory.HasConicalLimitsOfShape J C

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.HasConicalProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {I : Type u₁} (f : I → C) : Prop

An abbreviation for HasSLimit (Discrete.functor f).

Equations

• CategoryTheory.HasConicalProduct f = CategoryTheory.HasConicalLimit (CategoryTheory.Discrete.functor f)

theorem CategoryTheory.HasConicalProduct_hasProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] {I : Type u₁} (f : I → C) [CategoryTheory.HasConicalProduct f] : CategoryTheory.Limits.HasProduct f

class CategoryTheory.HasConicalProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : Prop

• has_limits_of_shape : ∀ {I : Type v} (f : I → C), CategoryTheory.HasConicalProduct f

  All discrete diagrams of bounded size have conical products.

theorem CategoryTheory.HasConicalProducts.has_limits_of_shape {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.SimplicialCategory C} [self : CategoryTheory.HasConicalProducts C] {I : Type v} (f : I → C), CategoryTheory.HasConicalProduct f

All discrete diagrams of bounded size have conical products.

instance CategoryTheory.HasConicalProducts_hasProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [CategoryTheory.HasConicalProducts C] : CategoryTheory.Limits.HasProducts C

Equations

• ⋯ = ⋯