FintypeCat API

Stream: mathlib4

[Christian Merten]

I am wondering what parts of the API for types should be mirrored for FintypeCat. Certainly its preferable to create the API for ConcreteCategory instead, but I can't make this specialize to FintypeCat. Example:

import Mathlib

open CategoryTheory

variable {C D : Type*} [Category C] [Category D] [ConcreteCategory D] (F : C ⥤ D)
 {X Y : C} (f : X ≅ Y)

attribute [local instance] ConcreteCategory.hasCoeToSort
attribute [local instance] ConcreteCategory.instFunLike

@[simp]
lemma FunctorToConcrete.map_inv_map_hom_apply (x : F.obj X) :
    ⇑(F.map f.inv) (⇑(F.map f.hom) x) = x := by
  rw [← comp_apply]
  show ⇑((F.mapIso f).hom ≫ (F.mapIso f).inv) x = x
  rw [Iso.hom_inv_id, id_apply]

example (F : C ⥤ FintypeCat) {X Y : C} (f : X ≅ Y) (x : F.obj X) :
    F.map f.inv (F.map f.hom x) = x := by
  -- erw [FunctorToConcrete.map_inv_map_hom_apply F f x] fails
  -- rw [FunctorToConcrete.map_inv_map_hom_apply F f x] fails
  -- simp only [FunctorToConcrete.map_inv_map_hom_apply F f x] fails
  -- simp does not make progress
  exact FunctorToConcrete.map_inv_map_hom_apply F f x

Is this expected? Can I make this work?

[Adam Topaz]

I’m not sure what you mean about this not specializing to FintypeCat….

[Adam Topaz]

Do these lemmas not work when D is FintypeCat?

[Christian Merten]

The lemma works, but the general simp lemma, stated for concrete categories, is not applied by simp when D is FintypeCat, note that even explicitly using it with simp only [..] does not work.

[Adam Topaz]

That’s annoying…

[Adam Topaz]

Can you trace the simp to see why it fails?

[Christian Merten]

That's what I tried to demonstrate with the example above.

[Christian Merten]

Adam Topaz said:

Can you trace the simp to see why it fails?

How do I do this?

[Adam Topaz]

set_option trace.Meta.Simp true (if i remember the name of the option correctly… I’m on mobile right now)

[Christian Merten]

I found it: Its set_option trace.Meta.Tactic.simp true.
The following code:

set_option trace.Meta.Tactic.simp true

example (F : C ⥤ FintypeCat) {X Y : C} (f : X ≅ Y) (x : F.obj X) :
    F.map f.inv (F.map f.hom x) = x := by
  simp only [FunctorToConcrete.map_inv_map_hom_apply F f x]

yields

▶ 45:3-45:60: error:
simp made no progress

▶ 45:3-45:60: information:
[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
      ?a = ?a
    with
      F.toPrefunctor.map f.inv (F.toPrefunctor.map f.hom x) = x

[Christian Merten]

I guess that means the only thing simp tried is rfl?

[Adam Topaz]

Hmmm…

[Adam Topaz]

What happens if you explicitly specify universes?

[Adam Topaz]

docs#CategoryTheory.ConcreteCategory

[Christian Merten]

Same result:

#check FunctorToConcrete.map_inv_map_hom_apply

CategoryTheory.FunctorToConcrete.map_inv_map_hom_apply.{u_5, u_4, u_3, u_2, u_1} {C : Type u_1} {D : Type u_2}
  [inst✝ : Category.{u_5, u_1} C] [inst✝¹ : Category.{u_3, u_2} D] [inst✝² : ConcreteCategory D] (F : C ⥤ D) {X Y : C}
  (f : X ≅ Y) (x : (forget D).toPrefunctor.obj (F.toPrefunctor.obj X)) :
  (F.toPrefunctor.map f.inv) ((F.toPrefunctor.map f.hom) x) = x

Specifiyng all universes:

example (F : C ⥤ FintypeCat.{w}) {X Y : C} (f : X ≅ Y) (x : F.obj X) :
    F.map f.inv (F.map f.hom x) = x := by
  -- exact FunctorToConcrete.map_inv_map_hom_apply.{u₂, w, w, w+1, u₁} F f x works
  simp only [FunctorToConcrete.map_inv_map_hom_apply.{u₂, w, w, w+1, u₁} F f x]

yields the same trace.

[Adam Topaz]

Does lean even find the concrete category instance?

[Christian Merten]

Yes:

#synth ConcreteCategory.{w, w, w+1} FintypeCat.{w}

▶ 45:1-45:51: information:
FintypeCat.concreteCategoryFintype

[Christian Merten]

It must be related to the function coercions: Even when replacing every occurence of D in the simp lemma with FintypeCat, it still does not work:

@[simp]
lemma FintypeCat.map_inv_map_hom_apply (F : C ⥤ FintypeCat.{w}) {X Y : C} (f : X ≅ Y)
    (x : F.obj X) : ⇑(F.map f.inv) (⇑(F.map f.hom) x) = x := by
  rw [← comp_apply]
  show ⇑((F.mapIso f).hom ≫ (F.mapIso f).inv) x = x
  rw [Iso.hom_inv_id, id_apply]

example (F : C ⥤ FintypeCat.{w}) {X Y : C} (f : X ≅ Y) (x : F.obj X) :
    F.map f.inv (F.map f.hom x) = x := by
  simp only [FintypeCat.map_inv_map_hom_apply F f x] -- fails with the same trace

When removing the explicit ⇑ coercions (which are not needed in the FintypeCat case), it works. But for general concrete categories the simp lemma can't be stated without ⇑ (or at least I did not succeed in doing so).

[Christian Merten]

This is a bit minimized:

import Mathlib

variable {X Y : FintypeCat} (f g : X ⟶ Y) (h : ⇑f = ⇑g)

example (x : X) : f x = g x := by
  simp only [h] --fails

Probably this is expected, but it makes working in FintypeCat horrible without copying every API lemma from the category of types.

[Christian Merten]

Maybe your bundled function approach would also make this less annoying?

[Adam Topaz]

Yeah I think that’s the issue here