Documentation

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Categories with finite limits. #

A typeclass for categories with all finite (co)limits.

class CategoryTheory.Limits.HasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] :

A category has all finite limits if every functor J ⥤ C with a FinCategory J instance and J : Type has a limit.

This is often called 'finitely complete'.

out : ∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [inst : CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J C
C has all limits over any type J whose objects and morphisms lie in the same universe and which has FinType objects and morphisms

Instances

instance CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasFiniteLimits C] :

CategoryTheory.Limits.HasLimitsOfShape J C

Equations

⋯ = ⋯

instance CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v', u', v, u} C] :

CategoryTheory.Limits.HasFiniteLimits C

Equations

⋯ = ⋯

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

CategoryTheory.Limits.HasFiniteLimits C

If C has all limits, it has finite limits.

Equations

⋯ = ⋯

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size (C : Type u) [CategoryTheory.Category.{v, u} C] (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.HasLimitsOfShape J C) :

CategoryTheory.Limits.HasFiniteLimits C

We can always derive HasFiniteLimits C by providing limits at an arbitrary universe.

class CategoryTheory.Limits.HasFiniteColimits (C : Type u) [CategoryTheory.Category.{v, u} C] :

A category has all finite colimits if every functor J ⥤ C with a FinCategory J instance and J : Type has a colimit.

This is often called 'finitely cocomplete'.

out : ∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [inst : CategoryTheory.FinCategory J], CategoryTheory.Limits.HasColimitsOfShape J C
C has all colimits over any type J whose objects and morphisms lie in the same universe and which has Fintype objects and morphisms

Instances

instance CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasFiniteColimits C] :

CategoryTheory.Limits.HasColimitsOfShape J C

Equations

⋯ = ⋯

instance CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{v', u', v, u} C] :

CategoryTheory.Limits.HasFiniteColimits C

Equations

⋯ = ⋯

instance CategoryTheory.Limits.hasFiniteColimits_of_hasColimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] :

CategoryTheory.Limits.HasFiniteColimits C

Equations

⋯ = ⋯

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size (C : Type u) [CategoryTheory.Category.{v, u} C] (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.HasColimitsOfShape J C) :

CategoryTheory.Limits.HasFiniteColimits C

We can always derive HasFiniteColimits C by providing colimits at an arbitrary universe.

instance CategoryTheory.Limits.fintypeWalkingParallelPair :

Fintype CategoryTheory.Limits.WalkingParallelPair

Equations

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

instance CategoryTheory.Limits.instFintypeWalkingParallelPairHom (j : CategoryTheory.Limits.WalkingParallelPair) (j' : CategoryTheory.Limits.WalkingParallelPair) :

Fintype (CategoryTheory.Limits.WalkingParallelPairHom j j')

Equations

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

instance CategoryTheory.Limits.instFinCategoryWalkingParallelPairWalkingParallelPairHomCategory :

CategoryTheory.FinCategory CategoryTheory.Limits.WalkingParallelPair

Equations

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

instance CategoryTheory.Limits.WidePullbackShape.fintypeObj {J : Type v} [Fintype J] :

Fintype (CategoryTheory.Limits.WidePullbackShape J)

Equations

CategoryTheory.Limits.WidePullbackShape.fintypeObj = inferInstanceAs (Fintype (Option J))

instance CategoryTheory.Limits.WidePullbackShape.fintypeHom {J : Type v} (j : CategoryTheory.Limits.WidePullbackShape J) (j' : CategoryTheory.Limits.WidePullbackShape J) :

Fintype (j ⟶ j')

Equations

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

instance CategoryTheory.Limits.WidePushoutShape.fintypeObj {J : Type v} [Fintype J] :

Fintype (CategoryTheory.Limits.WidePushoutShape J)

Equations

CategoryTheory.Limits.WidePushoutShape.fintypeObj = Eq.mpr ⋯ inferInstance

instance CategoryTheory.Limits.WidePushoutShape.fintypeHom {J : Type v} (j : CategoryTheory.Limits.WidePushoutShape J) (j' : CategoryTheory.Limits.WidePushoutShape J) :

Fintype (j ⟶ j')

Equations

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

instance CategoryTheory.Limits.finCategoryWidePullback {J : Type v} [Fintype J] :

CategoryTheory.FinCategory (CategoryTheory.Limits.WidePullbackShape J)

Equations

CategoryTheory.Limits.finCategoryWidePullback = { fintypeObj := inferInstance, fintypeHom := CategoryTheory.Limits.WidePullbackShape.fintypeHom }

instance CategoryTheory.Limits.finCategoryWidePushout {J : Type v} [Fintype J] :

CategoryTheory.FinCategory (CategoryTheory.Limits.WidePushoutShape J)

Equations

CategoryTheory.Limits.finCategoryWidePushout = { fintypeObj := inferInstance, fintypeHom := CategoryTheory.Limits.WidePushoutShape.fintypeHom }

class CategoryTheory.Limits.HasFiniteWidePullbacks (C : Type u) [CategoryTheory.Category.{v, u} C] :

HasFiniteWidePullbacks represents a choice of wide pullback for every finite collection of morphisms

out : ∀ (J : Type) [inst : Finite J], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
C has all wide pullbacks any Fintype J

Instances

instance CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type) [Finite J] [CategoryTheory.Limits.HasFiniteWidePullbacks C] :

CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C

Equations

⋯ = ⋯

class CategoryTheory.Limits.HasFiniteWidePushouts (C : Type u) [CategoryTheory.Category.{v, u} C] :

HasFiniteWidePushouts represents a choice of wide pushout for every finite collection of morphisms

out : ∀ (J : Type) [inst : Finite J], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
C has all wide pushouts any Fintype J

Instances

instance CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type) [Finite J] [CategoryTheory.Limits.HasFiniteWidePushouts C] :

CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C

Equations

⋯ = ⋯

theorem CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] :

CategoryTheory.Limits.HasFiniteWidePullbacks C

Finite wide pullbacks are finite limits, so if C has all finite limits, it also has finite wide pullbacks

theorem CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] :

CategoryTheory.Limits.HasFiniteWidePushouts C

Finite wide pushouts are finite colimits, so if C has all finite colimits, it also has finite wide pushouts

instance CategoryTheory.Limits.fintypeWalkingPair :

Fintype CategoryTheory.Limits.WalkingPair

Equations

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