feat(category_theory/limits): equivalences create limits

[semorrison]

We provide

instance has_limit_comp_equivalence {D : Type u'} [category.{v+1} D]
  (E : C ⥤ D) [is_equivalence E] [has_limit F] : has_limit (F ⋙ E) := ...

def has_limit_of_comp_equivalence {D : Type u'} [category.{v+1} D] 
  (E : C ⥤ D) [is_equivalence E] [has_limit (F ⋙ E)] : has_limit F := ...

[jcommelin]

@semorrison Can't you use https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/adjunction/limits.lean#L90

def right_adjoint_preserves_limits : preserves_limits G :=

After all, the equivalences in mathlib are now adjoint equivalences.

[semorrison]

Oh!

…

On Thu, Jul 4, 2019 at 8:42 AM Johan Commelin ***@***.***> wrote: @semorrison <https://github.com/semorrison> Can't you use https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/adjunction/limits.lean#L90 def right_adjoint_preserves_limits : preserves_limits G := After all, the equivalences in mathlib are now adjoint equivalences. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1175?email_source=notifications&email_token=AADUWBBZ433APQGBNQETLOLP5X45TA5CNFSM4H5GQBZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZHOMSQ#issuecomment-508487242>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADUWBFDRR5BPH7X4ORG473P5X45TANCNFSM4H5GQBZA> .

[semorrison]

Okay, I've switched to using right_adjoint_preserves_limits. Thanks for pointing this out!

Unfortunately the implicit arguments in the preserves_limit* API make it very hard to use, witness https://github.com/leanprover-community/mathlib/pull/1175/files#diff-171c7c8eaccb86dd820fc704b9e1e6e3R120. I think my preference is to fix this in a separate PR.

[jcommelin]

There is now a whole bunch of files where the only changes have to do with set.mem_preimage. Is this related to a recent PR of Patrick, and did some wires get crossed? Or is this intentional?

[semorrison]

No, sorry, that’s not intentional. I’ll investigate later, I need to give a talk in a moment.

…

On Thu, Jul 4, 2019 at 11:22 AM Johan Commelin ***@***.***> wrote: There is now a whole bunch of files where the only changes have to do with set.mem_preimage. Is this related to a recent PR of Patrick, and did some wires get crossed? Or is this intentional? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1175?email_source=notifications&email_token=AADUWBEINA7MUZVKZ7S3OSLP5YPVBA5CNFSM4H5GQBZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZHZNVA#issuecomment-508532436>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADUWBCFAU7OU5QGI62P4V3P5YPVBANCNFSM4H5GQBZA> .

[semorrison]

Sorted. Don't know what happened, but git checkout master src/topology/ solved the problem.

[semorrison]

I'm happy with this PR as is now. The proof

def is_limit_map_cone (E : D ⥤ C) [is_equivalence E]
  (c : cone K) (h : is_limit c) : is_limit (E.map_cone c) :=
begin
  have P : preserves_limits E := adjunction.right_adjoint_preserves_limits E.inv.adjunction,
  have P' := P.preserves_limits_of_shape,
  have P'' := P'.preserves_limit,
  have P''' := P''.preserves,
  exact P''' h,
end

is awful, but that's because of design problems in the preserves_limits.lean API. I think I can address those, but I'd prefer to do so in a separate commit.

[jcommelin]

@semorrison Shouldn't we also have the dual is_colimit_map_cocone etc...?

[semorrison]

Yes, eventually. :-) I have another PR lined up that does monadic adjunctions, and proves monadic functors, including reflective inclusions, create limits. So for that I only need this half. I'm about to go on holiday so may not get to the other half of this immediately, even though it should just be copy-paste.

[semorrison]

I added the corresponding definitions for colimits.