instHasCoseparator — Mathlib

English

Every Grothendieck abelian category has a coseparator, derived from a separator via an equivalence ShrinkHoms.

Русский

У абелевой категории Гротениджа есть косепоратор, получаемый из сепаратора через эквивалентность ShrinkHoms.

LaTeX

$$$\text{HasCoseparator } C$$$

Lean4

instance : HasCoseparator C :=
  by
  suffices HasCoseparator (ShrinkHoms C) from HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm
  obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C)) (isSeparator_separator _)
  exact ⟨G, hG⟩

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