English
The product functor is a localization functor for the product classes, given the previous construction.
Русский
Произведение функторов является локализационным функтором для соответствующих классов.
LaTeX
$$$\\text{prodIsLocalization} \\Rightarrow (L_1.prod L_2).IsLocalization (W_1.prod W_2)$$$
Lean4
/-- If `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` are localization functors
for `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` respectively,
and if both `W₁` and `W₂` contain identities, then the product
functor `L₁.prod L₂ : C₁ × C₂ ⥤ D₁ × D₂` is a localization functor for `W₁.prod W₂`. -/
instance prod [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] : (L₁.prod L₂).IsLocalization (W₁.prod W₂) :=
by
haveI := Construction.prodIsLocalization W₁ W₂
exact
of_equivalence_target (W₁.Q.prod W₂.Q) (W₁.prod W₂) (L₁.prod L₂) ((uniq W₁.Q L₁ W₁).prod (uniq W₂.Q L₂ W₂))
(NatIso.prod (compUniqFunctor W₁.Q L₁ W₁) (compUniqFunctor W₂.Q L₂ W₂))
