prodLift — Mathlib

English

The product of two localizations satisfies the universal property of the localized product category.

Русский

Произведение двух локализаций удовлетворяет универсальному свойству локализованной продукции категорий.

LaTeX

$$$\\text{prod} :\\text{ StrictUniversalPropertyFixedTarget (W1.Q.prod W2.Q) (W1.prod W2) E}$$$

Lean4

/-- The lifting of a functor `F : C₁ × C₂ ⥤ E` inverting `W₁.prod W₂` to a functor
`W₁.Localization × W₂.Localization ⥤ E` -/
noncomputable def prodLift : W₁.Localization × W₂.Localization ⥤ E :=
  by
  refine uncurry.obj (Construction.lift (prodLift₁ F hF).flip ?_).flip
  intro _ _ f₂ hf₂
  haveI : ∀ (X₁ : W₁.Localization), IsIso (((Functor.flip (prodLift₁ F hF)).map f₂).app X₁) := fun X₁ =>
    by
    obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
    exact
      ((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
            (((Functor.mapArrowFunctor _ _).mapIso (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app
              (Arrow.mk f₂))).2
        (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)
  apply NatIso.isIso_of_isIso_app

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