Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

CategoryTheory.Limits.HasFiniteLimits structure

Full source

/-- 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'.
-/
class HasFiniteLimits : Prop where
  /-- `C` has all limits over any type `J` whose objects and morphisms lie in the same universe
  and which has `FinType` objects and morphisms -/
  out (J : Type) [𝒥 : SmallCategory J] [@FinCategory J 𝒥] : @HasLimitsOfShape J 𝒥 C _

Category with finite limits

Informal description

A category $ C $ has all finite limits if for every finite category $ J $ and every functor $ F : J \to C $, the limit of $ F $ exists in $ C $. Such categories are often called *finitely complete*.

CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instance

[HasFiniteLimits C] (J : Type w) [SmallCategory J] [FinCategory J] : HasLimitsOfShape J C

Full source

instance (priority := 100) hasLimitsOfShape_of_hasFiniteLimits [HasFiniteLimits C] (J : Type w)
    [SmallCategory J] [FinCategory J] : HasLimitsOfShape J C := by
  apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
  apply HasFiniteLimits.out

Finite Limits Imply Limits of Finite Shape

Informal description

For any category $\mathcal{C}$ with finite limits and any finite category $\mathcal{J}$, $\mathcal{C}$ has limits of shape $\mathcal{J}$.

CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize theorem

[HasLimitsOfSize.{v', u'} C] : HasFiniteLimits C

Full source

