equivIsoLimit for cones over different diagrams?

Stream: new members

[Shanghe Chen]

Hi I saw CategoryTheory.Limits.IsLimit.equivIsoLimit shows that two isomorphic cones over the same diagram give limit or not at the same time. Is it similar theorem for two cones over different diagrams with the same shape?

[Joël Riou]

We have docs#CategoryTheory.Limits.IsLimit.postcomposeHomEquiv

[Shanghe Chen]

Ah awesome :tada: I am trying to read the doc and using it

[Shanghe Chen]

Btw do we have theorem turning a cone into a diagram? It seems similar to WidePullbackShape or WidePushoutShape but with also morphisms indexed by morphisms in the original diagram.

[Shanghe Chen]

image.png
as said in Riehl's _Category Theory in Context_

[Shanghe Chen]

I am trying

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
set_option autoImplicit false
universe v u v' u'

noncomputable section

open CategoryTheory Category

variable {C : Type u} [Category.{v} C]
variable (J : Type u') [Category.{v'} J]
variable {F : J ⥤ C}
variable (G : J ⥤ C)

def AddInitObj := Option J

namespace AddInitObj
inductive Hom : AddInitObj J -> AddInitObj J -> Type u'
  | id : ∀ X, Hom X X
  | term : ∀ j : J, Hom (some j) none
  | mor : ∀ j j' : J, ∀ (f: j ⟶ j'), Hom (some j) (some j')
  deriving DecidableEq
end AddInitObj

But it seems there is some universe level error saying

invalid universe level in constructor 'AddInitObj.Hom.mor', parameter 'f' has type
  j ⟶ j'
at universe level
  v'+1
it must be smaller than or equal to the inductive datatype universe level
  u'+1

[Kevin Buzzard]

[Category.{v'} J] means "Hom sets in J are in universe v'", so your Homs for AddInitObj J should also be taking values in universe v'.

[Shanghe Chen]

Ah the following version works for smallcategory:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
set_option autoImplicit false
universe v u v' u'

noncomputable section

open CategoryTheory Category

variable {C : Type u} [Category.{v} C]
variable (J : Type u') [SmallCategory J]
variable {F : J ⥤ C}
variable (G : J ⥤ C)

def AddInitObj := Option J

namespace AddInitObj
inductive Hom : AddInitObj J -> AddInitObj J -> Type u'
  | id : ∀ X, Hom X X
  | term : ∀ j : J, Hom (some j) none
  | mor : ∀ j j' : J, ∀ (f: j ⟶ j'), Hom (some j) (some j')
end AddInitObj

maybe I can try both postcomposeHomEquiv and turn cone into diagram and prove similar result hhhh

[Shanghe Chen]

Yeah changing to

inductive Hom : AddInitObj J -> AddInitObj J -> Type v'

gives error at the line | id : ∀ X, Hom X X now. Declaring J SmallCategory seems OK now :tada:

[Joël Riou]

We have WithInitial, see CategoryTheory.WithTerminal.

[Shanghe Chen]

Ah I didn’t notice it. Thank you very much :blush: