isDetecting_op_iff — Mathlib

English

IsDetecting 𝒢.op is equivalent to IsCodetecting 𝒢.

Русский

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

LaTeX

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

Lean4

theorem isDetecting_op_iff (𝒢 : Set C) : IsDetecting 𝒢.op ↔ IsCodetecting 𝒢 :=
  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)

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