Limits in FintypeCat

Stream: Is there code for X?

[Christian Merten]

Are there any results on (co)limits in FintypeCat? For example that it has all finite (co)limits and that forget FintypeCat preserves all finite (co)limits?

[Christian Merten]

Or that FintypeCat is a full subcategory of Type?

[Kevin Buzzard]

docs#FintypeCat

[Kevin Buzzard]

docs#FintypeCat.incl is full and faithful, these are both instances (you can just find them by clicking on the link in my last message and then scrolling down).

My guess is that page basically contains all facts about FintypeCat known to mathlib, so existence of and reflection of limits and colimits looks like it's not there

[Christian Merten]

Thanks, I was searching for docs#CategoryTheory.FullSubcategory in relation to FintypeCat because I found docs#CategoryTheory.Limits.hasLimit_of_closed_under_limits which I wanted to use to show that FintypeCat has all finite (co)limits. But I suppose I can use docs#CategoryTheory.createsLimitOfFullyFaithfulOfIso and the instances that you have linked?

[Kevin Buzzard]

Yeah these would be great additions to mathlib

[Christian Merten]

I need it for galois categories, so I'll have to write this at some point.

[Adam Topaz]

It seems we don’t have anything about (co)limits in FintypeCat

[Kevin Buzzard]

So maybe the plan is to prove that finite (Co)limits exist in Type and then show that they're finite (the limit injects into the product and the colimit admits a surjection from the coproduct) and then let general nonsense take over?

[Adam Topaz]

Yeah I think one should show that the forgetful functor creates all finite limits and colimits

[Christian Merten]

Yes, that was my idea and it is already shown that Type has all (finite) (co)limits.

[Adam Topaz]

Take a look at the api for (co)limits in concrete categories. There’s a bunch of stuff there that might help

[Christian Merten]

#8137, will fix the linting issues tomorrow.

[Christian Merten]

I was wondering what the best way to transport over results from docs#CategoryTheory.Limits.Shapes.Types is. Specifically I need some API around binary products, i.e. analogs of docs#CategoryTheory.Limits.Types.binaryProductIso etc.

One can certainly transport all data back and forth with FintypeCat.incl or one can just copy the code in docs#CategoryTheory.Limits.Shapes.Types more or less verbatim and replace all occurences of Type u with FintypeCat.{u}. Same question applies for all finite constructions in said file.

[Joël Riou]

I hope it is possible to do this using concrete categories. A few days ago, I did a PR about the products and pullbacks in concrete categories #8507. In particular https://github.com/leanprover-community/mathlib4/pull/8507/files#diff-5ed8283d8adc6009eb1d2aa1228b162f5d281a8d9d34c91a9f3004a625e7e3f4R45 is the bijection (forget C).obj (∏ F) ≃ ∀ j, F j with F : J → C and forget C : C ⥤ Type _ is the forgetful functor of a concrete category C (when forget commutes with suitable limits). Presumably, if you need more "shapes", this should be added to this new file Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory when #8507 is merged.

[Christian Merten]

Thanks for the pointer. I think FintypeCat is somewhat special, because the product is not only the product in types after applying forget FintypeCat (aka FintypeCat.incl) but is actually of (∏ F). Not having to compose everything with FintypeCat.incl makes it slightly less annoying to work with.

[Adam Topaz]

You could construct an explicit limit cone with a particular cone point.

[Christian Merten]

I think thats what's done in docs#CategoryTheory.Limits.Shapes.Types and this can be adapted easily to the case of FintypeCat. Is that what you are suggesting?

[Christian Merten]

Specifically I did this:

import Mathlib

namespace FintypeCat

def FProd.fst {X Y : FintypeCat.{u}} : FintypeCat.of (X × Y) ⟶ X := Prod.fst

@[simps! pt]
def binaryProductCone (X Y : FintypeCat.{u}) : BinaryFan X Y :=
  BinaryFan.mk FProd.fst Prod.snd

@[simp]
theorem binaryProductCone_fst (X Y : FintypeCat.{u}) : (binaryProductCone X Y).fst = Prod.fst :=
  rfl

@[simp]
theorem binaryProductCone_snd (X Y : FintypeCat.{u}) : (binaryProductCone X Y).snd = Prod.snd :=
  rfl