lemma hasFiniteLimits_of_hasLimitsOfSize [HasLimitsOfSize.{v', u'} C] :
    HasFiniteLimits C where
  out := fun J hJ hJ' =>
    haveI := hasLimitsOfSizeShrink.{0, 0} C
    let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
    @hasLimitsOfShape_of_equivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
    (@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _

Existence of Finite Limits from Limits of a Given Size

Informal description

If a category $\mathcal{C}$ has all limits of size $(v', u')$, then $\mathcal{C}$ has all finite limits.

CategoryTheory.Limits.hasFiniteLimits_of_hasLimits instance

[HasLimits C] : HasFiniteLimits C

Full source

/-- If `C` has all limits, it has finite limits. -/
instance (priority := 100) hasFiniteLimits_of_hasLimits [HasLimits C] : HasFiniteLimits C :=
  hasFiniteLimits_of_hasLimitsOfSize C

Categories with All Limits are Finitely Complete

Informal description

Every category $\mathcal{C}$ that has all (small) limits also has all finite limits.

CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize₀ instance

[HasLimitsOfSize.{0, 0} C] : HasFiniteLimits C

Full source

instance (priority := 90) hasFiniteLimits_of_hasLimitsOfSize₀ [HasLimitsOfSize.{0, 0} C] :
    HasFiniteLimits C :=
  hasFiniteLimits_of_hasLimitsOfSize C

Finite Completeness from Limits of Size (0, 0)

Informal description

For any category $\mathcal{C}$ that has all limits of size $(0, 0)$, $\mathcal{C}$ has all finite limits.

CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size theorem

(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasLimitsOfShape J C) : HasFiniteLimits C

Full source

/-- We can always derive `HasFiniteLimits C` by providing limits at an
arbitrary universe. -/
theorem hasFiniteLimits_of_hasFiniteLimits_of_size
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasLimitsOfShape J C) :
    HasFiniteLimits C where
  out := fun J hJ hhJ => by
    haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
    have l : @Equivalence J (ULiftHom (ULift J)) hJ
                          (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
    apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Finite Completeness via Limits of Finite Shapes

Informal description

A category $\mathcal{C}$ has all finite limits if for every finite category $\mathcal{J}$ (i.e., a category with finitely many objects and morphisms), $\mathcal{C}$ has limits of shape $\mathcal{J}$.

CategoryTheory.Limits.HasFiniteColimits structure

Full source

/-- 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'.
-/
class HasFiniteColimits : Prop where
  /-- `C` has all colimits over any type `J` whose objects and morphisms lie in the same universe
  and which has `Fintype` objects and morphisms -/
  out (J : Type) [𝒥 : SmallCategory J] [@FinCategory J 𝒥] : @HasColimitsOfShape J 𝒥 C _

Finitely cocomplete category

Informal description

A category $C$ has finite colimits if for every finite category $J$ (i.e., a category with finitely many objects and morphisms), the category $C$ has colimits for all functors $J \to C$. This property is often referred to as being "finitely cocomplete."

CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits instance

[HasFiniteColimits C] (J : Type w) [SmallCategory J] [FinCategory J] : HasColimitsOfShape J C

Full source

instance (priority := 100) hasColimitsOfShape_of_hasFiniteColimits [HasFiniteColimits C]
    (J : Type w) [SmallCategory J] [FinCategory J] : HasColimitsOfShape J C := by
  refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
  apply HasFiniteColimits.out

Finite Cocompleteness Implies Colimits of Finite Shapes

Informal description

For any category $C$ with finite colimits and any finite small category $J$, $C$ has colimits of shape $J$.

CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize theorem

[HasColimitsOfSize.{v', u'} C] : HasFiniteColimits C

Full source

lemma hasFiniteColimits_of_hasColimitsOfSize [HasColimitsOfSize.{v', u'} C] :
    HasFiniteColimits C where
  out := fun J hJ hJ' =>
    haveI := hasColimitsOfSizeShrink.{0, 0} C
    let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
    @hasColimitsOfShape_of_equivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
    (@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _

Existence of Finite Colimits from Colimits of Given Size

Informal description

If a category $\mathcal{C}$ has all colimits of size $(v', u')$, then $\mathcal{C}$ has finite colimits.

CategoryTheory.Limits.hasFiniteColimits_of_hasColimits instance

[HasColimits C] : HasFiniteColimits C

Full source

instance (priority := 100) hasFiniteColimits_of_hasColimits [HasColimits C] : HasFiniteColimits C :=
  hasFiniteColimits_of_hasColimitsOfSize C

Categories with All Colimits are Finitely Cocomplete

Informal description

Every category $\mathcal{C}$ that has all (small) colimits also has finite colimits.

CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instance

[HasColimitsOfSize.{0, 0} C] : HasFiniteColimits C

Full source

instance (priority := 90) hasFiniteColimits_of_hasColimitsOfSize₀ [HasColimitsOfSize.{0, 0} C] :
    HasFiniteColimits C :=
  hasFiniteColimits_of_hasColimitsOfSize C

Finite Colimits from Colimits of Size (0, 0)

Informal description

For any category $\mathcal{C}$ that has all colimits of size $(0, 0)$, $\mathcal{C}$ has finite colimits.

CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size theorem

(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasColimitsOfShape J C) : HasFiniteColimits C

Full source

/-- We can always derive `HasFiniteColimits C` by providing colimits at an
arbitrary universe. -/
theorem hasFiniteColimits_of_hasFiniteColimits_of_size
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasColimitsOfShape J C) :
    HasFiniteColimits C where
  out := fun J hJ hhJ => by
    haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
    have l : @Equivalence J (ULiftHom (ULift J)) hJ
                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
    apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Existence of Finite Colimits via Colimits of Finite Shapes

Informal description

A category $C$ has finite colimits if for every finite category $J$ (i.e., a category with finitely many objects and finitely many morphisms between any two objects), $C$ has colimits of shape $J$.

CategoryTheory.Limits.fintypeWalkingParallelPair instance

: Fintype WalkingParallelPair

Full source

instance fintypeWalkingParallelPair : Fintype WalkingParallelPair where
  elems := [WalkingParallelPair.zero, WalkingParallelPair.one].toFinset
  complete x := by cases x <;> simp

Finiteness of the Walking Parallel Pair Category

Informal description

The indexing category `WalkingParallelPair` for (co)equalizer diagrams is finite.

CategoryTheory.Limits.instFintypeWalkingParallelPairHom instance

(j j' : WalkingParallelPair) : Fintype (WalkingParallelPairHom j j')

Full source

instance instFintypeWalkingParallelPairHom (j j' : WalkingParallelPair) :
    Fintype (WalkingParallelPairHom j j') where
  elems :=
    WalkingParallelPair.recOn j
      (WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset
        [left, right].toFinset)
      (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)
  complete := by
    rintro (_|_) <;> simp
    cases j <;> simp

Finiteness of Morphisms in the Walking Parallel Pair Category

Informal description

For any two objects $j$ and $j'$ in the walking parallel pair category, the type of morphisms $\mathrm{WalkingParallelPairHom}(j, j')$ is finite.

CategoryTheory.Limits.instFinCategoryWalkingParallelPair instance

: FinCategory WalkingParallelPair

Full source

instance : FinCategory WalkingParallelPair where
  fintypeObj := fintypeWalkingParallelPair
  fintypeHom := instFintypeWalkingParallelPairHom

Finiteness of the Walking Parallel Pair Category

Informal description

The walking parallel pair category is a finite category, meaning it has finitely many objects and finitely many morphisms between any pair of objects.

CategoryTheory.Limits.WidePullbackShape.fintypeObj instance

[Fintype J] : Fintype (WidePullbackShape J)

Full source

instance fintypeObj [Fintype J] : Fintype (WidePullbackShape J) :=
  inferInstanceAs <| Fintype (Option _)

Finiteness of Objects in Wide Pullback Shapes

Informal description

For any finite type $J$, the category `WidePullbackShape J` has finitely many objects.

CategoryTheory.Limits.WidePullbackShape.fintypeHom instance

(j j' : WidePullbackShape J) : Fintype (j ⟶ j')

Full source

instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j') where
  elems := by
    obtain - | j' := j'
    · obtain - | j := j
      · exact {Hom.id none}
      · exact {Hom.term j}
    · by_cases h : some j' = j
      · rw [h]
        exact {Hom.id j}
      · exact ∅
  complete := by
    rintro (_|_)
    · cases j <;> simp
    · simp

Finiteness of Morphisms in Wide Pullback Shapes

Informal description

For any objects $j$ and $j'$ in the wide pullback shape category, the hom-set $\mathrm{Hom}(j, j')$ is finite.

CategoryTheory.Limits.WidePushoutShape.fintypeObj instance

[Fintype J] : Fintype (WidePushoutShape J)

Full source

instance fintypeObj [Fintype J] : Fintype (WidePushoutShape J) := by
  rw [WidePushoutShape]; infer_instance

Finiteness of Objects in Wide Pushout Shapes

Informal description

For any finite type $J$, the category `WidePushoutShape J` has finitely many objects.

CategoryTheory.Limits.WidePushoutShape.fintypeHom instance

(j j' : WidePushoutShape J) : Fintype (j ⟶ j')

Full source

instance fintypeHom (j j' : WidePushoutShape J) : Fintype (j ⟶ j') where
  elems := by
    obtain - | j := j
    · obtain - | j' := j'
      · exact {Hom.id none}
      · exact {Hom.init j'}
    · by_cases h : some j = j'
      · rw [h]
        exact {Hom.id j'}
      · exact ∅
  complete := by
    rintro (_|_)
    · cases j <;> simp
    · simp

Finiteness of Morphisms in Wide Pushout Shapes

Informal description

For any objects $j$ and $j'$ in the wide pushout shape category `WidePushoutShape J`, the hom-set $\mathrm{Hom}(j, j')$ is finite.

CategoryTheory.Limits.finCategoryWidePullback instance

[Fintype J] : FinCategory (WidePullbackShape J)

Full source

instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J) where
  fintypeHom := WidePullbackShape.fintypeHom

Finiteness of the Wide Pullback Shape Category

Informal description

For any finite type $J$, the wide pullback shape category $\mathrm{WidePullbackShape}\, J$ is a finite category, meaning it has finitely many objects and finite hom-sets between any two objects.

CategoryTheory.Limits.finCategoryWidePushout instance

[Fintype J] : FinCategory (WidePushoutShape J)

Full source

instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J) where
  fintypeHom := WidePushoutShape.fintypeHom

