English
Assume 𝒢 is detecting and f: X → Y is mono. Then f is an isomorphism if and only if for every s ∈ 𝒢, the map on Coyoneda along f is surjective.
Русский
Пусть 𝒢 детективно. Для мономорфизма f: X→Y имеем: f является изоморфизмом тогда и только тогда, когда для каждого s ∈ 𝒢 отображение наCoyoneda вдоль f сюръективно.
LaTeX
$$$IsDetecting(\mathcal{G}) \Rightarrow (\forall f: X\to Y)\; [Mono f] \; IsIso f \iff \forall s\in\mathcal{G},\; Surjective((\mathrm{coyoneda}(\mathrm{op}s)).map f)$$$
Lean4
theorem isIso_iff_of_mono {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X Y : C} (f : X ⟶ Y) [Mono f] :
IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f) :=
by
constructor
· intro h
rw [isIso_iff_yoneda_map_bijective] at h
intro A _
exact (h A).2
· intro hf
refine h𝒢 _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
· exact hf A hA g
· intro l₁ l₂ h₁ h₂
rw [← cancel_mono f, h₁, h₂]
