Geb.Mathlib.CategoryTheory.FinCat.Category

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Mathlib.CategoryTheory.FinCat.Basic
public import Mathlib.CategoryTheory.Category.Basic
public import Mathlib.Data.ULift

The generated mathlib category

A FinCat specification generates a mathlib Category: objects are lifted indices into Fin S.objCount, and morphisms are lifted values of S.Mor. Objects and morphisms sit at independent universe levels.

Main definitions

CategoryTheory.FinCat.Obj — the object type of the generated category.

CategoryTheory.FinCat.Obj.category — the Category instance.

CategoryTheory.FinCat.Obj.decidableEqHom — decidable equality of the generated morphisms.

Implementation notes

FinCat.Obj is a one-field structure rather than ULift (Fin _) directly, because a structure projection reduces by iota, which is available at reducible transparency, and because a Category instance on ULift (Fin _) would be a global instance on a type this file does not define.

The Category instance is written out rather than obtained by stacking CategoryTheory.ULiftHom on CategoryTheory.uliftCategory. mathlib's ULiftHom.category yields Category.{max v₂ v₁}; it reaches independent levels only because the underlying category sits at Category.{0} on Type 0, and going through it requires attribute [local instance] uliftCategory and two layers of ULift unwrapping in every proof.

Tags

category, finite category, decidable, constructive, choice-free, universe polymorphism

              @[expose] public sectionnamespace CategoryTheorynamespace FinCat

An object of the category generated by S: an object index, lifted. A one-field structure rather than ULift (Fin _) directly, because a structure projection reduces by iota, which is available at reducible transparency, and because a Category instance on ULift (Fin _) would be a global instance on a type this file does not define.

The index of the object.

@[ext] structure Obj.{u} (S : FinCat) : Type u where

  idx : ULift.{u} (Fin S.objCount)
  deriving DecidableEq

The category generated by S, with objects at level u and morphisms at level v, independently.

instance Obj.category.{v, u} (S : FinCat) : Category.{v} (Obj.{u} S) where
  Hom X Y := ULift.{v} (S.Mor X.idx.down Y.idx.down)
  id X := ULift.up (S.id X.idx.down)
  comp f g := ULift.up (S.compTotal f.down g.down)
  id_comp f := congrArg ULift.up (S.id_comp f.down)
  comp_id f := congrArg ULift.up (S.comp_id f.down)
  assoc f g h := congrArg ULift.up (S.compTotal_assoc f.down g.down h.down)

Decidable equality of the generated morphisms. Instance search does not unfold Quiver.Hom, so this does not follow from the category instance; inferInstanceAs names the unfolded type, and the decision itself is mathlib's ULift instance over Fin's.

instance Obj.decidableEqHom.{v, u} {S : FinCat} (X Y : Obj.{u} S) :
    DecidableEq (X ⟶ Y) :=
  inferInstanceAs (DecidableEq (ULift.{v} (S.Mor X.idx.down Y.idx.down)))

end FinCatend CategoryTheory