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] : Prop

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

• Action.instHasFiniteLimits
• AlgebraicGeometry.instHasFiniteLimitsScheme
• CategoryTheory.Abelian.hasFiniteLimits
• CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop
• CategoryTheory.Limits.FintypeCat.hasFiniteLimits
• CategoryTheory.Limits.functor_category_hasFiniteLimits
• CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimits
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize₀
• CategoryTheory.Limits.hasFiniteLimits_opposite
• CategoryTheory.Limits.instHasFiniteLimitsFunctor
• CategoryTheory.Over.hasFiniteLimits
• CategoryTheory.PreGaloisCategory.instHasFiniteLimits
• CategoryTheory.Sheaf.instHasFiniteLimits
• CategoryTheory.ShortComplex.hasFiniteLimits
• FDRep.instHasFiniteLimits
• FGModuleCat.instHasFiniteLimits
• HomologicalComplex.instHasFiniteLimits
• PresheafOfModules.hasFiniteLimits
• SheafOfModules.Finite.hasFiniteLimits
• instHasFiniteLimitsLightCondMod
• instHasFiniteLimitsLightCondSet

theorem CategoryTheory.Limits.HasFiniteLimits.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteLimits C] (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [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

@[instance 100]

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

• ⋯ = ⋯

theorem 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

@[instance 100]

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

• ⋯ = ⋯

@[instance 90]

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

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] : Prop

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

• Action.instHasFiniteColimits
• CategoryTheory.Abelian.hasFiniteColimits
• CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot
• CategoryTheory.Limits.FintypeCat.hasFiniteColimits
• CategoryTheory.Limits.functor_category_hasFiniteColimits
• CategoryTheory.Limits.hasFiniteColimits_of_hasColimits
• CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀
• CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits
• CategoryTheory.Limits.hasFiniteColimits_opposite
• CategoryTheory.Limits.instHasFiniteColimitsFunctor
• CategoryTheory.Sheaf.instHasFiniteColimits
• CategoryTheory.ShortComplex.hasFiniteColimits
• HomologicalComplex.instHasFiniteColimits
• ModuleCat.instHasFiniteColimits
• PresheafOfModules.Finite.hasFiniteColimits

theorem CategoryTheory.Limits.HasFiniteColimits.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteColimits C] (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [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

@[instance 100]

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

• ⋯ = ⋯

theorem 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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 90]

instance CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{0, 0, v, u} 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.instFinCategoryWalkingParallelPair : 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 = ⋯.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] : Prop

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

theorem CategoryTheory.Limits.HasFiniteWidePullbacks.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteWidePullbacks C] (J : Type) [Finite J] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C

C has all wide pullbacks any Fintype J

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] : Prop

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

theorem CategoryTheory.Limits.HasFiniteWidePushouts.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteWidePushouts C] (J : Type) [Finite J] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C

C has all wide pushouts any Fintype J

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.