-- We can't just made this an `abbreviation`
-- because of https://github.com/leanprover-community/lean/issues/429

Finiteness of the Wide Pushout Shape Category

Informal description

For any finite type $J$, the category $\mathrm{WidePushoutShape}\, J$ is a finite category. This means it has finitely many objects and, for every pair of objects $j$ and $j'$, the set of morphisms $\mathrm{Hom}(j, j')$ is finite.

CategoryTheory.Limits.HasFiniteWidePullbacks structure

Full source

/-- `HasFiniteWidePullbacks` represents a choice of wide pullback
for every finite collection of morphisms
-/
class HasFiniteWidePullbacks : Prop where
  /-- `C` has all wide pullbacks for any Finite `J` -/
  out (J : Type) [Finite J] : HasLimitsOfShape (WidePullbackShape J) C

Category with finite wide pullbacks

Informal description

A category $ C $ has finite wide pullbacks if for every finite collection of morphisms in $ C $, there exists a wide pullback. This means that for any finite index set $ J $ and any family of morphisms $ f_j : X_j \to Y $ (for $ j \in J $), there exists an object $ P $ and morphisms $ \pi_j : P \to X_j $ forming a limit cone over the diagram formed by the $ f_j $.

CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape instance

(J : Type) [Finite J] [HasFiniteWidePullbacks C] : HasLimitsOfShape (WidePullbackShape J) C

