balanced_opposite — Mathlib

English

If a category C is Balanced, then its opposite C^op isBalanced as well.

Русский

Если категория C сбалансирована, то и противоположная категория C^op тоже сбалансирована.

LaTeX

$$$$ \text{Balanced}(C^\mathrm{op}). $$$$

Lean4

instance balanced_opposite [Balanced C] : Balanced Cᵒᵖ :=
  {
    isIso_of_mono_of_epi := fun f fmono fepi => by
      rw [← Quiver.Hom.op_unop f]
      exact isIso_of_op _ }

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