Inclusion functor from a fullsubcategory is a Mono

Stream: Is there code for X?

[Yiming Xu]

I would like to use the cancellation property of the inclusion functor to prove equalities of functors that go into a full subcategory. Surprisingly, I do not find any theorem in
Mathlib.CategoryTheory.FullSubcategory saying that the inclusion functor defined as:

def fullSubcategoryInclusion : FullSubcategory Z ⥤ C :=
  inducedFunctor FullSubcategory.obj

is a mono.

May I please ask if it is proven to be a mono somewhere?

[Yiming Xu]

I am aware that despite the absense of "Mono", there is something called "FullyFaithful" in that file. But as my goal is working with strict equality instead of equivalence, it seems not to be what I want because all I can get from Mathlib.CategoryTheory.Functor.FullyFaithful seems to be equivalence.

[Yiming Xu]

I am not yet familiar enough with this library so maybe I am wrong with this (in which case thanks for correcting me!) But I aim to find an approach to use the fact that the inclusion functor from a full subcategory is a mono to prove strict equalities between functors to a full subcategory. Are there any devices that I could try?

[Markus Himmel]

I believe that docs#CategoryTheory.fullyFaithfulFullSubcategoryInclusion and docs#CategoryTheory.Functor.fullyFaithfulCancelRight is the best that mathlib has to offer here. Mathlib doesn't really develop equality of functors, because it's almost never a good idea to work with equality of functors unless the equality is definitional. Equality of functors (or, more fundamentally, equality of objects in a category) quicky leads to problems in practice because of what is commonly known as "DTT hell".

[Yiming Xu]

Thanks for the swift response!! I am searching for that precisely because I want to obtain equations between functors without the DTT hell, so I am trying to detour this. If I cannot do that, is there any hope that this equivalence is already connected to some theorems with eqToHom?

[Markus Himmel]

I think it would be easier to point you toward useful tools in mathlib if you shared a bit more code that shows what you're trying to achieve.

[Yiming Xu]

Sure. Thank you! I will try to write in more detail what I am trying to do later today.

[Yiming Xu]

basically I am working on (this project)[https://github.com/sinhp/groupoid_model_in_lean4] which has 2-category stuff.

[Yiming Xu]

It would take quite a while to phrase the original question. So I am sketching the outline of the problem. I wonder if my case is the kind of stuff that witnesses the necessity of the "almost" in "almost never a good idea"... Please retort if someone has something to say.

I have two ambient categories A1 and A2, and I have full subcategories S1 and S2 siting in A1 and A2, via inclusions $i_1:S_1\to A_1$, $i_2:S_2\to A_2$, respectively. I have two functors $F_1,F_2:S_1\Rightarrow S_2$. My aim is to prove $F_1= F_2$.

There is something called Functor.ext, but I do not want to use it. I hope the following works:

I prove $e_1:i_2\circ F_1 = F:A_1\Rightarrow A_2$ and $e_2:i_2\circ F_2 = F:A_1\Rightarrow A_2$ for some $F:A_1\Rightarrow A_2$. (Specifically, the $F_1$ here I have is defined using CategoryTheory.FullSubcategory.lift, and $F_2$ is a simpler description of it. $F_1$ is just $F$ for the domain and codomain restricted to full subcategories.)

So I will have $i_2\circ F_1 = :i_2\circ F_2$. If $i_2$ is monic, I can cancel the $i_2$ to obtain $F_1 = F_2$, which I want.

[Yiming Xu]

To clarify, the picture looks like this:

[Yiming Xu]

37d9da1a-cb6c-4262-9081-c3d05e712ce7.jpg

[Yiming Xu]

In the (very sad) case that mathlib really do not want me to do that, I would still prefer to prove something about functor being monic, and how is this connected to eqToHom, instead of calling Funtor.ext here. So please suggest something if there are some hints on this direction!

[Kevin Buzzard]

Why would you want to prove that two functors are equal though? This is an evil statement because it relies on the concept of equality of objects in a category, which is not preserved under equivalence of categories. Why don't you just write down a morphism between the functors and prove it's a natural isomorphism?

[Yiming Xu]

If I ask "Why should we insist using natural isos instead of equalities", I (naively) guess that the structuralisms would say "because that is enough, categorical reasoning should not rely on equality". But in practice, we are dealing with lots of strict pullbacks, I guess they are too many of them, and the natural isomorphims are not an interesting piece of information to keep record of along the proof. So, in my turn, I would ask "if we can get a neat equation between functors to easily get things type checked, since it is doable in Lean, why should we still insist on using isos everywhere just because the philosophy?" I am not claim that natural isos are impossible, but just my two cents, it is not clear that it deserves all the additional work. And as a user, I prefer to read thms with equalities, rather than have to pass through the isos explicitly even when reading a simple statement.

[Yiming Xu]

Disclaimer: I respect those who takes that piece of philosophy as belief and develop elegant proofs that avoid equalities once possible. But I disagree that pursing the convenience of equality between objects when working with a functor category id undesirable.

[Kevin Buzzard]

Equality in Lean's type theory is a very complicated thing. For example $\N=\Z$ is an undecidable statement in Lean -- it can neither be proved nor disproved, and indeed there are models of Lean's type theory in which it's true, and models in which it's false. So if you want to stick with equality of functors (and hence equality of objects), be warned. It might be possible to get it working and if so, then great! But maybe what is really needed here is better tooling to deal with natural isomorphisms.

[Yiming Xu]

Thanks for the warning, makes sense! I would be excited if a well-developed flow of working with natural isomorphism appears one day. I think for "working with equalities vs isos", the answer should be "intensional " rather than "extensional" :-) , i.e., addressing "in which manner" rather than merely "making a choice". Even if we get natural isos to work well, if the isos themselves appear everywhere in every thm and every proof, I am afraid that it would be a pain. I am curious how things go in both of these two directions.