Full source

instance hasLimitsOfShape_widePullbackShape (J : Type) [Finite J] [HasFiniteWidePullbacks C] :
    HasLimitsOfShape (WidePullbackShape J) C := by
  haveI := @HasFiniteWidePullbacks.out C _ _ J
  infer_instance

Existence of Limits for Finite Wide Pullback Shapes

Informal description

For any finite type $J$ and any category $\mathcal{C}$ with finite wide pullbacks, $\mathcal{C}$ has limits of shape $\mathrm{WidePullbackShape}\, J$.

CategoryTheory.Limits.HasFiniteWidePushouts structure

Full source

/-- `HasFiniteWidePushouts` represents a choice of wide pushout
for every finite collection of morphisms
-/
class HasFiniteWidePushouts : Prop where
  /-- `C` has all wide pushouts for any Finite `J` -/
  out (J : Type) [Finite J] : HasColimitsOfShape (WidePushoutShape J) C

Category with finite wide pushouts

Informal description

A category $ C $ has finite wide pushouts if for every finite collection of morphisms in $ C $, there exists a wide pushout. This means that for any finite index set $ J $ and any family of morphisms $ f_j : Y \to X_j $ (for $ j \in J $), there exists an object $ P $ and morphisms $ \iota_j : X_j \to P $ forming a colimit cocone over the diagram formed by the $ f_j $.

CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape instance

(J : Type) [Finite J] [HasFiniteWidePushouts C] : HasColimitsOfShape (WidePushoutShape J) C

Full source

instance hasColimitsOfShape_widePushoutShape (J : Type) [Finite J] [HasFiniteWidePushouts C] :
    HasColimitsOfShape (WidePushoutShape J) C := by
  haveI := @HasFiniteWidePushouts.out C _ _ J
  infer_instance

Existence of Colimits for Finite Wide Pushout Shapes

Informal description

For any finite type $J$ and any category $C$ with finite wide pushouts, $C$ has colimits of shape $\mathrm{WidePushoutShape}\, J$.

CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits instance

[HasFiniteLimits C] : HasFiniteWidePullbacks C

Full source

/-- Finite wide pullbacks are finite limits, so if `C` has all finite limits,
it also has finite wide pullbacks
-/
instance (priority := 900) hasFiniteWidePullbacks_of_hasFiniteLimits [HasFiniteLimits C] :
    HasFiniteWidePullbacks C :=
  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteLimits.out _⟩

Finite Wide Pullbacks from Finite Limits

Informal description

Every category $C$ with all finite limits also has all finite wide pullbacks.

CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits instance

[HasFiniteColimits C] : HasFiniteWidePushouts C

Full source

/-- Finite wide pushouts are finite colimits, so if `C` has all finite colimits,
it also has finite wide pushouts
-/
instance (priority := 900) hasFiniteWidePushouts_of_has_finite_limits [HasFiniteColimits C] :
    HasFiniteWidePushouts C :=
  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteColimits.out _⟩

Finite Colimits Imply Finite Wide Pushouts

Informal description

Every finitely cocomplete category has finite wide pushouts.

CategoryTheory.Limits.fintypeWalkingPair instance

: Fintype WalkingPair

Full source

instance fintypeWalkingPair : Fintype WalkingPair where
  elems := {WalkingPair.left, WalkingPair.right}
  complete x := by cases x <;> simp

Finite Indexing Category for Binary (Co)products

Informal description

The indexing category `WalkingPair` for binary (co)products is finite.