the coherent isomorphism

Stream: Infinity-Cosmos

[Emily Riehl]

A preliminary version of the homotopy coherent isomorphism is defined in a branch. We defined everything inductively and then proved a few simple lemmas with very inefficient inductive proofs. Golfing suggestions are very welcome. I'm also trying to determine whether walkingIso is already in mathlib.

[Joël Riou]

I would not think walkingIso is already in mathlib, but is not it true that in this category, given two objects X and Y, there is exactly one morphisms from X to Y, in which case the definition of Hom could be just Unit:

def category (A : Type u) : Category A where
  -- `A` should be replaced by a type-synonym in order to make an instance out of this
  Hom _ _ := Unit
  id _ := ⟨⟩
  comp _ _ := ⟨⟩

Is there a canonical name for such a "contractible" category with a given set of objects A?

[Joël Riou]

Then, the main construction becomes:

inductive WalkingIso : Type where
  | zero
  | one

instance : Category WalkingIso where
  Hom _ _ := Unit
  id _ := ⟨⟩
  comp _ _ := ⟨⟩

def WalkingIso.ofIso {C : Type u} [Category.{v} C] {X Y : C} (e : X ≅ Y) :
    WalkingIso ⥤ C where
  obj := fun
    | zero => X
    | one => Y
  map := @fun
    | zero, zero, _ => 𝟙 _
    | zero, one,  _ => e.hom
    | one,  zero, _ => e.inv
    | one,  one,  _ => 𝟙 _

[Emily Riehl]

Joël Riou said:

I would not think walkingIso is already in mathlib, but is not it true that in this category, given two objects X and Y, there is exactly one morphisms from X to Y, in which case the definition of Hom could be just Unit:

def category (A : Type u) : Category A where
  -- `A` should be replaced by a type-synonym in order to make an instance out of this
  Hom _ _ := Unit
  id _ := ⟨⟩
  comp _ _ := ⟨⟩

Is there a canonical name for such a "contractible" category with a given set of objects A?

I've seen it called the "indiscrete" or "chaotic" category, though "contractible" is perhaps an even better term. This defines the right adjoint to the forgetful functor ob : Cat -> Set, whose right adjoint is given by the discrete category construction.

It seems to me that this notion isn't in mathlib either. I have some students who are looking for a beginner project, so I might suggest this to them: define such categories (mirroring the existing definition of discrete categories) and construct these adjunctions.

[Adam Topaz]

@Emily Riehl we do have docs#CategoryTheory.Discrete

[Adam Topaz]

Oh, I see, you're referring to the adjunction. Yes, you're right, we probably don't have that, although the API for Discrete does essentially give you the adjunction via docs#CategoryTheory.Discrete.functor docs#CategoryTheory.Discrete.natTrans etc.

[Emily Riehl]

Yes, I should have been clearer. Thanks for the suggestion.

[Emily Riehl]

Joël Riou said:

Then, the main construction becomes:

inductive WalkingIso : Type where
  | zero
  | one

instance : Category WalkingIso where
  Hom _ _ := Unit
  id _ := ⟨⟩
  comp _ _ := ⟨⟩

def WalkingIso.ofIso {C : Type u} [Category.{v} C] {X Y : C} (e : X ≅ Y) :
    WalkingIso ⥤ C where
  obj := fun
    | zero => X
    | one => Y
  map := @fun
    | zero, zero, _ => 𝟙 _
    | zero, one,  _ => e.hom
    | one,  zero, _ => e.inv
    | one,  one,  _ => 𝟙 _

Could you explain @fun? In general, I don't know how to efficiently induct over multiple parameters, particularly implicit ones like we have here.

[Adam Topaz]

@fun makes all the implicit variables explicit.

[Adam Topaz]

in this case (I think) you can just replace map := @fun with map (untested)

[Emily Riehl]

That's giving me a type mismatch error.

[Adam Topaz]

Ok, I was wrong. Anyway, maybe this version is clearer?

def WalkingIso.ofIso {C : Type u} [Category.{v} C] {X Y : C} (e : X ≅ Y) :
    WalkingIso ⥤ C where
  obj x :=
    match x with
    | zero => X
    | one => Y
  map {x y} f :=
    match x, y, f with
    | zero, zero, _ => 𝟙 _
    | zero, one,  _ => e.hom
    | one,  zero, _ => e.inv
    | one,  one,  _ => 𝟙 _

[Adam Topaz]

The point is that the map field only has the morphism as an explicit parameter, with the two objects implicit. Doing @fun makes everything explicit, or alternatively you can match explicitly on the objects and morphism as I have done above.

