The wide subcategory on monomorphisms?

Stream: Is there code for X?

[Brendan Seamas Murphy]

I was hoping that this was already implemented by the MorphismProperty stuff but it didn't look like it. Is there a more specialized way of doing it that's already in mathlib?

[Adam Topaz]

I don’t think we have anything like this. I would add the construction of a wide subcat associated to a morphism property which respects isos and compositions

[Brendan Seamas Murphy]

Yeah, I'll go ahead and do that

[Adam Topaz]

Do we have docs#CategoryTheory.MorphismProperty.respectsIdentity

[Adam Topaz]

I guess respecting isos is a less evil property anyway

[Brendan Seamas Murphy]

Re: (non) evil stuff, the function MorphismProperty.map forms the image up to isomorphisms instead of the image on the nose and I think this is a bad design decision & that the name is misleading. If someone is working with categories as strict objects/working in the 1-cat Cat then you really would want the on the nose image. I would suggest having map be the strict map and defining essMap (P : MorphismProperty C) (F : C ⥤ D) := isoClosure (map P F). Anyone have thoughts on this?

[Joël Riou]

It seems you are looking for docs#CategoryTheory.MorphismProperty.IsMultiplicative

Please note that we do not have the notion of isomorphisms of categories: we only have equivalences. Early designs decisions in the category theory library prevent people to even think about "evil" stuff.

I would not mind too much if you renamed MorphismProperty.map as essMap, define a more strict map and prove the lemma P.essMap F = isoClosure (P.map F).

[Brendan Seamas Murphy]

I'm not sure what you mean by not having the notion of isomorphism of categories? There is an instance LargeCategory Cat and thus a notion of isomorphism of categories in mathlib. It seems like a bad idea to prevent people from thinking about evil stuff if the goal is to be able to formalize math, since some category theory is evil (eg grothendieck fibrations, the thomason model structure)

Edit: Also there's a definition of skeletal categories in mathib

[Adam Topaz]

Why are Grothendieck fibrations evil? They’re not evil if you do them correctly (I.e. using pseudofunctors)

[Brendan Seamas Murphy]

The definition of a cartesian morphism talks about equality of morphisms in different Homs, and so equality of objects

[Adam Topaz]

Maybe “prevent” is too strong a word, but experience shows that “evil” translates to “pain when formalizing” quite consistently

[Brendan Seamas Murphy]

Er, that's not quite right sorry. It's the existence of a cartesian lift that talks about equality of objects

[Adam Topaz]

Doesn’t that get solved with pseudofunctors?

[Adam Topaz]

If you think of a Grothendieck fibration as a plain old functor, then I agree that it is evil

[Brendan Seamas Murphy]

I thought you were talking about functors vs pseudofunctors on the other side of the grothendieck correspondence, sorry. What do you have in mind for the definition of a grothendieck fibration?

[Brendan Seamas Murphy]

Usually they go between 1-categories, so I'm not sure how one could be replaced with a pseudofunctor

[Adam Topaz]

Oh wait I’m thinking of the Grothendieck construction, sorry.

[Adam Topaz]

Anyway, if you have higher category theory where you can talk about sheaves of categories, do you really still need Grothendieck fibrations?

[Brendan Seamas Murphy]

/shrug I would say that's a matter of opinion. Do we still need the total space of a vector bundle if we can think of it as a locally free sheaf instead?

[Brendan Seamas Murphy]

(also, to be clear, there is a way of making the definition non-evil in the literature. but people talk and reason about grothendieck fibrations more frequently than they do street fibrations)

[Adam Topaz]

(FWIW, I've been thinking a lot about what "evil" really means lately, as I've been doing some stuff around Lawvere theories)

[Notification Bot]

Brendan Seamas Murphy has marked this topic as resolved.

[Notification Bot]

Brendan Seamas Murphy has marked this topic as unresolved.

[Brendan Seamas Murphy]

I added some stuff about wide subcategories and in the process refactored parts of the MorphismProperty file (changing map -> essMap like discussed above and making more order-theoretic structures apparent). I also ended up with some stuff about setoids and the saturation of a subset (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.20that.20descends.20to.20a.20quotient), as well as adding general lemmas in the order theory library. I'd also like to unify the Quiver.Total and CategoryTheory.Arrow structures; it would be nice if the comma category structure was initially defined for a pair of prefunctors between quivers (this is a little odd since the "comma quiver" doesn't actually have a quiver structure, but I still think it would be nice to unify things). Not sure if I should keep working on that on this branch or treat it as a separate thing after this is merged

In progress PR: https://github.com/leanprover-community/mathlib4/compare/master...MorphismPropertySubcategory

[Brendan Seamas Murphy]

Also, the argument order of map/inverseImage is very strange and I think it should be flipped for consistency with eg sets

[Joël Riou]

For the order of arguments of MorphismProperty.inverseImage, the idea was to allow dot notation.

[Brendan Seamas Murphy]

P.inverseImage F just looks backwards to me, but maybe I'm alone here

[Patrick Massot]

You are not alone, this issue appear in several places in Mathlib, and I think we should simply not use dot notation in this case.

