unop — Mathlib

English

If L: C^op ⥤ D^op is a localization with respect to W^op, then L.unop: C ⥤ D is a localization with respect to W.

Русский

Если L: C^op → D^op локализует по W^op, то L.unop: C → D локализует по W.

LaTeX

$$$(L.unop).IsLocalization(W)$$$

Lean4

instance unop (L : Cᵒᵖ ⥤ Dᵒᵖ) (W : MorphismProperty Cᵒᵖ) [L.IsLocalization W] : L.unop.IsLocalization W.unop :=
  have : CatCommSq (opOpEquivalence C).functor L.op L.unop (opOpEquivalence D).functor := ⟨Iso.refl _⟩
  of_equivalences L.op W.op L.unop W.unop (opOpEquivalence C) (opOpEquivalence D)
    (fun _ _ _ hf ↦ MorphismProperty.le_isoClosure _ _ hf)
    (fun _ _ _ hf ↦ by
      have := Localization.inverts L W _ hf
      dsimp
      infer_instance)

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