equality of cones

Stream: mathlib4

[Nicolas Rolland]

In the library, we have

/--
Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
-/
@[simps]
def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G where
  obj c :=
    { pt := c.pt
      π := c.π ≫ α }
  map f := { hom := f.hom }

/-- Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as
postcomposing by `α` and then by `β`. -/
@[simps!]
def postcomposeComp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
    postcompose (α ≫ β) ≅ postcompose α ⋙ postcompose β :=
  NatIso.ofComponents fun s => Cones.ext (Iso.refl _)

Is there a reason why postcomposeComp is not giving an equality ?

In the same vein, there are no real extensionality lemma on Cone, only some up-to-iso

def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt)
    (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j := by aesop_cat) : c ≅ c' where

Is this just missing, probably because dealing with HEq or eqToHom is a pain, or is it a design choice ?

[Eric Wieser]

I'm pretty sure avoiding equality in category theory is often a deliberate design choice

[Adam Topaz]

The philosophical/mathematical reason is that equality of objects is “evil” (i.e. not preserved by equivalence of cats). The practical reason is that non-definitional equality of objects is very likely to prevent a lot of the category theory automation from working well.

[Nicolas Rolland]

In that case it seems equal by associativity of composition of natural transformations.

if that’s « evil », what isn’t … ?

[Adam Topaz]

But the natural transformation is part of the object!

[Joël Riou]

Nicolas Rolland said:

In that case it seems equal by associativity of composition of natural transformations.

if that’s « evil », what isn’t … ?

Definitional equalities are certainly not evil, but the associativity of the composition of morphisms in categories is not a definitional equality. (One of the problems with equalities of objects/functors is that most of the time it is not very practical to use them, while the isomorphisms API is usually convenient enough.)

[Nicolas Rolland]

I see the argument about usability.

Evilness is much less clear to me...

As far as I remember it meant that giving a central role to a notion which is not equivalence-invariant is foolish. Of course definitional equality is not concerned about this.

Have you a link about what is the real argument about evilness ?

[Kevin Buzzard]

Equality in a category is "evil" in the same sense that asking about what the elements of the elements of a group are -- that latter question is not invariant under isomorphism, which is the fundamental way that groups can be "mathematically the same". Hence asking about elements of elements of groups is not a mathematical question. In category theory the fundamental way that categories are the same is equivalence of categories, and equality of objects is not respected by this equivalence relation, so in some sense it's also not a mathematical question.

[Nicolas Rolland]

I understand that we shouldn’t be interested about a general statement which is not invariant by equivalence. It would mean the statement is too particular and not about category theory.

But if I am building a categorie, I can talk about objects being the same. I can equality talk about two categories being the same. If I build a functor to Cat, I have to rely prove functor equality which seems even worse (?)

Equality of objects is probably evil to rely on, but I fail to see how it’s bad to assert it while building things…

[Adam Topaz]

The point is that it’s not invariant under equivalence of categories.

[Adam Topaz]

For example the statement “this category has 37 objects” is evil because, again, that’s not invariant under equivalences.

[Nicolas Rolland]

In a statement postcompose (α ≫ β) = postcompose α ⋙ postcompose β what is not invariant under equivalence of categories ?

Not trying to nitpick, I genuinely do not understand what this is all about.

As for “this category has 37 objects” exemple, it is nonetheless very useful to talk about "the" terminal category, with 1 object and a single morphism (and make good use of those facts !). Is this "evil" too ?

[Jakob von Raumer]

This is the way I see it: As it's a main princple of category theory to talk about objects only up to (sometimes unique) isomorphism, it's good practice to "forget" about all properties of a construction which do not obey this principle as soon as possible. The "API" of postcompose consists entirely of the iso that you cited and of its behaviour on the identity NatTrans. That's all you need to use and talk about postcompose.

[Joël Riou]

Nicolas Rolland said:

As for “this category has 37 objects” exemple, it is nonetheless very useful to talk about "the" terminal category, with 1 object and a single morphism (and make good use of those facts !). Is this "evil" too ?

In general, the terminal object is not unique, it is only unique up to a (unique) isomorphism. We have such a suitable API for initial/terminal objects.

[Nicolas Rolland]

Joël Riou said:

Nicolas Rolland said:

As for “this category has 37 objects” exemple, it is nonetheless very useful to talk about "the" terminal category, with 1 object and a single morphism (and make good use of those facts !). Is this "evil" too ?

In general, the terminal object is not unique, it is only unique up to a (unique) isomorphism. We have such a suitable API for initial/terminal objects.

