alternate (defeq) `nerve` definition

Stream: Infinity-Cosmos

[Thomas Murrills]

I was working on #25010 and trying to understand the definition of nerve, and realized it could be written directly in terms of the yoneda embedding, with no reference to ComposableArrows. Now, that might not be desirable, since I'm guessing there are lemmas about ComposableArrows! :) But thought I'd share in case it's of any interest or belongs anywhere.

Something of some minor interest here is a universe-polymorphic version of the yoneda embedding specifically for Cat (relying on Functor instead of Hom) which seems necessary for this to work. (Does this exist already somewhere?)

import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.CategoryTheory.ComposableArrows

open CategoryTheory.Category Simplicial

namespace CategoryTheory

def Cat.yoneda.{v', u', v, u} : Cat.{v, u} ⥤ Cat.{v', u'}ᵒᵖ ⥤ Type (max u v u' v') where
  obj X :=
    { obj := fun Y => Y.unop ⥤ X
      map := fun f g => f.unop ⋙ g
    }
  map f :=
    { app := fun _ g => g ⋙ f }

universe v u

@[simps!] -- necessary?
def nerveYoneda (C : Type (u)) [Category.{v} C] : SSet.{max u v} :=
  SimplexCategory.toCat.op ⋙ Cat.yoneda.obj (.of C)

-- Current definition
/-- The nerve of a category -/
@[simps]
def nerve (C : Type u) [Category.{v} C] : SSet.{max u v} where
  obj Δ := ComposableArrows C (Δ.unop.len)
  map f x := x.whiskerLeft (SimplexCategory.toCat.map f.unop)
  -- `aesop` can prove these but is slow, help it out:
  map_id _ := rfl
  map_comp _ _ := rfl

theorem nerveYoneda_eq_nerve : nerveYoneda = nerve := rfl

end CategoryTheory

[Thomas Murrills]

Aside: I also wrote down the defs for functorially lifting Cat.{u,v} to Cat.{max u u', max v v'}, planning to insert it as a functor between SimplexCategory.toCat.op and the regular yoneda.

This turned out to be awkward, and rewriting yoneda for Cat was nicer. But I'll put it here in case anyone ever needs it and searches Zulip for inspiration... :)

Note: ULiftCat is similar to ULiftHom, but effectively lifts the whole category, objects and arrows, at once.

ulift for Cat

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory.Category

namespace CategoryTheory

def ULiftCat.{u', v', u} (C : Type u) : Type (max u u') :=
  let _ := ULift.{v'} Unit -- is there a better way?
  ULift.{u'} C

instance uliftCat.{u', v', u, v} (C : Type u) [Category.{v} C] :
    Category.{max v v'} (ULiftCat.{u', v'} C) where
  Hom X Y := ULift <| X.down ⟶ Y.down
  id X := .up <| 𝟙 X.down
  comp f g := .up <| f.down ≫ g.down

@[simps]
def Functor.up.{u', v', u, v} {X Y : Type u} [Category.{v} X] [Category.{v} Y] (F : X ⥤ Y) :
    ULiftCat.{u',v'} X ⥤ ULiftCat.{u',v'} Y where
  obj := fun ⟨x⟩ => ULift.up <| F.obj x
  map := fun ⟨f⟩ => ULift.up <| F.map f

@[simps] -- should this be named `Cat.ULift` instead?
def Cat.up.{u', v', u, v} : Cat.{v,u} ⥤ Cat.{max v v', max u u'} where
  obj C := .of <| ULiftCat.{u', v'} C
  map := .up

[Emily Riehl]

Conceptually, it seems simpler to have something like ULiftCat to lift the whole category at once, but maybe there's a design reason I don't know that this is a bad idea? I'd be curious for others to weigh in.

I wonder, though, if the order of your universe arguments should be permuted to match the usual convention for Cat.{v,u} with the v for the homs and the u for the objects.

[Emily Riehl]

I'm quite surprised by

theorem nerveYoneda_eq_nerve : nerveYoneda = nerve := rfl

given how many composites go into SimplexCategory.toCat. @Joël Riou could you comment?

[Kevin Buzzard]

theorem nerveYoneda_eq_nerve : nerveYoneda = nerve := by
  unfold nerveYoneda nerve
  ext 𝓒 h𝓒
  dsimp
  unfold ComposableArrows
  -- are functors identical?
  apply Functor.ext -- just to see what's going on
  · -- are morphisms identical?
    dsimp
    intro X Y f
    unfold ComposableArrows.whiskerLeft
    unfold Cat.yoneda
    dsimp
    rw [comp_id, id_comp] -- I am slightly confused about why these are `rfl` here
    -- ⊢ (fun g => ⋯.functor ⋙ g) = fun x => ⋯.functor ⋙ x
    -- `⋯.functor` means `Monotone.functor` here
    rfl
  · -- are objects identical?
    intro X
    dsimp
    unfold Cat.yoneda
    dsimp
    unfold forget₂ HasForget₂.forget₂ PartOrd.hasForgetToPreord
    dsimp
    unfold Lat.hasForgetToPartOrd
    dsimp
    unfold LinOrd.hasForgetToLat
    dsimp
    unfold NonemptyFinLinOrd.hasForgetToLinOrd
    dsimp
    unfold InducedCategory.hasForget₂
    dsimp only
    unfold inducedFunctor NonemptyFinLinOrd.toLinOrd NonemptyFinLinOrd.of
    -- RHS is `Fin ((Opposite.unop X).len + 1) ⥤ 𝓒`
    conv_lhs =>
      dsimp -- LHS is also `Fin ((Opposite.unop X).len + 1) ⥤ 𝓒`

You can close any goal at any point with rfl and it gets harder and harder to stop Lean from closing the goal the more you unfold.

[Joël Riou]

In basic concrete categories, compositions with identities are rfl, which makes rfl a quite powerful tactic...

[Thomas Murrills]

Emily Riehl said:

I wonder, though, if the order of your universe arguments should be permuted to match the usual convention for Cat.{v,u} with the v for the homs and the u for the objects.

They should! :grinning_face_with_smiling_eyes: (I realized that v came before u everywhere only after writing this code, but only went back to edit Cat.yoneda...)

[Thomas Murrills]

(Also, I'm realizing that Functor.up should (after swapping the order of universes in ULiftCat) not insist that the universes of the two categories are the same:)

@[simps]
def Functor.up.{v'₁, u'₁, v'₂, u'₂, v₁, u₁, v₂, u₂} {X : Type u₁} {Y : Type u₂}
    [Category.{v₁} X] [Category.{v₂} Y] (F : X ⥤ Y) :
    ULiftCat.{v'₁, u'₁} X ⥤ ULiftCat.{v'₂, u'₂} Y where
  obj := fun ⟨x⟩ => ULift.up <| F.obj x
  map := fun ⟨f⟩ => ULift.up <| F.map f