balanced_of_preserves — Mathlib

English

If F reflects isomorphisms and preserves epimorphisms and monomorphisms and D is balanced, then C is balanced.

Русский

Если F отражает изоморфизмы и сохраняет эпиморфизмы и мономорфизмы, а D сбалансирована, то C также сбалансирована.

LaTeX

$$$\\text{Balanced}(D) \\,\\wedge\\, F.ReflectsIsomorphisms \\wedge F.\\PreservesEpimorphisms \\wedge F.\\PreservesMonomorphisms \\Rightarrow \\text{Balanced}(C).$$$

Lean4

theorem balanced_of_preserves (F : C ⥤ D) [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms]
    [Balanced D] : Balanced C where
  isIso_of_mono_of_epi f _
    _ := by
    rw [← isIso_iff_of_reflects_iso (F := F)]
    exact isIso_of_mono_of_epi _

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