conical simplicial limits

Stream: Infinity-Cosmos

[Emily Riehl]

I've been experimentally adding things to @Dagur Asgeirsson's file on conical limits and have run into a universe error I don't understand.

The file starts with some variables

variable {J C : Type*} [Category J] [Category C] [SimplicialCategory C]

while I thought was identical to writing

universe u v u₁ v₁
variable {J : Type u₁} [Category.{v₁} J]
variable {C : Type u} [Category.{v} C] [SimplicialCategory C]

But when I replace the former with the latter it breaks a bunch of stuff in his proof that conical limits induce an isomorphism. Any idea what's up?

[Emily Riehl]

The reason I'm trying to be more explicit about universes is I'm having trouble defining HasConicalLimits which refers to a simplicial category that has all conical limits up to the size of its hom simplicial sets.

[Matthew Ballard]

The former creates universe metavariables. These metavariables can secretly hide universe constraints in the code.

[Matthew Ballard]

Specifically the undecorated Category classes

[Adam Topaz]

We need a [Category* C] elaborator!

[Adam Topaz]

Here's a prototype:

import Mathlib

elab "Category*" C:term : term => do
  let v ← Lean.Meta.mkFreshLevelMVar
  let C ← Lean.Elab.Term.elabTerm C none
  let .sort (.succ u) := (← Lean.Meta.inferType C) | throwError "ERROR"
  let cat : Lean.Expr := .const ``CategoryTheory.Category [v,u]
  Lean.Elab.Term.levelMVarToParam (.app cat C)

open CategoryTheory in
example (C : Type*) [Category* C] (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) : X ⟶ Z := f ≫ g

[Emily Riehl]

If I've understood @Matthew Ballard's point, it seems that in the code below there are secret universe constraints that the universe metavariables automatically configure themselves to satisfy. But when I replace them with named universe variables, the named variables don't satisfy the constraint unless explicitly told about it.

[Emily Riehl]

I think I see the issue. One of the errors caused when using named variables is here

noncomputable def limitComparison (X : C) :
    sHom X c.pt ⟶ limit (F ⋙ (sHomFunctor C).obj (op X)) :=
  limit.lift _ (((sHomFunctor C).obj (op X)).mapCone c)

where the error message is failed to synthesize HasLimit (F ⋙ (sHomFunctor C).obj (op X)). This functor is valued in a presheaf category valued in Type v so should have a limit if v is at least max u₁ v₁.

[Emily Riehl]

Unfortunately the code is still broken with

variable {J : Type u₁} [Category.{v₁} J]
variable {C : Type u} [Category.{max u₁ v₁} C] [SimplicialCategory C] {F : J ⥤ C} (c : Cone F)

though it works with

variable {J : Type v} [Category.{v} J]
variable {C : Type u} [Category.{v} C] [SimplicialCategory C] {F : J ⥤ C} (c : Cone F)

I'm not sure why...

[Kim Morrison]

Adam Topaz said:

Here's a prototype:

import Mathlib

elab "Category*" C:term : term => do
  let v ← Lean.Meta.mkFreshLevelMVar
  let C ← Lean.Elab.Term.elabTerm C none
  let .sort (.succ u) := (← Lean.Meta.inferType C) | throwError "ERROR"
  let cat : Lean.Expr := .const ``CategoryTheory.Category [v,u]
  Lean.Elab.Term.levelMVarToParam (.app cat C)

open CategoryTheory in
example (C : Type*) [Category* C] (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) : X ⟶ Z := f ≫ g

Looks good to me. Could we combine it with a linter that forbids bare [Category C]?

[Adam Topaz]

Well, one thing I would still like to experiment with is arranging the morphism universe parameter to come before the object one.

[Adam Topaz]

But I won’t have time to try doing that seriously for a couple of days

[Adam Topaz]

Also matching on .succ u isn’t ideal

[Dagur Asgeirsson]

@Emily Riehl I've opened https://github.com/emilyriehl/infinity-cosmos/pull/13 which fixes the universe issues in this file. It adds the assumption [HasLimitsOfShape J SSet] (which will always hold if J is "small enough") to fix the issues in the section about the comparison maps. It also reorders the universe arguments so that HasConicalLimitsOfSize has the desired meaning.

