doc-next-gen

Mathlib.CategoryTheory.FinCategory.AsType

Module docstring

{"# Finite categories are equivalent to category in Type 0. "}

CategoryTheory.FinCategory.ObjAsType abbrev
: Type
Full source 
/-- A FinCategory `α` is equivalent to a category with objects in `Type`. -/
--@[nolint unused_arguments]
abbrev ObjAsType : Type :=
  InducedCategory α (Fintype.equivFin α).symm
Type Representation of Objects in a Finite Category
Informal description
For a finite category $\alpha$, the type `ObjAsType α` represents a type equivalent to the objects of $\alpha$ in `Type`. This provides a way to view the objects of a finite category as elements of a type in `Type`.
CategoryTheory.FinCategory.instFintypeHomObjAsType instance
{i j : ObjAsType α} : Fintype (i ⟶ j)
Full source 
instance {i j : ObjAsType α} : Fintype (i ⟶ j) :=
  FinCategory.fintypeHom ((Fintype.equivFin α).symm i) _
Finite Morphism Sets in Finite Categories
Informal description
For any finite category $\alpha$ and objects $i, j$ in the type representation of $\alpha$, the set of morphisms $\text{Hom}(i, j)$ is finite.
CategoryTheory.FinCategory.objAsTypeEquiv definition
: ObjAsType α ≌ α
Full source 
/-- The constructed category is indeed equivalent to `α`. -/
noncomputable def objAsTypeEquiv : ObjAsTypeObjAsType α ≌ α :=
  (inducedFunctor (Fintype.equivFin α).symm).asEquivalence
Equivalence between type representation and original finite category
Informal description
For a finite category $\alpha$, the equivalence `objAsTypeEquiv` establishes an equivalence of categories between the type `ObjAsType α` (which represents the objects of $\alpha$ as elements of `Type`) and the original finite category $\alpha$. This equivalence is constructed using: 1. The inverse of the equivalence between $\alpha$ and its finite enumeration (via `Fintype.equivFin`) 2. The induced functor from this equivalence 3. The packaging of this functor as a full equivalence (via `asEquivalence`) The construction ensures that working with objects as elements of `Type` is equivalent to working with the original finite category structure.
CategoryTheory.FinCategory.AsType abbrev
: Type
Full source 
/-- A FinCategory `α` is equivalent to a fin_category with in `Type`. -/
--@[nolint unused_arguments]
abbrev AsType : Type :=
  Fin (Fintype.card α)
Type interpretation of a finite category
Informal description
For a finitely presented category `α`, the type `AsType α` represents a corresponding category where objects are interpreted as elements of `Type`. This construction provides a way to work with finite categories within the type universe `Type`.
CategoryTheory.FinCategory.categoryAsType instance
: SmallCategory (AsType α)
Full source 
@[simps -isSimp id comp]
noncomputable instance categoryAsType : SmallCategory (AsType α) where
  Hom i j := Fin (Fintype.card (@Quiver.Hom (ObjAsType α) _ i j))
  id _ := Fintype.equivFin _ (𝟙 _)
  comp f g := Fintype.equivFin _ ((Fintype.equivFin _).symm f ≫ (Fintype.equivFin _).symm g)
Category Structure on Type Representation of Finite Categories
Informal description
For any finite category $\alpha$, the type `AsType α` carries a canonical small category structure.
CategoryTheory.FinCategory.asTypeToObjAsType definition
: AsType α ⥤ ObjAsType α
Full source 
/-- The "identity" functor from `AsType α` to `ObjAsType α`. -/
@[simps]
noncomputable def asTypeToObjAsType : AsTypeAsType α ⥤ ObjAsType α where
  obj := id
  map {_ _} := (Fintype.equivFin _).symm
Identity functor from type interpretation to object type representation
Informal description
The functor from `AsType α` to `ObjAsType α` is defined as the identity on objects and uses the inverse of the equivalence between finite morphism sets and finite types on morphisms. Specifically, for any objects $X, Y$ in `AsType α`, the morphism map is given by the inverse of the bijection between $\text{Hom}(X, Y)$ and its corresponding finite type representation.
CategoryTheory.FinCategory.objAsTypeToAsType definition
: ObjAsType α ⥤ AsType α
Full source 
/-- The "identity" functor from `ObjAsType α` to `AsType α`. -/
@[simps]
noncomputable def objAsTypeToAsType : ObjAsTypeObjAsType α ⥤ AsType α where
  obj := id
  map {_ _} := Fintype.equivFin _
Identity functor from object type to category type
Informal description
The functor from `ObjAsType α` to `AsType α` that acts as the identity on objects and uses the equivalence between finite morphism sets to define the action on morphisms.
CategoryTheory.FinCategory.asTypeEquivObjAsType definition
: AsType α ≌ ObjAsType α
Full source 
/-- The constructed category (`AsType α`) is equivalent to `ObjAsType α`. -/
noncomputable def asTypeEquivObjAsType : AsTypeAsType α ≌ ObjAsType α where
  functor := asTypeToObjAsType α
  inverse := objAsTypeToAsType α
  unitIso := NatIso.ofComponents Iso.refl
  counitIso := NatIso.ofComponents Iso.refl
Equivalence between `AsType α` and `ObjAsType α` categories
Informal description
The constructed category `AsType α` is equivalent to `ObjAsType α` via the functors `asTypeToObjAsType α` and `objAsTypeToAsType α`, with both the unit and counit natural isomorphisms being identity isomorphisms.
CategoryTheory.FinCategory.equivAsType definition
: AsType α ≌ α
Full source 
/-- The constructed category (`ObjAsType α`) is indeed equivalent to `α`. -/
noncomputable def equivAsType : AsTypeAsType α ≌ α :=
  (asTypeEquivObjAsType α).trans (objAsTypeEquiv α)
Equivalence between type representation and finite category
Informal description
The equivalence of categories between the type representation `AsType α` and the original finite category `α` is constructed by composing the equivalence `asTypeEquivObjAsType α` (between `AsType α` and `ObjAsType α`) with the equivalence `objAsTypeEquiv α` (between `ObjAsType α` and `α`). This establishes that the type-based representation of the finite category is equivalent to the original finite category structure.