As any object « defined » by UP vs constructed uniquely.

But is it evil to claim any of those have one object and one morphism ?

[Kevin Buzzard]

(deleted)

[Nicolas Rolland]

Jakob von Raumer said:

This is the way I see it: As it's a main princple of category theory to talk about objects only up to (sometimes unique) isomorphism, it's good practice to "forget" about all properties of a construction which do not obey this principle as soon as possible. The "API" of postcompose consists entirely of the iso that you cited and of its behaviour on the identity NatTrans. That's all you need to use and talk about postcompose.

So what you say is that it is true that postcompose (α ≫ β) = postcompose α ⋙ postcompose β but we should not use it ?

[Nicolas Rolland]

Kevin Buzzard said:

It's not true that there is one terminal object. For example in the category of sets, any set with one element is a terminal object and there are uncountably many of these. So it's worse than evil, it's just wrong.

That’s not the discussion here.

The purported evil property is that they have one element.

[Kevin Buzzard]

Right, you should use EqToHom, because that's not evil. Re the set comment: yes, sorry, I misunderstood the question.

[Nicolas Rolland]

I don’t see how postcompose (α ≫ β) = postcompose α ⋙ postcompose β is evil

[Kevin Buzzard]

It's evil in a technical sense which I think you do understand, you just don't think it's relevant.

[Kevin Buzzard]

There used to be a page in nLab discussing evil arguments in category theory but it seems to have been removed (and right now I'm behind the great firewall so it's difficult to search)

[Nicolas Rolland]

No, I genuinely have no idea in what « technical » sense this is wrong. In my book it is true.

[Kevin Buzzard]

"evil" is being used in a technical sense here. If you are lucky enough to be able to search the internet right now, see if you can find anything on evil arguments in category theory. Sorry, I'm a bit limited in what I can do right now.

[Kevin Buzzard]

