isCodetecting_op_iff — Mathlib

English

IsCodetecting 𝒢.op is equivalent to IsDetecting 𝒢.

Русский

IsCodetecting 𝒢.op эквивалентно IsDetecting 𝒢.

LaTeX

$$$IsCodetecting(𝒢.op) \iff IsDetecting(𝒢)$$$

Lean4

theorem isCodetecting_op_iff (𝒢 : Set C) : IsCodetecting 𝒢.op ↔ IsDetecting 𝒢 :=
  by
  refine ⟨fun h𝒢 X Y f hf => ?_, fun h𝒢 X Y f hf => ?_⟩
  · refine (isIso_op_iff _).1 (h𝒢 _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop
    exact ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
  · refine (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op
    refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
    exact Quiver.Hom.unop_inj (by simpa only using hy)

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