[Emily Riehl]

Thanks @Dagur Asgeirsson

[Emily Riehl]

I've been trying to build out some API around the conical simplicial limits, but I could use some advice on
(a) structuring things property (eg should these be theorems or instances) and
(b) help in filling some sorries (where I'm stuck).
This all concerns the Limits file under SimplicialCategory created by @Dagur Asgeirsson

Specifically, I'd like to be able to add an assumption that a simplicial category K has a certain type of conical simplicial limits and have lean infer that K then has the underlying unenriched limits of the same type.

For example

instance HasConicalProducts_hasProducts [HasConicalProducts C] : HasProducts C := by sorry

[Emily Riehl]

Some results/constructions in this direction are straightforward (aside from the choice of variables names; advice is very welcome):

/--
A limit cone `c` in a simplicial category `A` is a *simplicially enriched limit* if for every
`X : C`, the cone obtained by applying the simplicial coyoneda functor `(X ⟶[A] -)` to `c` is a
limit cone in `SSet`.
-/
structure IsSLimit where
  isLimit : IsLimit c
  isSLimit (X : C) : IsLimit <| ((sHomFunctor C).obj (op X)).mapCone c

/-- Conical simplicial limits are also limits in the unenriched sense.-/
def IsSLimit_islimit (slim : IsSLimit c) : IsLimit c := slim.isLimit

[Dagur Asgeirsson]

Everything of the form "has conical limit -> has limit" is can be an instance.
Regarding the sorry in HasConicalLimitsOfSize_hasLimitsOfSize I can take a look a bit later, but I suspect the problem is that Lean is making up some universes and everything should just work if you provide the HasConicalLimitsOfSize instance and the HasLimitsOfSize that you want to prove with (the same) explicit universes

[Emily Riehl]

I managed to close these sorries but with horrible proofs. Can anyone explain what I'm doing wrong?

[Emily Riehl]

Specifically

/-- `C` has all conical limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
if it has conical limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
-/
@[pp_with_univ]
class HasConicalLimitsOfSize (C : Type u) [Category.{v} C] [SimplicialCategory C] : Prop where
  /-- All functors `F : J ⥤ C` from all small `J` have conical limits -/
  has_conical_limits_of_shape : ∀ (J : Type u₁) [Category.{v₁} J], HasConicalLimitsOfShape J C := by
    infer_instance

instance HasConicalLimitsOfSize_hasLimitsOfSize [HasConicalLimitsOfSize.{v₂, u₂, v, u} C] :
    HasLimitsOfSize.{v₂, u₂, v, u} C where
  has_limits_of_shape := by
    intro J hyp
    constructor
    intro F
    have lem1 : HasConicalLimitsOfSize.{v₂, u₂, v, u} C := by infer_instance
    have lem2 : HasConicalLimitsOfShape J C := by
      apply lem1.has_conical_limits_of_shape
    have : HasConicalLimit F := by
      apply lem2.has_conical_limit
    exact HasConicalLimit_hasLimit F

[Emily Riehl]

variable (C) in
class HasConicalProducts : Prop where
  /-- All discrete diagrams of bounded size have conical products.  -/
  has_conical_limits_of_shape : ∀ J : Type w, HasConicalLimitsOfShape (Discrete J) C :=
    by infer_instance
--  has_limits_of_shape : ∀ { I : Type w} (f : I → C), HasConicalProduct f := by
--    infer_instance

instance HasConicalProducts_hasProducts [hyp : HasConicalProducts.{w, v, u} C] :
     HasProducts.{w, v, u} C := by
  intro I
  constructor
  intro f
  have := hyp.has_conical_limits_of_shape I
  have : HasConicalLimit f := by infer_instance
  exact HasConicalLimit_hasLimit f

[Emily Riehl]

I couldn't figure out how to reference the hypothesis HasConicalProducts in the latter without giving it a name; I got a circular universe error I hadn't seen before.

[Emily Riehl]

It's possible that some of the issue here has to do with whether products are indexed by functions out of a type or functors out a discrete category. In mathlib HasProduct is indexed by functions out of a type but HasProducts references limits of discrete diagrams (indexed by functors out of a discrete category). See the commented out alternative form of has_conical_limits_of_shape.

[Dagur Asgeirsson]

I'm taking a look

[Dagur Asgeirsson]

The issue was just that the instances HasConicalLimitsOfShape -> HasConicalLimit and HasConicalLimitsOfSize -> HasConicalLimitsOfShape weren't declared until further down in the file. Now the proofs are basically just inferInstance

[Dagur Asgeirsson]

https://github.com/emilyriehl/infinity-cosmos/pull/38

[Emily Riehl]

Thank you. Someday I hope I won't be so bad at this... ;)

[Kevin Buzzard]

It's certainly quite the learning curve, for sure! Moreover I think learning category theory is a very hard place to start. I remember the first Lean for the Curious Mathematician in something like 2020, when I had felt like I was on top of the system, and Kim Morrison had put some category theory exercises together for the attendees, and after about 2 hours of working on them I had just about stumbled through the first one -- and this was after we'd written the perfectoid space paper!

[Dagur Asgeirsson]

Especially the API for limits takes some getting used to

[Emily Riehl]

I'm back with my regularly scheduled trouble with instances and universe levels.

@Mario Carneiro pointed out (of course) that since an ∞-cosmos has conical products it should have a conical terminal object. Unfortunately, lean does not agree.

I tried to remedy this situation as follows:

section ConicalProducts
variable {C : Type u} [Category.{v} C] [SimplicialCategory C]

/-- An abbreviation for `HasSLimit (Discrete.functor f)`. -/
abbrev HasConicalProduct { I : Type w} (f : I → C) := HasConicalLimit (Discrete.functor f)

instance HasConicalProduct_hasProduct {I : Type w} (f : I → C) [HasConicalProduct f] :
    HasProduct f := HasConicalLimit_hasLimit (Discrete.functor f)

variable (C) in
class HasConicalProducts : Prop where
  /-- All discrete diagrams of bounded size have conical products.  -/
  has_conical_limits_of_shape : ∀ J : Type w, HasConicalLimitsOfShape (Discrete J) C :=
    by infer_instance
--  has_limits_of_shape : ∀ { I : Type w} (f : I → C), HasConicalProduct f := by
--    infer_instance

instance HasConicalProducts_hasProducts [hyp : HasConicalProducts.{w, v, u} C] :
    HasProducts.{w, v, u} C := by
  intro I
  constructor
  intro f
  have := hyp.has_conical_limits_of_shape I
  have : HasConicalLimit f := by infer_instance
  exact HasConicalLimit_hasLimit f

instance HasConicalProducts_hasConicalTerminal [hyp : HasConicalProducts.{0, v, u} C] :
    HasConicalTerminal C := hyp.has_conical_limits_of_shape PEmpty.{1}

instance HasConicalProducts_hasConicalTerminal' [hyp : HasConicalProducts C] :
    HasConicalTerminal C :=
  have inst := hyp.has_conical_limits_of_shape PEmpty
  sorry


end ConicalProducts

[Emily Riehl]

My question is firstly whether the final statement is correct. If so, does anyone have suggestions for how to fill the last sorry.

[Mario Carneiro]

the statement looks correct to me

[Mario Carneiro]

what happens when you just replace the 0 with w?

[Mario Carneiro]

I guess you will need a slightly different PEmpty but otherwise it seems like it would work

[Dagur Asgeirsson]

Since HasConicalTerminal is defined in terms of Discrete.{0} PEmpty, you can't directly infer it. As Mario points out, you could get something like HasConicalLimitsOfShape (Discrete.{w} PEmpty. To get the one of size 0, you'd need an analogue of docs#CategoryTheory.Limits.hasLimitsOfSizeShrink to finish.

Alternatively, since these shapes are equivalent categories, an analogue of docs#CategoryTheory.Limits.hasLimitsOfShape_of_equivalence would work.

In any case, these would both be useful to have

[Emily Riehl]

Thanks for these suggestions. I tried to implement everything (which took me down various rabbit holes to):

variable {J : Type u₁} [Category.{v₁} J]
variable {C : Type u} [Category.{v} C] [SimplicialCategory C]

def hasConicalLimitOfIso.coneIso {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) (X : C) :
    ((sHomFunctor C).obj (op X)).mapCone ((Cones.postcompose α.hom).obj c) ≅
      (Cones.postcompose (isoWhiskerRight α ((sHomFunctor C).obj (op X))).hom).obj
        (((sHomFunctor C).obj (op X)).mapCone c) := sorry

[Emily Riehl]

But despite proving conical analogues of everything you mentioned I still wasn't able to finish this proof:

instance HasConicalProducts_hasConicalTerminal' [hyp : HasConicalProducts.{w, v, u} C] :
    HasConicalTerminal C := by
  unfold HasConicalTerminal
  have inst := hyp.has_conical_limits_of_shape PEmpty
  let eq : PEmpty.{w + 1} ≃ PEmpty.{1} := Equiv.equivPEmpty PEmpty.{w + 1}
  let eq' : Discrete PEmpty.{w + 1} ≃ Discrete PEmpty.{1} :=
    Equiv.equivOfIsEmpty (Discrete PEmpty.{w + 1}) (Discrete PEmpty.{1})
  refine hasConicalLimitsOfShape_of_equivalence (J := Discrete PEmpty.{w+1}) ?_
  sorry

[Emily Riehl]

I think the problem might by the theorems concern equivalences of categories , which confusingly (to me) are denoted with the symbol ≅. But this does not type check in either eq or eq' because

argument
PEmpty.{1}
has type
Type : Type 1
but is expected to have type
Type w : Type (w + 1)

[Dagur Asgeirsson]

Note that equivalence of categories is denoted ≌ (\backcong) and not ≅ (\iso/\cong). Is that the symbol you wrote? It should typecheck between the Discrete PEmpty's (the other ones aren't categories).

