isCodetector_iff_reflectsIsomorphisms_yoneda_obj

English

A codetector G is equivalent to the Yoneda image of G reflecting isomorphisms after applying op or not, i.e., the Yoneda object reflects isomorphisms.

Русский

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

LaTeX

$$$\\mathrm{IsCodetector}(G) \\iff (\\mathrm{yoneda.obj}(G)).\\mathrm{ReflectsIsomorphisms}$$$

Lean4

theorem isCodetector_iff_reflectsIsomorphisms_yoneda_obj (G : C) :
    IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms :=
  by
  refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩
  · refine (isIso_unop_iff _).1 (hG.def _ ?_)
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
  · rw [← isIso_op_iff]
    suffices IsIso ((yoneda.obj G).map f.op) by exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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