isSeparating — Mathlib

English

In a category with equalizers, if a set 𝒢 of objects is detecting, then it is separating; i.e., the ability to detect isomorphisms via 𝒢 implies the separating property for parallel arrows.

Русский

В категории с равными пределами, если множество объектов 𝒢 обнаруживает изоморфизмы, то оно разделяет пары параллельных стрел; то есть детектирование изоморфизмов приводит к свойству разделения.

LaTeX

$$$\text{IsSeparating}(\mathcal{G}) \;\text{given that} \; \text{IsDetecting}(\mathcal{G})\text{ (under HasEqualizers).}$$$

Lean4

theorem isSeparating [HasEqualizers C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) : IsSeparating 𝒢 := fun _ _ f g hfg =>
  have : IsIso (equalizer.ι f g) := h𝒢 _ fun _ hG _ => equalizer.existsUnique _ (hfg _ hG _)
  eq_of_epi_equalizer

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