isDetecting — Mathlib

English

In a balanced category, if a set 𝒢 is separating, then it is detecting.

Русский

В сбалансированной категории, если множество 𝒢 разделяющее, тогда оно обнаруживает изоморфизмы.

LaTeX

$$$IsSeparating(\mathcal{G}) \Rightarrow IsDetecting(\mathcal{G})$$$

Lean4

theorem isDetecting [Balanced C] {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) : IsDetecting 𝒢 :=
  by
  intro X Y f hf
  refine (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => h𝒢 _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩
  · obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)
    rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]
  · refine h𝒢 _ _ fun G hG i => ?_
    obtain ⟨t, rfl, -⟩ := hf G hG i
    rw [Category.assoc, hgh, Category.assoc]

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