op_iff — Mathlib

English

For any L: C ⥤ D and W a morphism property on C, L.op.IsLocalization W.op if and only if L.IsLocalization W.

Русский

Для любого L: C → D и W — свойство морфизмов на C, L^op является локализацией относительно W^op тогда и только тогда, когда L локализует относительно W.

LaTeX

$$$(L^{op}).IsLocalization(W^{op}) \\iff L.IsLocalization(W)$$$

Lean4

@[simp]
theorem op_iff (L : C ⥤ D) (W : MorphismProperty C) : L.op.IsLocalization W.op ↔ L.IsLocalization W :=
  ⟨fun _ ↦ inferInstanceAs (L.op.unop.IsLocalization W.op.unop), fun _ ↦ inferInstance⟩

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