[Adam Topaz]

One subtle point to note is that you can't use recursion when defining a projection in a structure like this (IMO this is a defect that should be addressed). Here is an example illustrating how to get around this:

structure F where
  f : Nat → Nat

def ff : F where
  f := aux
where aux
  | 0 => 0
  | n+1 => aux n

/-
Lean can't show termination for this:

def gg : F where
  f | 0 => 0
    | n+1 => gg.f n
-/

[Emily Riehl]

Thanks this is a helpful explanation. A question I was asked in my tutorial yesterday that I couldn't answer was whether there's a way to get lean to automatically generate the cases for an induction (like Agda does). After I type match blah with I've been typing out the "| case => sorry" stuff manually for each case.

[Emily Riehl]

I know if you type "induction X Y" then you see the cases in infoview, but I find proofs written with "match X Y" to be much more readable.

[Adam Topaz]

Yes, that's done with code-actions. In vscode if you get the yellow lightbulb to pop up, one of the options would be "generate skeleton for recursive definition" (approx) as one of the options.

[Adam Topaz]

We don't have Agda's nice hole commands for case splitting on specific terms as far as I know.

[Adam Topaz]

For example, in the following

import Mathlib.Tactic

def f : Nat → Nat := _

if you put the cursor at the _, you should get such a lightbulb.

[Adam Topaz]

And indeed it seems that we don't have a nice code action for matching as in the following example

import Mathlib.Tactic

def f (x : Nat) : Nat :=
  match x with

I wish we did have such an action though!

[Emily Riehl]

One more (unrelated) question, while you're here. Do you know who accepts pull requests on the Lean blog? @herostrat made an announcement of this project for me, which is ready to go live if it meets with the moderators' approval:

https://github.com/leanprover-community/blog/pull/91

[Kevin Buzzard]

I don't know who is allowed to pull the trigger but I left an approving review and raised a minor issue.

[Emily Riehl]

There's a new file CoherentIso.lean which incorporates the suggestions made by several folks here. @Alvaro Belmonte just contributed his very first lean code, in the file CodiscreteCat.lean on codiscrete categories.

[Emily Riehl]

It would be good to PR the codiscrete stuff to mathlib at some point, so feedback here would be very helpful. In particular, Alvaro gives two proofs that the codiscrete category functor is right adjoint to the object functor. I wasn't sure which is best. He could extract the data of the other and leave it as auxiliary definitions/theorems.

[Emily Riehl]

/-- A function induces a functor between codiscrete categories.-/
def funToFunc {A B : Type u} (f : A → B) : Codiscrete A ⥤ Codiscrete B where
  obj a := f a
  map _ := ⟨⟩

def functor : Type u ⥤ Cat.{0,u} where
  obj A := Cat.of (Codiscrete A)
  map := funToFunc

open Adjunction Cat

/-- For a category `C` and type `A`, there is an equivalence between functions `objects.obj C ⟶ A`
and functors `C ⥤ Codiscrete A`.-/
def homEquiv' (C : Cat) (A : Type*) : (objects.obj C ⟶ A) ≃ (C ⟶ functor.obj A) where
  toFun := lift
  invFun := invlift
  left_inv _ := rfl
  right_inv _ := rfl

/-- The functor that turns a type into a codiscrete category is right adjoint to the objects
functor.-/
def adj : objects ⊣ functor := mkOfHomEquiv
  {
    homEquiv := homEquiv'
    homEquiv_naturality_left_symm := fun _ _ => Eq.refl _
    homEquiv_naturality_right := fun _ _ => Eq.refl _
  }

/-- A second proof of the same adjunction.  -/
def adj' : Cat.objects ⊣ functor where
  unit := {
    app := fun _ => {
      obj := fun _ => _
      map := fun _ => ⟨⟩
    }
  }
  counit := {
    app := fun _ => id
  }
  left_triangle_components := by
    intro _
    simp only [Functor.id_obj, Functor.comp_obj, id_eq]
    rfl
  right_triangle_components := by
    intro _
    simp only [Functor.id_obj, Functor.comp_obj, id_eq]
    rfl

[Dagur Asgeirsson]

adj' looks like aesop can take care of the triangle identities (if that's the case the fields can be erased)

[Alvaro Belmonte]

I finish doing the PR# #17174 of codiscrete categories to mathlib. Since I am still pretty new to lean I don't know what else I could tackle, if there is anything else I could do for the project any pointers would be greatly appreciated.