/-- The product type `X × Y` is a binary product for `X` and `Y`. -/
@[simps!]
def binaryProductLimit (X Y : FintypeCat.{u}) : IsLimit (binaryProductCone X Y) where
  lift (s : BinaryFan X Y) x := (s.fst x, s.snd x)
  fac _ j := Discrete.recOn j fun j => WalkingPair.casesOn j rfl rfl
  uniq _ _ w := funext fun x => Prod.ext (congr_fun (w ⟨WalkingPair.left⟩) x) (congr_fun (w ⟨WalkingPair.right⟩) x)

/-- The category of types has `X × Y`, the usual cartesian product,
as the binary product of `X` and `Y`.
-/
@[simps]
def binaryProductLimitCone (X Y : FintypeCat.{u}) : Limits.LimitCone (pair X Y) :=
  ⟨_, binaryProductLimit X Y⟩

/-- The categorical binary product in `Type u` is cartesian product. -/
noncomputable def binaryProductIso (X Y : FintypeCat.{u}) : Limits.prod X Y ≅ FintypeCat.of (X × Y) :=
  limit.isoLimitCone (binaryProductLimitCone X Y)

@[elementwise (attr := simp)]
theorem binaryProductIso_hom_comp_fst (X Y : FintypeCat.{u}) :
    (binaryProductIso X Y).hom ≫ _root_.Prod.fst = Limits.prod.fst :=
  limit.isoLimitCone_hom_π (binaryProductLimitCone X Y) ⟨WalkingPair.left⟩

@[elementwise (attr := simp)]
theorem binaryProductIso_hom_comp_snd (X Y : FintypeCat.{u}) :
    (binaryProductIso X Y).hom ≫ _root_.Prod.snd = Limits.prod.snd :=
  limit.isoLimitCone_hom_π (binaryProductLimitCone X Y) ⟨WalkingPair.right⟩

end FintypeCat

[Christian Merten]

which is just copy paste from docs#CategoryTheory.Limits.Shapes.Types but adapted to FintypeCat.

[Joël Riou]

I think the best solution is to rely on what we have for general concrete categories (and develop more if you need more shapes), and then just use FintypeCat.equivEquivIso {A B : FintypeCat} : A ≃ B ≃ (A ≅ B) in order to translate the equivalences in Type into isomorphisms in FintypeCat if this is really what you need. I do not think we want to duplicate too much of the code.

[Christian Merten]

I see your argument, although to have a usable API for FintypeCat one needs to add quite a few additional simp lemmas (e.g. binaryProductIso_hom_comp_fst above) that will be going back and forth with isomorphisms and applying the Type u equivalent at the right place. So I think in the end, not just replicating leads to the same amount of code.

[Joël Riou]

In case of finite products and using #8507, the following code does the job:

import Mathlib.CategoryTheory.Limits.FintypeCat
import Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

universe u

open CategoryTheory Limits

namespace FintypeCat

variable {J : Type} [DecidableEq J] [Fintype J] (X : J → FintypeCat.{u})

noncomputable instance : PreservesLimit (Discrete.functor X) (forget FintypeCat.{u}) :=
  (inferInstance : PreservesLimit _ incl.{u})

noncomputable def productIso :
    (∏ X) ≅ of (∀ j, X j) :=
  equivEquivIso (Concrete.productEquiv X)

@[simp]
lemma productIso_hom_apply_apply (x : (forget FintypeCat.{u}).obj (∏ X)) (j : J) :
    (productIso X).hom x j = Pi.π X j x :=
  Concrete.productEquiv_apply_apply X x j

@[simp]
lemma productIso_inv_apply_π (x : ∀ j, X j) (j : J) :
    Pi.π X j ((productIso X).inv x) = x j :=
  Concrete.productEquiv_symm_apply_π X x j

end FintypeCat

[Christian Merten]

Indeed, this looks very convincing, thanks. When #8507 is merged, I'll try to add the FintypeCat version of the shapes I need. I guess this should then go in a new file Mathlib.CategoryTheory.Limits.Shapes.FintypeCat?

[Joël Riou]

Yes, this is the right location!