structure CategoryTheory.IsSLimit {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : Type (max (max u_1 u_2) (u_4 + 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)

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_1} {C : Type u_2} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (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_1} {C : Type u_2} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : C) (h : CategoryTheory.IsSLimit c) : 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_1} {C : Type u_2} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : C) (h : CategoryTheory.IsSLimit c) : CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.limitComparison c X)

noncomputable def CategoryTheory.SimplicialCategory.limitComparisonIso {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (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_1} {C : Type u_2} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.SimplicialCategory C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) [∀ (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

• isLimit : CategoryTheory.IsSLimit self.cone

  The proof that is the limit cone

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₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [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 ⋯

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₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [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

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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] [self : CategoryTheory.HasConicalLimitsOfSize.{u, v, u₁, v₁} C] (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.HasConicalLimitsOfShape J C

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

@[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

• ⋯ = ⋯

@[reducible, inline]

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

An abbreviation for HasConicalLimit (Discrete.functor f).

Equations

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