[Dagur Asgeirsson]

This works:

import Mathlib

universe w

open CategoryTheory

def eq : Discrete PEmpty.{1} ≌ Discrete PEmpty.{w+1} :=
  Discrete.equivalence (Equiv.equivPEmpty PEmpty.{1})

[Kim Morrison]

(My apologies for the long ago notation choice of \backcong...)

[Emily Riehl]

Dagur Asgeirsson said:

Note that equivalence of categories is denoted ≌ (\backcong) and not ≅ (\iso/\cong). Is that the symbol you wrote? It should typecheck between the Discrete PEmpty's (the other ones aren't categories).

Indeed, this was what I was missing! Hilarious.

[Kim Morrison]

Kim Morrison said:

(My apologies for the long ago notation choice of ≌ ```

If someone wants to fix it, I don't particularly see that it is too late. It would be a fun but probably unlikely experiment to try just overloading ≅. But failing that, what would be better?

[Joël Riou]

I do not think that ≌/≅ needs a fix :-)

[Emily Riehl]

Agreed. It's clearly documented at the start of the file (which I didn't check). Lesson learned.

[Kevin Buzzard]

Mathematicians would not even distinguish the two symbols, this is just a mathlib gotcha.

[Joël Riou]

Mathematicians also use the same symbol -> for a morphism and a functor. I am happy we do not conflate the two :-)

[Mario Carneiro]

I think Kevin is saying that a mathematician would not differentiate between the symbols ≌/≅ when writing. As far as I know, mathematicians do use clearly distinct symbols for equivalence and isomorphism, namely ≃ and ≅ respectively.

[Mario Carneiro]

I tend to agree that mathlib's deliberate use of unicode confusables is a bad habit

[Kevin Buzzard]

It's just one of those things you have to learn, like how every few months someone asks about why a | b works for someone else and not for them, because they didn't realise that "divides" is \|

[Kim Morrison]

Mario Carneiro said:

I think Kevin is saying that a mathematician would not differentiate between the symbols ≌/≅ when writing. As far as I know, mathematicians do use clearly distinct symbols for equivalence and isomorphism, namely ≃ and ≅ respectively.

I dimly remember way back in the day when I settled on backcong, going looking through unicode hoping for the third in the sequence ≃, ≅, ..., to use for the next categorical level. But I didn't find anything.

[Jon Eugster]

In coordination with @Emily Riehl I generalised these from simplicial sets to conical limit over a general enriched ordinary category: https://github.com/emilyriehl/infinity-cosmos/pull/78

@Dagur Asgeirsson would you have the chance to glimpse over the definitions and see if I did things right?
Is there any particular choice for the order of universes at the top?

I would create PR's to mathlib with these additions now

[Dagur Asgeirsson]

I took a quick look and it looks reasonable. You can ping me when the mathlib PR is ready and I can do a proper review on that. I think the name should contain the word Enriched, maybe by putting it in the CategoryTheory.Enriched namespace. Probably CategoryTheory.Enriched.IsLimit is too confusing, so maybe CategoryTheory.Enriched.IsConicalLimit or CategoryTheory.Enriched.IsEnrichedLimit.

[Dagur Asgeirsson]

Also, when you open the mathlib PR, make sure to mirror the file structure of the ordinary limit API as much as possible

[Jon Eugster]

Thanks! I think Emily suggested IsConicalLimit over IsEnrichedLimit so maybe CategoryTheory.Enriched.IsConicalLimit?

[Emily Riehl]

I like "conical" because in the future we will develop a more general theory of enriched limits, including cotensors (formalized by @Daniel Carranza) and more general weighted limits. Each of these deserve to be called "enriched limits" but the term "conical" distinguishes the enriched limits which have ordinary cone shapes.

[Emily Riehl]

@Dagur Asgeirsson and @Joël Riou do you have any suggestions for the CategoryTheory/Enriched directory structure?

Right now mathlib has Basic.lean (defining enriched categories) Ordinary.lean (defining enriched ordinary categories) and other files like Opposite.lean which develop opposite categories for both enriched categories and enriched ordinary categories. This seems reasonable to me (for now at least).

Following this, I'd suggest @Jon Eugster's InfinityCosmos/ForMathlib/Enriched/Ordinary/Limits get filed as Mathlib/Enriched/ConicalLimits.

[Joël Riou]

Emily Riehl said:

Dagur Asgeirsson and Joël Riou do you have any suggestions for the CategoryTheory/Enriched directory structure?

Ah, I have already merged #20903, but if a better option is found, we may proceed otherwise...

[Emily Riehl]

Ah, great, somehow I missed this. Glad to hear everyone else is ahead of me ;)

[Emily Riehl]

Two more organizational questions:

• at some point there is a namespace isConicalLimit. Should this be IsConicalLimit? Are all namespaces in UpperCamelCase?
• At the end of the Limits file (which I think should be renamed ConicalLimits) there are some special cases involving specific diagram shapes: terminal objects, products, and pullbacks. Should these be broken out into their own files? Should the HasConicalTerminal get added to the IsConicalTerminal file?

[Emily Riehl]

Finally, for the eventual PR to mathlib, how much should @Jon Eugster PR at a time?

[Jon Eugster]

Emily Riehl said:

Two more organizational questions:

• At the end of the Limits file (which I think should be renamed ConicalLimits) there are some special cases involving specific diagram shapes: terminal objects, products, and pullbacks. Should these be broken out into their own files? Should the HasConicalTerminal get added to the IsConicalTerminal file?

Dagur suggested to try mirroring the existing Limit-API as much as possible, therefore I figured this file would be split at least into Mathlib/CategoryTheory/Enriched/Ordinary/Limits/IsConicalLimit.lean and Mathlib/CategoryTheory/Enriched/Ordinary/Limits/HasConicalLimit.lean. I thought of putting them into this Enriched.Ordinal folder because it all assume EnrichedOrdinaryCategory. And I would look at mathlib to figure out how to split-up files around this specific diagram shapes and conical-terminal, too. Does that sound good?

[Jon Eugster]

Emily Riehl said:

• at some point there is a namespace isConicalLimit. Should this be IsConicalLimit? Are all namespaces in UpperCamelCase?

I thought namespaces ought to match the definition/structure's name they are about, so they might be lower-case. (sections are probably only upper-case, but not sure.) Although, I don't think it matters if the statements don't have that definition as explicit argument, because dot-notation won't be a thing anyways.

[Jon Eugster]

or would CategoryTheory/Enriched/Limits be a better place?

[Dagur Asgeirsson]

Emily Riehl said:

Finally, for the eventual PR to mathlib, how much should Jon Eugster PR at a time?

I would start by opening a PR with all the material. Then it's often natural to split it into several PRs, perhaps one per new file added

[Dagur Asgeirsson]

The declaration is called IsConicalLimit (upper camel case because it's a type), so the namespace should be called that as well. (but there is nothing wrong with namespaces in lower camel case)

[Dagur Asgeirsson]

Regarding files for the specific shapes, there is nothing wrong with one file for each shape. These will initially be very small files, but in the future we might want to develop more API for some of these shapes. I would suggest creating a Limits folder inside Enriched (or maybe inside Enriched/Ordinary). Initially, we maybe don't need much of a folder structure inside the Enriched/Limits folder, but that can always be changed later, e.g. if we end up with lots of files for specific shapes, we might create a Shapes folder, etc.

[Jon Eugster]

Dagur Asgeirsson said:

The declaration is called IsConicalLimit (upper camel case because it's a type), so the namespace should be called that as well. (but there is nothing wrong with namespaces in lower camel case)

ah, I thought @Emily Riehl's question was about the namespace conicalLimit which belongs to the def conicalLimit above it and therefore would be lower case.

namespace IsConicalLimit has always been upper case as you explained correctly :+1:

[Dagur Asgeirsson]

Right, they are both correct (analogous to IsLimit and limit)

[Kevin Buzzard]

What is the use of a lower case namespace? Probably means that you can never use dot notation, and somehow isn't that the point of namespaces?

[Dagur Asgeirsson]

Dot notation isn't the only point of namespaces, it's also a way of shortening names by opening the relevant namespace

[Nick Ward]

I will place a vote for putting things in Enriched/Limits if we can get away with it. Mathlib.CategoryTheory.Enriched.Ordinary.Limits.Foo starts to feel a bit long in my opinion.

[Jon Eugster]

Nick Ward said:

I will place a vote for putting things in Enriched/Limits

sounds reasonable. I looked at the other files in Mathlib/CategoryTheory/Enriched and basically all of them use EnrichedOrdinaryCategory somewhere (if not exclusively).

[Jon Eugster]

There's no an entire PR series cummulating in: #20967

One missing point are references. @Dagur Asgeirsson did you have anything particularly when you wrote this for simplicial sets?

[Dagur Asgeirsson]

Great! I think I was just using the infinity-cosmos blueprint

[Nick Ward]

This is quite a well-organized stack of PRs. One for each :octopus: arm!

[Emily Riehl]

The standard reference is Kelly's book with conical limits appearing in section 3.8.

[Nick Ward]

@Jon Eugster can you help me understand what -- see Note [lower instance priority] refers to? It seems this is a standard way to reference things in mathlib, but I do not know where to find such a note.

[Jon Eugster]

Nick Ward said:

Jon Eugster can you help me understand what -- see Note [lower instance priority] refers to? It seems this is a standard way to reference things in mathlib, but I do not know where to find such a note.

it's here. I believe these library notes ought to link but as far as I know nobody ever reimplemented that feature.

[Nick Ward]

Thank you! Apologies by the way if my limited PR comments have found their way to the wrong PRs in the series.

[Jon Eugster]

ah no worries, I'll have a look tomorrow and apply any suggestions to the correct PR. thanks for looking at them

[Emily Riehl]

@Jon Eugster what would you like us to do with the InfinityCosmos version of this PR? We could either (i) merge it now or (ii) let it be.

I don't want to add to your workflow; the mathlib PR is the main thing. So if (ii) is easiest that's fine.

But on the other hand, you've updated the InfinityCosmos/Basic and InfinityCosmos/Isofibrations files in a way I'd like to start using.

[Jon Eugster]

Emily Riehl said:

Jon Eugster what would you like us to do with the InfinityCosmos version of this PR? We could either (i) merge it now or (ii) let it be.

I'd be happy if you merge this now.

[Emily Riehl]

Merged! I didn't delete your branch, though, in case you still want it for some reason. But if not, please feel free to delete this yourself.

Thanks for all your work on this. Please feel free to @ me at any time if I can be helpful with the Mathlib PRs.