The point is that when you are making a mathematical theory you have to write down your definitions, so you have to say what things mean. If you build mathematics from set theory there is an axiom telling you what it means for two sets to be equal -- they're equal iff they have the same elements. In category theory there is no such axiom or definition, the concept that two objects of a category are equal is not defined within category theory, and for good reason: it's not equivalence-invariant (i.e. it's not true that if e : C -> D is an equivalence then c1=c2 iff e(c1)=e(c2)). However if you do category theory within Lean then the objects of a category do have an equality defined on them, and that's because Lean defines equality of terms of a fixed type via an inductive definition, and objects of a category are defined to be terms of a fixed type in Lean's model of the theory, so the definition applies. Hence because of choices coming from the model, rather than the theory itself, you can talk about equality of objects in a category within Lean. But this is a consequence of the way the theory has been set up, and you shouldn't necessarily expect equality to behave well, because there are no axioms or theorems involving equality of objects in category theory. There is however Eq.rec in Lean (aka the rw tactic), so that's a way which you can use equality in Lean's model of category theory. But the correct concept of equality in category theory is isomorphism, which is data (it involves a choice of isomorphism, and in Lean you have to make this choice even if there is only one -- moving from the Prop universe to the Type universe is Lean's version of the axiom of choice), and to manipulate objects in category theory using the axioms of category theory you're going to need that data. EqToHom is what provides the data. Sure you can work with equality, but once you get going you'll need to know the API for category theory in mathlib and this is designed with isomorphisms, not equalities.

[Nicolas Rolland]

All the valid points you make about equality are at play here

def assocOK : ∀ {F G H I : J ⥤ M} (α : F ⟶ G) (β : G ⟶ H) ( γ : H ⟶ I),
    (α  ≫ β ) ≫ γ = α ≫ β ≫ γ  := by aesop

Aka, we already have that the post-composing by a composite is equal to postcomposing by each component, with the caveat you mentioned that we defer to something outside of category to talk about equality.

If we now consider cones, which are simply natural transformation from a constant functor and package them up in a category, I don't see why this would become « evil » in any technical sense.

def assocEVIL : ∀ { G H I : J ⥤ M} (pt : M) (cone : (const J).obj pt ⟶ G) (β : G ⟶ H) (γ : H ⟶ I),
    (cone  ≫ β ) ≫ γ = cone ≫ β ≫ γ  := by aesop

Category theory is only a useful way to package things which exists independently of it.  I don’t really see why there should be any loss or penalty for the simple fact of packaging established things up in a category.  We had equality, why give it up ?

That equality is not defined within category theory, but it is defined outside, is ok. As you say, in Set it will be something. In another category it will have some other meaning. We defer to the particular category at play to say what it actually means. Just like morphisms equality is not defined within category theory, but it is defined, "outside" of category theory, for each category, and we have to prove that it holds to craft a category.

Here, specifically, we have two functors, and we want them to be equal. Equality of functors is defined by the fact that it transports an object to same object in the target category, and a morphism to the same morphism in the target category. 

Aka what « same » means for each image is deferred to the target category of the functors. 

Here the target category is the category of cones of a functor H. In that category, it means we have the same tip and the same legs. So those equalities are in terms of the target category of H. The tips here are definitionally equal. The legs are almost definitionally equal, we need associativity of composition of natural transformations, which come from the axiom of associativity in the target category. What is evil here ?

The argument that equivalence is a better API for some (most ?) purposes is understandable.
Especially since that there are few functors to Cat in Mathlib currently (but is it discouraged ?)

As for the « evilness » one, I just do not see what it could possibly mean here in that particular case.

[Adam Topaz]

docs#CategoryTheory.Limits.Cones.postcompose is a functor from the category of cones to another category of cones. If you postcompose with $a \gg b$ that's equal to first postcomposing with $a$ then postcomposing with $b$, yes. But, if you happen to replace (at least one of) the category of cones with an equivalent category, you could end up in a situation where an equality will not hold true on the nose. That's what I meant when I said above that this equality is not preserved under equivalence.

[Adam Topaz]

Now the subtle part is that if $F : C \to D$ is a functor and you consider the category of cones over $F$, replacing either $C$ or $D$ (and/or doing something analogous for the source and target of $G$) by equivalent categories will induce equivalences on the category of cones, where the equality in question is (I think) preserved. But these are very special equivalences on the category of cones!

[Adam Topaz]

In your code snippet you identified a cone with the underlying natural transformation, but natural transformations don’t have the category structure that cones do, so this is somewhat misleading

[Nicolas Rolland]

Adam Topaz said:

In your code snippet you identified a cone with the underlying natural transformation, but natural transformations don’t have the category structure that cones do, so this is somewhat misleading

As I understand the "evilness" argument, it would also apply to the discrete category whose objects are those natural transformations. so I don't think it is misleading.

It's hard to see why christening some things under a label "category" would entail loosing some knowledge. Category theory is just a vocabulary :

If I refer to natural transformations from a constant functor as such, or as an objects of a discrete category of natural transformations from a constant functor, that should not change (at least in theory, the implementation can differ) what I can say about them.

[Yuma Mizuno]

Labelings are important and suggest to Lean and implementers how to treat expressions. For example, the discrete category label (technically Discrete type synonym) suggests that we should not think about equality between objects, although we can. This is not enforced by the system, but is more like a design pattern.

The general best practice here is not to think about equality between types. Objects of categories are intended to be used to provide types for morphisms.

[Nicolas Rolland]

I can imagine that it is a best practice (or a Lean limitation ?)

But this can bite when abstracting to write functors into Cat, like here.

I dispute the argument that it is about "evilness" or category theory related ideas : there should be, in principle, no restriction on what can be said about some items resulting from the mere fact of organizing them in a category.

Of course practice and limitation of the system is another matter.

[Kevin Buzzard]

Yeah people do do evil things with categories in Lean because you can't remove =, you can just point out that it might not be the best idea in some situations. I'm seeing people using = when developing the theory of stacks in Lean and you see it in the literature as well.

[Joël Riou]

Nicolas Rolland said:

I can imagine that it is a best practice (or a Lean limitation ?)

But this can bite when abstracting to write functors into Cat, like here.

The recommended practice (especially for mathlib contributions) is to avoid using equality of objects/functors when it is not necessary, and use isomorphisms if it is possible (sometimes, it may require expanding the existing API). If you formalise significant results/constructions which very much need equality of objects, I am quite sure that mathlib maintainers would be happy with these additions. We would probably be much more reluctant in case of a PR which would only add lemmas that some of us consider "evil".

[Nicolas Rolland]

This seems to be a problem for categorical abstraction and modular programming.
Functors to Cat, for instance, are extremely useful for categorical reasoning.
Take the covariant embedding \phi_ of Cat into Dist, the bicategory of distributors.
It is a classical result that this embedding is full and faithful (Yoneda lemma really) by basic UP reasoning

$Nat~ F~ G ∈ ∫_a B(Fa,Ga) ≅ ∫_a [B^{op},Set](B(-,Fa),B(-,Ga)) ∋ Nat (\phi_F) (\phi_G)$

The middle ≅ holds because two iso functors are mapped to two iso category of Ends (whose object are terminal wedges) because there is a functor to Cat.

If I understand correctly, this simple categorical reasoning won't fly in Lean, because

theorem wedgeHom_comp {F G H : (Bᵒᵖ×B) ⥤ M} (α : F ⟶ G) (β : G ⟶ H) : wedgeHom α ⋙ wedgeHom β
  =  wedgeHom (α ≫ β) := sorry_evil

prevents from having such functor. So some specialized version has to be used

def isoFctrIsoWedgeInType {F G : (Bᵒᵖ×B) ⥤ M} (i: F ≅ G) : Wedge F ≅ Wedge G  where ...

It works, but the net loss in abstraction and modularity is obvious.

Apart from that :

1- It is extremely bothering that one can say something about some mathematical entities, which we can not say when considering the same entities as objects of a category. This is a high price to pay and a strong negative advertisement to usage of category theory.

2- In theory I still don't see how some of us can consider this evil...
I think there is some confusion as to what the purpose and scope of this "evil" notion is precisely.
Could this be "Evil evilness" ?

[Adam Topaz]

You can say whatever you want (assuming that it type checks, of course). But the practical implications of saying “evil” things is that automation from the category theory library is much more likely to fail.

[Jakob von Raumer]

Do we consider the current state of #16971 as :angry_devil: or :angel:? Not sure anyone cares that whiskering induces a strict endofunctor on Cat instead of a pseudofunctor.

[Adam Topaz]

The stuff in that PR seems fine to me since everything is proved with rfl. That means that it (probably) won't lead to DTT hell.

[Yuma Mizuno]

Jakob von Raumer said:

Do we consider the current state of #16971 as :angry_devil: or :angel:? Not sure anyone cares that whiskering induces a strict endofunctor on Cat instead of a pseudofunctor.

The rfl in

@[simp]
theorem whiskeringLeft_obj_id : (whiskeringLeft C C E).obj (𝟭 _) = 𝟭 _ :=
  rfl

depends on the following defeq:

𝟭 C ⋙ G =?= G

CategoryTheory.whiskerLeft (𝟭 C) α =?= α

I think the lemma itself is fine, but this should not be a simp lemma, at least unless it is really necessary, in the same philosophy as the comment at docs#CategoryTheory.Functor.comp_id.

The evilness of the rfl case is less than that of the non-rfl case, but there is still a possibility that it could be a problematic at simp or isDefEq performance in the future.

[Nicolas Rolland]

Yuma Mizuno said:

The evilness of the rfl case is less than that of the non-rfl case

Can you (or anyone...) clarify what you mean precisely by that ?
Is the evilness, in your sense of the word, of rfl an idea coming from category theory, or some best practice ?
Can it be rephrased as you considering "f" and "f >> id" as not equal, or evilly so, just because they are referred to as objects ?

I fail to see what goal is pursued, or what problem is solved, by considering pre/post-composition not as a strict endofunctor.
This seems very close to the associativity I had (no) issue with.

[Yuma Mizuno]

Since the defeq (equallity can be proved by `rfl) is almost the "identification", it's usually fine to put an equality. Sometimes we need to recall that the defeq is actually not a true identification, and depends on how Lean or tactics handle expressions.

The simp setting might be more controversial, and my intention was mostly a compatibility with the existing setting in the library.

[Adam Topaz]

Thanks to @Yuma Mizuno 's reminder about Functor.comp_id, I do agree that the Lemma from the PR should not be tagged with simp.

[Yuma Mizuno]

I noticed that Functor.comp_id and Functor.id_comp could not be proven with rfl in Lean 3, but they can be proven with rfl now. There may be a remnant of this in the current situation of these equalities.

[Yuma Mizuno]

The related remark is that the Functor.assoc could be proved in rfl even in lean 3, but Functor.associator was preferred in many situations.

[Nicolas Rolland]

Yuma Mizuno said:

Since the defeq (equallity can be proved by `rfl) is almost the "identification", it's usually fine to put an equality. Sometimes we need to recall that the defeq is actually not a true identification, and depends on how Lean or tactics handle expressions.

So, just to clarify, that has nothing to do with category theory. It pertains to Lean and its use.
Notably, we rely on some normal form to identify expressions via defeq.

It would be helpful to have another, more descriptive name for this kind of "evilness", distinct from the categorical one, (which is already confusing enough...), if this has an impact on any aspect .

[Jakob von Raumer]

Thanks for your input, @Yuma Mizuno ! Will remove the simps