limit lift is iso

Stream: Is there code for X?

[Emily Riehl]

I'd like to prove that a map defined as a limit.lift of some cone over some diagram is an isomorphism by proving that this cone is a limit cone. Is there a theorem for this?

I see some related things that would be less efficient to use, for instance, that a cone morphism between two limit cones is an isomorphism. Suggestions very welcome!

[Dagur Asgeirsson]

Is docs#CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso what you're looking for?

[Emily Riehl]

This is close, but since I want a specific map to be an isomorphism, I'd have to check that the arrow of the isomorphism given in the conclusion of conePointUniqueUpToIso equals the specific component cone.pt (which is by definition) and then that this map agrees with my original limit.lift (which is probably a theorem) and then conclude that the latter map is an isomorphism since it is equal to an isomorphism.

[Emily Riehl]

Or is there a way to avoid all that?

[Dagur Asgeirsson]

The proof that the hom of this isomorphism equals limit.lift is by rfl:

[Dagur Asgeirsson]

import Mathlib

open CategoryTheory Limits

variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D) (c : Cone F) (hc : IsLimit c) [HasLimit F]

instance : IsIso (limit.lift F c) :=
  inferInstanceAs (IsIso (hc.conePointUniqueUpToIso (limit.isLimit F)).hom)

[Emily Riehl]

@Dagur Asgeirsson here is why I'm having trouble using the existing functions. I'm working on the file

https://github.com/leanprover-community/mathlib4/blob/infty-cosmos/Mathlib/NotInfinityCosmos.lean

(apologies for its current state) on the theorem nerve2coskNatTrans.component_isIso. It would be nice if I could work backwards from the goal to the statement I'm trying to prove (that something or other is a limit cone) but Lean doesn't let me refine the goal first using Iso.isIso_hom and then ideally using conePointUniqueUpToIso ?_ (limit.islimit _).

At the same time the lean info view doesn't display full information about the cone that I'm trying to prove is a limit cone, so I can't copy it out to work forwards to prove the statements I think I need. I know what this cone should be, but I don't know what lean thinks it is, so I'm worried, eg, that if I construct the cone myself to prove that it's a limit, I'll have demonstrated this for a cone that is equal (but not definitionally) or isomorphic to the one I need, and then have to struggle with that.

[Dagur Asgeirsson]

I'll have a look at your branch

[Dagur Asgeirsson]

Can you fill in the two sorries in https://github.com/leanprover-community/mathlib4/blob/dagur/infty-cosmos/Mathlib/NotInfinityCosmos.lean#L547-L554 ?

Note that your branch is quite far behind the current master, and in particular the Kan extension API has changed quite a bit. You might want to merge master and see if you need to make any adaptations to make everything work before continuing

[Dagur Asgeirsson]

I pushed my changes to a new branch based off of yours, if you want to use the code, just merge mine into yours

[Dagur Asgeirsson]

(or copy the code)