Typeclasses on categories, syntax issues

Stream: new members

[Saul Glasman]

Hi,

I'm trying to build up the definition of a model category via some weaker structures, but trying to compose typeclasses here I'm hitting a syntax error I don't understand, and I suspect I've made an elementary mistake. My file is:

import category_theory.fully_faithful
universes u v

open category_theory

namespace category_theory.model

variables (C: Type u) [category.{v} C]

class subcategory (D: Type u) [category.{v} D] :=
(inc: D ⥤ C)
(inc_faithful: faithful inc)

class relative_category (D: Type u) [category.{v} D] extends (subcategory D) :=
(inc_wide: function.surjective inc.obj)

end category_theory.model

But lean doesn't seem to like extends (subcategory D) - I get the error

type expected at
  subcategory D
term has type
  Π (D : Type u) [_inst_2 : category D], Type (max u v)

What do I have wrong here? I should probably ask this too: what's the "Π" that I often see appearing in type expressions?

[Kevin Buzzard]

If you hover over subcategory you'll see it has type Π (C : Type u) [_inst_1 : category C] (D : Type u) [_inst_2 : category D], Type (max u v). Pi is just "for all", if you like. subcategory is expecting four inputs here, namely C, the structure of a category on C, and then D and the structure of a category on D. Two are in square brackets, meaning that those inputs will be supplied by Lean's type class system. But the other two are in round brackets which means that the user is expected to supply them. In particular subcategory D is still a function -- it's expecting another input. You probably want subcategory C D, although looking at other subthings like subring it seems that you might want to take a different approach and make D a field of the class rather than an input (I am not very good with classes, all I know is that there are lots of pitfalls).

[Kevin Buzzard]

What's going on with the Pi is that Lean has something called "dependent functions", which are functions from a type X to...well, the type of the output depends on the term being input! Here's an example very familiar to mathematicians. If we have infinitely many true-false statements $P(0)$, $P(1)$, $P(2)\ldots$ and we want to construct proofs of them all, then we need a function which takes as input a natural $n$ and spits out a proof of $P(n)$. If you think about it, this is slightly weirder than a function, because in Lean $P(n)$ is a type, and a proof of $P(n)$ is a term of that type, so the proof function takes as input $n$ and spits out a term whose type depends on $n$, so it's difficult to imagine it as a traditional function from the naturals to some fixed type -- there is no "type of all proofs of all propositions" for the same sort of reason that there's no set of all sets. The function $P$ itself (the statements of the theorems) is just a regular function from $\mathbb{N}$ to Prop, but the proof function is not a function in a traditional sense, it's a term of the Pi type Π (n : nat), P n, or, as a mathematician would usually write, a proof of $\forall n\in\mathbb{N}, P(n)$.

[Kevin Buzzard]

Theorem Proving In Lean provides a more computer-science-focussed explanation of Pi types in section 2.8.

[Adam Topaz]

Everything Kevin said is of course important, but another way to look at this in this particular case is that, a priori, D has nothing to do with C, so you need to tell lean explicitly that D is a subcategory of C, i.e. you would have to write subcategory C D. The actual reason, coming from lean syntax, is that you wrote variables (C: Type u) [category.{v} C], and C appears in the definition of subcategory, so lean automatically makes C an explicit variable in the declaration of subcategory.

[Kevin Buzzard]

I also realise that I probably can make a type of all proofs of all propositions -- it's Π (P : Prop), P :-)

[Adam Topaz]

That's a good empty type :)

[Kevin Buzzard]

oh yeah, it seems to say that every proposition is true :-)

[Adam Topaz]

BTW, I think this is one instance where it makes sense to define a subcategory as a category with a faithful functor, as opposed to, say, something analogous to bundled subrings (which are defined as a subset of the ring with some conditions), essentially due to the equivalence principle in category theory ( https://ncatlab.org/nlab/show/principle+of+equivalence )

[Kevin Buzzard]

and Lean doesn't buy Σ (P : Prop), P

[Adam Topaz]

Oh, and one more comment, since faithful is a class, it makes sense to define subcategory using the following syntax:

class subcategory (D: Type u) [category.{v} D] :=
(inc: D ⥤ C)
[faithful inc]

This way lean would go and try to find a faithful instance for inc using typeclass search, instead of requiring the user to manually tell lean what the instance is.

[Adam Topaz]

This works:

def foo := Σ (P : Prop), (plift P)

[Kevin Buzzard]

This doesn't: example : Σ (P : Prop), plift P := ⟨true, trivial⟩

[Kevin Buzzard]

got it -- example : Σ (P : Prop), plift P := ⟨true, plift.up trivial⟩

[Adam Topaz]

Yeah. it's the plift thing

[Adam Topaz]

Saul is a homotopy theorist, so you can just tell him that a dependent function is a section of a fibration :)

