Isomorphism criteria through descriptions of morphisms out of an object

Let f : A' ⟶ A be a morphism. Suppose that for every object F the morphisms A ⟶ F are described as the elements of some type X F satisfying a property P F, the morphisms A' ⟶ F as the elements of X' F satisfying P' F, and that under these descriptions precomposition with f is a map r F : X F → X' F. By the Yoneda lemma, f is an isomorphism if and only if every element of X' F satisfying P' F is the image under r F of a unique element of X F satisfying P F.

A typical instance is a map of relative free sheaves, where morphisms out of the relative free sheaf of i : U ⟶ V are the sections over V that restrict to zero along i, and r F is a restriction map of sections.

Main results

• TauCeti.CategoryTheory.isIso_iff_existsUnique_of_homEquiv: the isomorphism criterion.

theorem TauCeti.CategoryTheory.isIso_iff_existsUnique_of_homEquiv {D : Type u} [CategoryTheory.Category.{v, u} D] {A' A : D} (f : A' ⟶ A) {X X' : D → Type w} {P : (F : D) → X F → Prop} {P' : (F : D) → X' F → Prop} (r : (F : D) → X F → X' F) (e : (F : D) → (A ⟶ F) ≃ { t : X F // P F t }) (e' : (F : D) → (A' ⟶ F) ≃ { s : X' F // P' F s }) (he : ∀ (F : D) (g : A ⟶ F), ↑((e' F) (CategoryTheory.CategoryStruct.comp f g)) = r F ↑((e F) g)) : CategoryTheory.IsIso f ↔ ∀ (F : D) (s : X' F), P' F s → ∃! t : X F, P F t ∧ r F t = s

Let f : A' ⟶ A, and suppose that for every object F, morphisms A ⟶ F and A' ⟶ F correspond to the elements of X F satisfying P F and of X' F satisfying P' F, in such a way that precomposition with f becomes r F : X F → X' F. Then f is an isomorphism if and only if every element of X' F satisfying P' F is r F t for a unique t satisfying P F.