Dagur Asgeirsson
Dagur Asgeirsson
This PR includes some Grothendieck construction stuff, which it shouldn't, according to the PR description
Indeed, `IsCocontinuous` is enough to preserve local surjectivity. I haven't managed to prove the other direction for a cover dense fully faithful functor, I'm not sure how to relate the...
Ok, here is a more promising approach: ```lean lemma isLocallySurjective_of_whisker' (H : D ⥤ C) [H.IsCoverDense J] [H.Full] [H.Faithful] [IsLocallySurjective (H.inducedTopologyOfIsCoverDense J) (whiskerLeft H.op f)] : IsLocallySurjective J f where...
Ok, the latter approach worked. I bet it can be modified for locally injective as well. I'll finish it and clean up tomorrow.
Nice, thanks! Actually the proof I wrote using `J.transitive` also works for that statement.
All that's left in this PR is now some instances I added in the equivalence file, the preserving and reflecting of local injectivity and surjectivity is #13621
This PR has changed a bit, lots of the initial material has been incorporated into other PRs that have now been merged, but what's left now is still used in...
Thanks! bors merge