[Reid Barton]

Since weak equivalences form a wide subcategory, and the basic operation is asking whether a morphism of the ambient category is a weak equivalence, I think it's better not to use this equivalence-invariant approach and just use some variation on \Pi {X Y : C} (f : X --> Y), Prop.

[Reid Barton]

@Saul Glasman You should take a look at https://github.com/rwbarton/lean-homotopy-theory and https://github.com/rwbarton/lean-model-categories/tree/top-dev (note: this one is a non-master branch).

[Adam Topaz]

Oh right, this is for defining a model structure. There is also docs#category_theory.arrow which you can use instead of the Pi type that Reid mentioned

[Adam Topaz]

I.e. you can use set (arrow C)

[Reid Barton]

I think I also started with a similar approach using extends but a problem is that as soon as you add a second class of morphisms (like cofibrations) you need a way to distinguish whether you're talking about the weak equivalences subcategory or the cofibrations subcategory.

[Reid Barton]

I think using arrow will get awkward pretty quickly because Lean is bad at unification problems like "what's a : arrow C with a.hom = f".

[Reid Barton]

It's more practical to just make all the objects involved into implicit arguments--I edited my original message to reflect this.

[Adam Topaz]

Sometimes (like in this case) I wish categories were defined as categories internal to types, where the type of all arrows is a first class citizen like the type of objects.

[Reid Barton]

The downside is that it's not as convenient to take the intersection of two wide subcategories, but (a) that's not something that happens very often, (b) even if you get to reuse the intersection of sets, you still need to prove it is closed under composition, say, so there's more work that needs to happen anyways

[Saul Glasman]

Thanks everyone!

[Saul Glasman]

Reid, I didn't know that you had worked on model categories - I'll take a look at your approach

[Saul Glasman]

I think I still don't know how to read Π (D : Type u) [_inst_2 : category D], Type (max u v), which is supposed to be the type of subcategory D. Does it mean "for each type D and (implicit) category structure on D, a type"? Shouldn't D be fixed here?

[Reid Barton]

I can translate your Lean code back into math:
Let $C$ be a category.
Definition. A $C$-subcategory structure on a category $D$ consists of a faithful functor $i : D \to C$.
Definition. A relative category is a category $D$ equipped with a $D$-subcategory structure such that $i$ is surjective on objects.

[Reid Barton]

You'll note that something is missing in the second definition: a $D$-subcategory structure on what?

[Reid Barton]

The error is saying that subcategory D expected more arguments, this missing other category (which, as a result of the chosen variable names, Lean is also calling D).

[Saul Glasman]

So there are actually two different Ds?

[Kevin Buzzard]

Reid is just saying that in the definition of relative category which you posted, no C is mentioned, so there must be something wrong.

[Adam Topaz]

If you want to go with the faithful functor route without having to specify both Cand D you could do something like this:

structure subcategory :=
(D : Type*)
[I : category D]
(inc: D ⥤ C)
[J : faithful inc]

[Reid Barton]

I realize now my English translation is ambiguous in the phrase "a category $D$ equipped with a $D$-subcategory structure" which could be interpreted as "a category $D$ equipped with a $D$-subcategory structure on $D$".

[Reid Barton]

But, that's not the right notion anyways. There needs to be a second category at some point, which is going to play the role of the subcategory of weak equivalences.

[Saul Glasman]

@Reid Barton , I did one of the "todo"s in your model categories repo as an exercise (retracts of weak equivalences in a model category are weak equivalences) - wonder if you would be willing to accept a PR/give feedback?

[Reid Barton]

Hi @Saul Glasman, very cool! As you probably noticed, the model categories repository has been dormant for a long time, but please do submit a PR!

[Reid Barton]

At this point the model category repository is so old that, moving forward, it would probably be better to start from scratch.

[Saul Glasman]

Done! https://github.com/rwbarton/lean-model-categories/pull/1/files

[Saul Glasman]

Reid Barton said:

At this point the model category repository is so old that, moving forward, it would probably be better to start from scratch.

Yeah, I noticed that if I updated the mathlib dependency to current in the model categories repo, things failed fairly dramatically...