feat(FiberedCategory/HomLift): definition of IsHomLift

[callesonne]

We define the notion IsHomLift which aims to provide API for working with equalities p(\phi) = f for a functor p and morphisms \phi, f. This API is extensively used in an upcoming PR defining the notion of fibered categories. See the repository Stacks-project for WIP using this notion.

Co-authored-by: Paul Lezau [email protected]

---

[callesonne]

Okay, I've made some changes now. ~~One thing to note is that the file is significantly slower than before on my computer, but maybe this doesn't matter so much~~ (this was just due to some lemmas that shouldnt have been tagged with @[simp], this has been fixed now).

Another thing that would be nice, but I'm not sure how to add, is if aesop_cat (or simp) could deduce domain_eq and codomain_eq given that a suitable instance of IsHomLift is available. That would be helpful for automation when defining IsHomLift instances. For example, I feel that the domain_eq field of comp_lift_id_right should be able to be automated. Do you know if this is possible in any way?

One thought I just had, is that maybe it could be a good idea to add the class IsObjLift, which would allow type-class inference to infer domain_eq and codomain_eq. But maybe this is a bit overkill.

[joelriou]

One thought I just had, is that maybe it could be a good idea to add the class IsObjLift, which would allow type-class inference to infer domain_eq and codomain_eq. But maybe this is a bit overkill.

I have added a suggestion of alternate proof for comp_lift_id_right. If we can be avoid introducing IsObjLift. It is probably better!

(In proofs involving a map f over another map g, I think that in many cases, we should be able to do substitutions so that we may assume that g is definitionally p.map f: first substitute the equality of objects (as I did above), then simp the map equality to get rid of the eqToHom, and then substitute the equality of maps.)

[callesonne]

One thought I just had, is that maybe it could be a good idea to add the class IsObjLift, which would allow type-class inference to infer domain_eq and codomain_eq. But maybe this is a bit overkill.

I have added a suggestion of alternate proof for comp_lift_id_right. If we can be avoid introducing IsObjLift. It is probably better!

(In proofs involving a map f over another map g, I think that in many cases, we should be able to do substitutions so that we may assume that g is definitionally p.map f: first substitute the equality of objects (as I did above), then simp the map equality to get rid of the eqToHom, and then substitute the equality of maps.)

Thanks a lot! I will keep this in mind for the other proofs in this PR (I think it might become especially relevant for the other IsFibered PR). I didn't know that rfl could be used as a pattern like that, thats very good to know, so thanks a lot!

[callesonne]

I have now fixed your comments, as well as redefined IsHomLift using inductive types as in the zulip thread. I also added a macro subst_hom_lift to make the substitution a bit more readable.

[callesonne]

I'm not convinced about using IsHomLift as a class anymore, basically for the following two reasons:

1. IsHomLift p f φ makes it so that I can leave parameters p, f, φ implicit, which makes it slightly more convenient to apply lemmas which has it as a parameter. Especially in situations where the expressions for f and φ are somewhat complicated (involving eqToHoms ) it would be quite convenient to not have to write them down explicitly.
2. There are often situations where type-class inference can't infer IsHomLift, and having it as a class makes it quite inconvenient to try and give this instance explicitly. For example the following lemma is very simple, but can't be inferred by type-class inference: protected lemma id {p : 𝒳 ⥤ 𝒮} {R : 𝒮} {a : 𝒳} (ha : p.obj a = R) : p.IsHomLift (𝟙 R) (𝟙 a) := . So whenever I want to use this instance, I have to either have another line before with a have statement, which feels inconvenient for such a simple lemma, or use @ notation.

Also, I havn't felt many of the benefits of having it as a class, I think the only noticeable thing to me is that IsHomLift.comp can be inferred, which can be quite nice.

It is very possible that I am not fully using the benefits of having a class (and that these issues shouldn't arise if I use it correctly), so please take what I say with a grain of salt :)

[joelriou]

1. `IsHomLift p f φ` makes it so that I can leave parameters `p, f, φ` implicit, which makes it slightly more convenient to apply lemmas which has it as a parameter. Especially in situations where the expressions for `f` and `φ` are somewhat complicated (involving `eqToHoms` ) it would be quite convenient to not have to write them down explicitly.

The change of design (using an inductive type, the API for substitutions, etc) makes it so that in principle, you should not need to write that many lemmas where eqToHom should appear in the assumptions (although, they may occasionally appear in the statements).

2. There are often situations where type-class inference can't infer `IsHomLift`, and having it as a class makes it quite inconvenient to try and give this instance explicitly. For example the following lemma is very simple, but can't be inferred by type-class inference:
   `protected lemma id {p : 𝒳 ⥤ 𝒮} {R : 𝒮} {a : 𝒳} (ha : p.obj a = R) : p.IsHomLift (𝟙 R) (𝟙 a) := `.

We should basically almost never need to use this lemma, because we may do subst ha, and then the instance can be infered!

[callesonne]

Okay, this makes sense. I think the times I have encountered it has all been in short term-mode proofs, when I had to change the proof from 1 to 2 lines because of this. But then like you say this will be the worst case, as in longer proofs I should just do the substitution first. So I am happy with it :)

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style