Documentation

Mathlib.CategoryTheory.FinCategory.AsType

Finite categories are equivalent to category in Type 0. #

source
@[inline, reducible]
abbrev CategoryTheory.FinCategory.ObjAsType (α : Type u_1) [Fintype α] :
Type

A FinCategory α is equivalent to a category with objects in Type.

Equations
Instances For
    source
    instance CategoryTheory.FinCategory.instFintypeHomObjAsTypeToQuiverToCategoryStructCategoryFinCardCoeEquivInstFunLikeEquivSymmEquivFin (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {i : CategoryTheory.FinCategory.ObjAsType α} {j : CategoryTheory.FinCategory.ObjAsType α} :
    Fintype (i ⟶ j)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable def CategoryTheory.FinCategory.objAsTypeEquiv (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] :
    CategoryTheory.FinCategory.ObjAsType α ≌ α

    The constructed category is indeed equivalent to α.

    Equations
    Instances For
      source
      @[inline, reducible]
      abbrev CategoryTheory.FinCategory.AsType (α : Type u_1) [Fintype α] :
      Type

      A FinCategory α is equivalent to a fin_category with in Type.

      Equations
      Instances For
        source
        theorem CategoryTheory.FinCategory.categoryAsType_id (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (i : CategoryTheory.FinCategory.AsType α) :
        CategoryTheory.CategoryStruct.id i = (Fintype.equivFin (i ⟶ i)) (CategoryTheory.CategoryStruct.id i)
        source
        theorem CategoryTheory.FinCategory.categoryAsType_comp (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
        ∀ {X Y Z : CategoryTheory.FinCategory.AsType α} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = (Fintype.equivFin (X ⟶ Z)) (CategoryTheory.CategoryStruct.comp ((Fintype.equivFin (X ⟶ Y)).symm f) ((Fintype.equivFin (Y ⟶ Z)).symm g))
        source
        noncomputable instance CategoryTheory.FinCategory.categoryAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
        CategoryTheory.SmallCategory (CategoryTheory.FinCategory.AsType α)
        Equations
        source
        @[simp]
        theorem CategoryTheory.FinCategory.asTypeToObjAsType_obj (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (a : CategoryTheory.FinCategory.AsType α) :
        (CategoryTheory.FinCategory.asTypeToObjAsType α).obj a = id a
        source
        @[simp]
        theorem CategoryTheory.FinCategory.asTypeToObjAsType_map (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {X : CategoryTheory.FinCategory.AsType α} {Y : CategoryTheory.FinCategory.AsType α} (a : Fin (Fintype.card (X ⟶ Y))) :
        (CategoryTheory.FinCategory.asTypeToObjAsType α).map a = (Fintype.equivFin (X ⟶ Y)).symm a
        source
        noncomputable def CategoryTheory.FinCategory.asTypeToObjAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
        CategoryTheory.Functor (CategoryTheory.FinCategory.AsType α) (CategoryTheory.FinCategory.ObjAsType α)

        The "identity" functor from AsType α to ObjAsType α.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.FinCategory.objAsTypeToAsType_map (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {X : CategoryTheory.FinCategory.ObjAsType α} {Y : CategoryTheory.FinCategory.ObjAsType α} (a : X ⟶ Y) :
          (CategoryTheory.FinCategory.objAsTypeToAsType α).map a = (Fintype.equivFin (X ⟶ Y)) a
          source
          @[simp]
          theorem CategoryTheory.FinCategory.objAsTypeToAsType_obj (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (a : CategoryTheory.FinCategory.ObjAsType α) :
          (CategoryTheory.FinCategory.objAsTypeToAsType α).obj a = id a
          source
          noncomputable def CategoryTheory.FinCategory.objAsTypeToAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
          CategoryTheory.Functor (CategoryTheory.FinCategory.ObjAsType α) (CategoryTheory.FinCategory.AsType α)

          The "identity" functor from ObjAsType α to AsType α.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def CategoryTheory.FinCategory.asTypeEquivObjAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
            CategoryTheory.FinCategory.AsType α ≌ CategoryTheory.FinCategory.ObjAsType α

            The constructed category (AsType α) is equivalent to ObjAsType α.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable instance CategoryTheory.FinCategory.asTypeFinCategory (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
              CategoryTheory.FinCategory (CategoryTheory.FinCategory.AsType α)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              noncomputable def CategoryTheory.FinCategory.equivAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] :
              CategoryTheory.FinCategory.AsType α ≌ α

              The constructed category (ObjAsType α) is indeed equivalent to α.

              Equations
              Instances For