prod — Mathlib

English

If L1,L2 are localizations with identities, then the product L1.prod L2 is a localization for W1.prod W2.

Русский

Если L1 и L2 являются локализациями с идентичностями, то произведение L1.prod L2 является локализацией для W1.prod W2.

LaTeX

$$$[L_1.IsLocalization W_1] [L_2.IsLocalization W_2] \\Rightarrow (L_1.prod L_2).IsLocalization (W_1.prod W_2)$$$

Lean4

/-- The product of two (constructed) localized categories satisfies the universal
property of the localized category of the product. -/
noncomputable def prod : StrictUniversalPropertyFixedTarget (W₁.Q.prod W₂.Q) (W₁.prod W₂) E
    where
  inverts := (Localization.inverts W₁.Q W₁).prod (Localization.inverts W₂.Q W₂)
  lift := fun F hF => prodLift F hF
  fac := fun F hF => prod_fac F hF
  uniq := prod_uniq

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