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} [SmallCategory J] (K : Functor J FintypeCat) (j : J) :
Finite ((K.comp FintypeCat.incl).obj j)
source
@[implicit_reducible]
noncomputable instance CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] :
Fintype (limit K)

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

Equations
source
@[implicit_reducible]
noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits {J : Type} [SmallCategory J] [FinCategory J] :
CreatesLimitsOfShape J FintypeCat.incl
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetFunObjFiniteOfFinCategory {J : Type} [SmallCategory J] [FinCategory J] :
CreatesLimitsOfShape J (forget FintypeCat)

Help typeclass inference to infer creation of finite limits for the forgetful functor.

Equations
source
instance CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory {J : Type} [SmallCategory J] [FinCategory J] :
HasLimitsOfShape J FintypeCat
source
instance CategoryTheory.Limits.FintypeCat.hasFiniteLimits :
HasFiniteLimits FintypeCat
source
instance CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits :
PreservesFiniteLimits FintypeCat.incl
source
instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetFunObjFinite :
PreservesFiniteLimits (forget FintypeCat)

Help typeclass inference to infer preservation of finite limits for the forgetful functor.

source
noncomputable def CategoryTheory.Limits.FintypeCat.productEquiv {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) :
(∏ᶜ X).obj ≃ ((i : ι) → (X i).obj)

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).obj) (i : ι) :
    (productEquiv X) x i = (ConcreteCategory.hom (Pi.π X i)) x
    source
    @[simp]
    theorem CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply {ι : Type u_1} [Finite ι] (X : ι → FintypeCat) (x : (i : ι) → (X i).obj) (i : ι) :
    (ConcreteCategory.hom (Pi.π X i)) ((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).obj] :
    Nonempty (∏ᶜ X).obj
    source
    instance CategoryTheory.Limits.FintypeCat.finite_colimitType {J : Type u_1} [SmallCategory J] [FinCategory J] (K : Functor J (Type u)) [∀ (j : J), Finite (K.obj j)] :
    Finite K.ColimitType

    The colimit type of a functor from a finite category to Types that only involves finite objects is finite.

    source
    theorem CategoryTheory.Limits.FintypeCat.finite_of_isColimit {J : Type u_1} [SmallCategory J] [FinCategory J] {K : Functor J (Type u)} [∀ (j : J), Finite (K.obj j)] {c : Cocone K} (hc : IsColimit c) :
    Finite c.pt

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

    source
    @[implicit_reducible]
    noncomputable instance CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] :
    Fintype (colimit K)

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

    Equations
    source
    @[implicit_reducible]
    noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits {J : Type} [SmallCategory J] [FinCategory J] :
    CreatesColimitsOfShape J FintypeCat.incl
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetFunObjFiniteOfFinCategory {J : Type} [SmallCategory J] [FinCategory J] :
    CreatesColimitsOfShape J (forget FintypeCat)

    Help typeclass inference to infer creation of finite colimits for the forgetful functor.

    Equations
    source
    instance CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory {J : Type} [SmallCategory J] [FinCategory J] :
    HasColimitsOfShape J FintypeCat
    source
    instance CategoryTheory.Limits.FintypeCat.hasFiniteColimits :
    HasFiniteColimits FintypeCat
    source
    instance CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits :
    PreservesFiniteColimits FintypeCat.incl
    source
    instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetFunObjFinite :
    PreservesFiniteColimits (forget FintypeCat)

    Help typeclass inference to infer preservation of finite colimits for the forgetful functor.

    source
    theorem CategoryTheory.Limits.FintypeCat.jointly_surjective {J : Type u_1} [SmallCategory J] [FinCategory J] (F : Functor J FintypeCat) (t : Cocone F) (h : IsColimit t) (x : t.pt.obj) :
    ∃ (j : J) (y : (fun (X : ObjectProperty.FullSubcategory Finite) => X.obj) (F.obj j)), (ConcreteCategory.hom (t.ι.app j)) y = x