[Joël Riou]

Yiming Xu said:

Disclaimer: I respect those who takes that piece of philosophy as belief and develop elegant proofs that avoid equalities once possible. But I disagree that pursing the convenience of equality between objects when working with a functor category id undesirable.

Experience shows that in most cases, things go much smoother using isomorphisms of functors (+ conditions satisfied by these isomorphisms) instead of equalities of functors. There are a few situations where we do need to use equalities of functors. For example, when studying the nerve of a category, when we say that two n-simplices are equal, we actually mean that two functors are equal (and for this, we have some lemmas like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/ComposableArrows.html#CategoryTheory.ComposableArrows.ext%E2%82%85)
In the context of the localization of categories, there is a certain universal property (in the category of categories) which requires using equalities of functors https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Predicate.lean#L68-L79 (see the fac and uniq fields) but it is used only in the internals of the API in order to prove safer statements involving isomorphisms rather than equalities. Otherwise, equalities of functors are kind of ok in the conclusion of lemmas when they are definitional equalities.
I can understand you would like to state equalities of functors, but I feel it is absurd to be reluctant to use the most appropriate lemma to do so, which is Functor.ext...

[Robin Carlier]

Joël Riou said:

In the context of the localization of categories, there is a certain universal property (in the category of categories) which requires using equalities of functors https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Predicate.lean#L68-L79 (see the fac and uniq fields) but it is used only in the internals of the API in order to prove safer statements involving isomorphisms rather than equalities.

I don’t want to derail the discussion too much here, but is there a particular reason you picked this universal property for localizations, rather than the one you’d have with natural isomorphism everywhere rather than equality (which would be the localization in the (2,1)-categorical sense)? (of course, given the rest of what’s in the file, using Lifting, you get something equivalent, but I’m curious about not making it the definition.)

[Yiming Xu]

Joël Riou said:

Yiming Xu said:

Disclaimer: I respect those who takes that piece of philosophy as belief and develop elegant proofs that avoid equalities once possible. But I disagree that pursing the convenience of equality between objects when working with a functor category id undesirable.

Experience shows that in most cases, things go much smoother using isomorphisms of functors (+ conditions satisfied by these isomorphisms) instead of equalities of functors. There are a few situations where we do need to use equalities of functors. For example, when studying the nerve of a category, when we say that two n-simplices are equal, we actually mean that two functors are equal (and for this, we have some lemmas like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/ComposableArrows.html#CategoryTheory.ComposableArrows.ext%E2%82%85)
In the context of the localization of categories, there is a certain universal property (in the category of categories) which requires using equalities of functors https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Predicate.lean#L68-L79 (see the fac and uniq fields) but it is used only in the internals of the API in order to prove safer statements involving isomorphisms rather than equalities. Otherwise, equalities of functors are kind of ok in the conclusion of lemmas when they are definitional equalities.
I can understand you would like to state equalities of functors, but I feel it is absurd to be reluctant to use the most appropriate lemma to do so, which is Functor.ext...

The core reason is that when we prove there is a functor between functor categories, there are fields of the construction of instance/structure that explicitly ask us to prove equality between functors instead of allowing us to compose with any equivalence. I believe what we meet now is like your case for the 2-cells (or higher cells) between simplices.

What I am attempting to do is to develop some lemmas which minimize the direct usage of Functor.ext. For instance, in the case that the functors to compare are on a subcategory, at least Functor.ext should not be called directly on these two functors. The first step of this attempt is to reduce the problem I outlined into proving:

lemma fullSubcategoryInclusion_Mono {C:Type*} [Category C] (Z: C → Prop) :
Mono (Cat.homOf (fullSubcategoryInclusion Z)) := sorry

May I please ask if you could suggest something obvious to try according to your experience? And, as you said that you find it absurd to use Functor.ext too much, is there anything you may summarize as the first things to try to avoid Functor.ext to get equalities between functors? It would be ideal if we could develop an API addressing the common cases of the usage of Functor.ext. (No worries if not obvious at all! Just in case that you may say something about that.)

[Yiming Xu]

Joël Riou said:

Yiming Xu said:

Disclaimer: I respect those who takes that piece of philosophy as belief and develop elegant proofs that avoid equalities once possible. But I disagree that pursing the convenience of equality between objects when working with a functor category id undesirable.

Experience shows that in most cases, things go much smoother using isomorphisms of functors (+ conditions satisfied by these isomorphisms) instead of equalities of functors. There are a few situations where we do need to use equalities of functors. For example, when studying the nerve of a category, when we say that two n-simplices are equal, we actually mean that two functors are equal (and for this, we have some lemmas like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/ComposableArrows.html#CategoryTheory.ComposableArrows.ext%E2%82%85)
In the context of the localization of categories, there is a certain universal property (in the category of categories) which requires using equalities of functors https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Predicate.lean#L68-L79 (see the fac and uniq fields) but it is used only in the internals of the API in order to prove safer statements involving isomorphisms rather than equalities. Otherwise, equalities of functors are kind of ok in the conclusion of lemmas when they are definitional equalities.
I can understand you would like to state equalities of functors, but I feel it is absurd to be reluctant to use the most appropriate lemma to do so, which is Functor.ext...

Thanks a lot for this elaboration! I will try to devote some time to reading the links.

[Joël Riou]

Robin Carlier said:

I don’t want to derail the discussion too much here, but is there a particular reason you picked this universal property for localizations, rather than the one you’d have with natural isomorphism everywhere rather than equality (which would be the localization in the (2,1)-categorical sense)? (of course, given the rest of what’s in the file, using Lifting, you get something equivalent, but I’m curious about not making it the definition.)

My definition of L.IsLocalization W does not use the strict universal property either, but the property that the functor from the "constructed localization" is an equivalence (then, IsLocalization behaves well with respect to equivalences of categories, not just isomorphisms of categories). I only provide a constructor for IsLocalization which uses StrictUniversalPropertyFixedTarget as an input.
Here are two reasons not to use the relaxed universal property in the definition:

• the "relaxed" universal property which is stated as docs#CategoryTheory.Localization.functorEquivalence has to hold for all universes (and we cannot say "let us fix the universes once for all", because the localization may increase the universe levels), and if it was stated only for a fixed big enough universe, it would not be so easy to develop the API...
• if we were to use that relaxed universal property as the definition of F.IsLocalization W, the proofs of https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Prod.lean#L98-L105
  https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Opposite.lean#L28-L41 and https://github.com/leanprover-community/mathlib4/blob/dad08fa365650bbf2f7aed844722fea2c735069c/Mathlib/CategoryTheory/Localization/Composition.lean#L33-L46 would be more complicated, as the burden of proof would be much more important: the proofs would probably have to include some of the ingredients which appear in the relatively nontrivial proof of docs#CategoryTheory.Localization.Construction.whiskeringLeftEquivalence for the constructed localized category (the key lemma is docs#CategoryTheory.Localization.Construction.morphismProperty_is_top which is about the fully faithfulness of the functor given by the precomposition with the localization functor)

[Steve Awodey]

Kevin Buzzard said:

Why would you want to prove that two functors are equal though? This is an evil statement because it relies on the concept of equality of objects in a category, which is not preserved under equivalence of categories. Why don't you just write down a morphism between the functors and prove it's a natural isomorphism?

I certainly agree that in category theory in general (and in math that's using it), it's better to work up to isomorphism than up to equality! But for this particular project (HoTTLean), we are using categories and functors as algebraic objects, in order to strictly model the rules of dependent type theory, as explained in this paper.

Thanks for any advice you (all) can give on how to make Lean do what we want!

[Joël Riou]

Yiming Xu said:

And, as you said that you find it absurd to use Functor.ext too much

No, what I find absurd is that you insist on proving equalities of functors and at the same time you do not want to use the essentially unique tool we have to do it, which is Functor.ext.
As @Markus Himmel has implied above, if there are any functors I : C ⥤ D which deserve to be the analogues of monomorphisms, these are the functors such the postcomposition with I give fully faithful functors (E ⥤ C) ⥤ (E ⥤ D) for any category E. (Similarly as a monomorphism i : c ⟶ d in a category is a morphism such the postcomposition with i gives an injective map (e ⟶ c) → (e ⟶ d) for any object e.) It turns out that the functors I as above are exactly the fully faithful functors.

[Yiming Xu]

I mean we should make attempt to call Functor.ext in an organized way instead of everywhere. It is a pain to "get into dependent rw once we have chance to encounter it". It should be only called on the most managable defs and thms. The above I wrote is again an abstraction to some particular case which is less managable.

[Joël Riou]

Steve Awodey said:

I certainly agree that in category theory in general (and in math that's using it), it's better to work up to isomorphism than up to equality! But for this particular project (HoTTLean), we are using categories and functors as algebraic objects, in order to strictly model the rules of dependent type theory, as explained in this paper.

Thanks for any advice you (all) can give on how to make Lean do what we want!

There are genuine situations where we need strict commutations of diagrams of categories and functors (e.g. this happens when "sheafifying" algebraic K-theory in the works by Brown-Gersten and Thomason), and in order to do so we may even have to "strictify" certain pseudofunctors to get actual functors. In such situations, I would say that the end justifies the means.

[Joël Riou]

If you need to prove an equality of functors, I would say that the best practice would be to define an isomorphism first, and then only to use the lemma docs#CategoryTheory.Functor.ext_of_iso in order to get an equality.

[Robin Carlier]

Joël Riou said:

[...]

Thanks for the in-depth explanation!

[Yiming Xu]

Joël Riou said:

If you need to prove an equality of functors, I would say that the best practice would be to define an isomorphism first, and then only to use the lemma docs#CategoryTheory.Functor.ext_of_iso in order to get an equality.

Many many thanks! I checked your links above. Your project is so (impressively!) large that I cannot find a case of the usage of Functor.ext_of_iso. If it is easy enough to identify, could you please point to a place that Functor.ext_of_iso is used, and you are satisfied with the proof, so we can consult that as a reference?

[Joël Riou]

There are good examples in CategoryTheory.Category.Quiv.

[Yiming Xu]

Joël Riou said:

There are good examples in CategoryTheory.Category.Quiv.

Sorry! I do not spot a any occurrence of ext_of_iso in this file. May I please confirm that you are suggesting this one?
https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Quiv.html

[Robin Carlier]

rg 'Functor.ext_of_iso' gives the following 5 matches:

Mathlib/CategoryTheory/Category/Quiv.lean
92:  Functor.ext_of_iso (freeMapIdIso V) (fun _ ↦ rfl) (fun _ ↦ rfl)
108:  Functor.ext_of_iso (freeMapCompIso F G)

Mathlib/CategoryTheory/ComposableArrows.lean
207:  Functor.ext_of_iso
275:  Functor.ext_of_iso (isoMk₁ (eqToIso left) (eqToIso right) (by simp [map'_eq_hom₁, w]))
540:  exact Functor.ext_of_iso (isoMkSucc (eqToIso h₀) (eqToIso h) (by

[Yiming Xu]

Thank you! I do not see any of them, it is indicating that I should update my mathlib!! Good reminder.