Limit over a diagram of a single object and morphism

Stream: Is there code for X?

[Junyan Xu]

... is canonically isomorphic to the object. Do we have this?

import Mathlib.CategoryTheory.Limits.IsLimit
open CategoryTheory Limits
variable {C J} [Category C] [Category J] (F : J ⥤ C)
theorem ι_isIso_of_subsingleton [Subsingleton J] (j : J) [Subsingleton (j ⟶ j)]
    {t : Cocone F} (ht : IsColimit t) : IsIso t.ι := by
  sorry

un- #xy: I'd like to show if you have a presheaf on a topological space and an isolated point x in the space, then the germ map is an isomorphism from the sections on the open set {x} to the stalk at x.

[Adam Topaz]

I think you can deduce this from the fact that a colimit of a diagram with a terminal object is just the image of that terminal object, which we do have in mathlib

[Adam Topaz]

And showing that your diagram has a terminal object using your sub singleton assumptions should be barely more than inferInstance

[Adam Topaz]

It may actually be more direct to show that the poset of nhds of an isolated point has an initial object in your in-xy’d case

[Junyan Xu]

Thanks! I didn't end up needing this; my goal is to show if a basic open D(f) in the spectrum of a comm. ring is a singleton {p}, then localization away from f is the same as localization at p. I was able to do it without using the structure sheaf in #18891 because @Andrew Yang has done the preliminary work (correspondence between clopens and idempotents) without using it.

[Andrew Yang]

Out of curiosity: what do you need this for?

[Andrew Yang]

Ah I see the linked PR

[Junyan Xu]

Original motivation was to show the Picard group of Artinian ring is trivial :)