English
Dually to the mono case, if f: X → Y is epi and 𝒢 is codetecting, then f is an isomorphism iff for every s ∈ 𝒢, the map on Yoneda along f.op is surjective.
Русский
Дуально к случаю симметричного: если f: X→Y эпиморфизм и 𝒢 кодетектирует, то f — изоморфизм тогда и только тогда, когда для каждого s∈𝒢 отображение на Yoneda вдоль f.op сюръективно.
LaTeX
$$$IsCodetecting(\mathcal{G}) \Rightarrow (\forall f: X\to Y) [Epi f] \; IsIso f \iff \forall s\in\mathcal{G},\; Surjective((\mathrm{yoneda}.obj s).map f.op)$$$
Lean4
theorem isIso_iff_of_epi {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢) {X Y : C} (f : X ⟶ Y) [Epi f] :
IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op) :=
by
constructor
· intro h
rw [isIso_iff_coyoneda_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_epi f, h₁, h₂]
