isDetector_iff_reflectsIsomorphisms_coyoneda_obj

English

A detector G is equivalent to the Yoneda image of G reflecting isomorphisms; i.e., G is a detector iff the Yoneda image reflects isomorphisms.

Русский

Детектор G эквивалентен тому, что образ Yoneda отражает изоморфизмы; то есть G является детектором тогда как образ Yoneda отражает изоморфизмы.

LaTeX

$$$\\mathrm{IsDetector}(G) \\iff (\\mathrm{coyoneda.obj}(\\mathrm{op}\,G)).\\mathrm{ReflectsIsomorphisms}$$$

Lean4

theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) :
    IsDetector G ↔ (coyoneda.obj (op G)).ReflectsIsomorphisms :=
  by
  refine ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h => (isDetector_def _).2 fun X Y f hf => ?_⟩
  · rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
    exact hf h
  · suffices IsIso ((coyoneda.obj (op G)).map f) by exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Похожие утверждения