Documentation

Mathlib.CategoryTheory.Limits.FintypeCat

(Co)limits in the category of finite types #

We show that finite (co)limits exist in FintypeCat and that they are preserved by the natural inclusion FintypeCat.incl.

source
instance CategoryTheory.Limits.FintypeCat.instFiniteObjCompFintypeCatIncl {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J FintypeCat) (j : J) :
Finite ((K.comp FintypeCat.incl).obj j)
Equations
  • ⋯ = ⋯
source
noncomputable instance CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] :
Fintype (CategoryTheory.Limits.limit K)

Any functor from a finite category to Types that only involves finite objects, has a finite limit.

Equations
source
noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
CategoryTheory.CreatesLimitsOfShape J FintypeCat.incl
Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetOfFinCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget FintypeCat)
Equations
  • CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetOfFinCategory = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits
source
instance CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
CategoryTheory.Limits.HasLimitsOfShape J FintypeCat
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Limits.FintypeCat.hasFiniteLimits :
CategoryTheory.Limits.HasFiniteLimits FintypeCat
Equations
source
noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteLimits :
CategoryTheory.Limits.PreservesFiniteLimits FintypeCat.incl
Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForget :
CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget FintypeCat)
Equations
source
noncomputable def CategoryTheory.Limits.FintypeCat.productEquiv {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) :
↑(∏ᶜ X) ≃ ((i : ι) → ↑(X i))

The categorical product of a finite family in FintypeCat is equivalent to the product as types.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.FintypeCat.productEquiv_apply {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) (x : ↑(∏ᶜ X)) (i : ι) :
    (CategoryTheory.Limits.FintypeCat.productEquiv X) x i = CategoryTheory.Limits.Pi.π X i x
    source
    @[simp]
    theorem CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) (x : (i : ι) → ↑(X i)) (i : ι) :
    CategoryTheory.Limits.Pi.π X i ((CategoryTheory.Limits.FintypeCat.productEquiv X).symm x) = x i
    source
    instance CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) [∀ (i : ι), Nonempty ↑(X i)] :
    Nonempty ↑(∏ᶜ X)
    Equations
    • ⋯ = ⋯
    source
    noncomputable instance CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] :
    Fintype (CategoryTheory.Limits.colimit K)

    Any functor from a finite category to Types that only involves finite objects, has a finite colimit.

    Equations
    source
    noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
    CategoryTheory.CreatesColimitsOfShape J FintypeCat.incl
    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetOfFinCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
    CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget FintypeCat)
    Equations
    • CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetOfFinCategory = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits
    source
    instance CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
    CategoryTheory.Limits.HasColimitsOfShape J FintypeCat
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Limits.FintypeCat.hasFiniteColimits :
    CategoryTheory.Limits.HasFiniteColimits FintypeCat
    Equations
    source
    noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteColimits :
    CategoryTheory.Limits.PreservesFiniteColimits FintypeCat.incl
    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForget :
    CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget FintypeCat)
    Equations
    source
    theorem CategoryTheory.Limits.FintypeCat.jointly_surjective {J : Type u_1} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J FintypeCat) (t : CategoryTheory.Limits.Cocone F) (h : CategoryTheory.Limits.IsColimit t) (x : ↑t.pt) :
    ∃ (j : J) (y : ↑(F.obj j)), t.ι.app j y = x