[Joël Riou]

Brendan Seamas Murphy said:

Not sure if I should keep working on that on this branch or treat it as a separate thing after this is merged

I would think that this is already too big for a single PR, and that it should at least be split into several PR (one or two for the modifications of the most lowlevel files only, one for the renamings about MorphismProperty.map, one for the new WideCategory stuff).

Initially, I had suggested defining MorphismProperty C as Set (Arrow C), but this idea was rejected (do not ask me why). Then, reintroducing Set (Arrow C) as part of the MorphismProperty API is probably not welcome.

[Joël Riou]

Anyway, this should also be a good opportunity to split the file CategoryTheory.MorphismProperty into several shorter files.

[Brendan Seamas Murphy]

Ah okay, I didn't know that about the history of MorphismProperty. I think it's desirable to be able to write P f or f \in P where f is a homomorphism, but we can't do this with DFunlike or Mem because of their choice of outparams (I think?). Can you link to the original discussion about this? I feel like it might be nicest to have MorphismProperty be a set of arrows directly and to provide a coercion from X ⟶ Y to Arrow C

[Brendan Seamas Murphy]

(i will put a pause on any further work and making splitting stuff up a priority today)

[Adam Topaz]

I don't remember the history, but I think the Set (Arrow C) approach was rejected because writing $f \in P$ for a morphism f : X -> Y, which has type X \hom Y and not Arrow C, would have caused issues.

[Adam Topaz]

Note that Membership X Y has X as an outParam.

[Adam Topaz]

Brendan Seamas Murphy said:

...provide a coercion from X ⟶ Y to Arrow C

I think this exists...

[Brendan Seamas Murphy]

Ah yep it does

[Joël Riou]

Brendan Seamas Murphy said:

Ah okay, I didn't know that about the history of MorphismProperty. I think it's desirable to be able to write P f or f \in P where f is a homomorphism

If f :X ⟶ Y, it is possible to write P f, but not f \in P. It is probably better we cannot write f \in P because this would give two different syntaxes for the exact same thing, which we should try to avoid (e.g. in order to do rewrites, we would need twice as many lemmas depending on which syntax is used...). If w : Arrow C, we can write P w.hom, which seems quite reasonable.

I feel like it might be nicest to have MorphismProperty be a set of arrows directly and to provide a coercion from X ⟶ Y to Arrow C

The current design and the Set (Arrow C) design are equally ok. The point is that there is already a certain amount of code which uses the current design (algebraic geometry, localization of categories, and I have many more planned PRs...). Then, unless some very strong arguments are given, refactoring this just for the sake of changing the definition seems to me like a total waste of time and energy.

[Brendan Seamas Murphy]

Adam Topaz said:

I don't remember the history, but I think the Set (Arrow C) approach was rejected because writing $f \in P$ for a morphism f : X -> Y, which has type X \hom Y and not Arrow C, would have caused issues.

Yeah I'm realizing this now, and I don't really understand what's causing these issues. In my mental model the fact that Membership has the member-type as an outparam means that when I write $f \in P$ the typesclass resolution should find an instance Membership (Arrow C) (MorphismProperty C), deduce that f needs to have type Arow C, then find the coercion from X \hom Y to Arraow C

[Brendan Seamas Murphy]

Can someone break down for me why this isn't what happens?

[Adam Topaz]

If you explicitly tell lean to coerce, then it works:

import Mathlib

open CategoryTheory
variable (C : Type*) [Category C] (X Y : C) (f : X ⟶ Y) (S : Set (Arrow C))

example : Prop := ↑f ∈ S

[Adam Topaz]

you could trace typeclass inference to see what's going on.

[Adam Topaz]

If I understand correctly the issue without the explicit coercion is that typeclass search finds the Membership (Arrow C) (Set (Arrow C)) instance, with Arrow C being an outParam, and since the type of f is not Arrow C, the search fails. Now with the up arrow, there is another class to find for the coercion, and lean knows that it should look for a coercion to Arrow C from the other step, and it is finally able to find such a coercion, so it works.

[Brendan Seamas Murphy]

Maybe the issue is that I don't know when or why lean decides to insert coercions

[Brendan Seamas Murphy]

gah, (. ∈ P) f does typecheck

[Adam Topaz]

I guess lean does insert coercions when it elaborates function applications? We should wait for a typeclass expert to chime in :)

[Brendan Seamas Murphy]

(f : _) ∈ P fails to synthesize a membership instance like before, (f : ?_) ∈ P works!

[Brendan Seamas Murphy]

I've made a series of PRs breaking up my one big commit from earlier: #10347, #10348, #10349, and #10350. The actual wide subcategory definition isn't in any of these, I'd like to hold off on PRing it in until Quiver.Total/Arrow and WideSubquiver/MorphismProperty are better unified (also, WideSubquiver is a bad name and WideSubcategory should be a special case of the subcategory formed by a MorphismProperty closed under composition and taking the identity of the domain/codomain of any morphism in it, but which may not contain all objects)

[Johan Commelin]

I kicked the first one on the queue