prod — Mathlib

English

If W1 is inverted by F1 and W2 by F2, then their product W1.prod W2 is inverted by F1.prod F2.

Русский

Если W1 разворачивается по F1 и W2 по F2, то их произведение разворачивается по F1.prod F2.

LaTeX

$$$ (W_1.\mathrm{IsInvertedBy} F_1) \to (W_2.\mathrm{IsInvertedBy} F_2) \Rightarrow (W_1 \mathrm{prod} W_2).\mathrm{IsInvertedBy}(F_1 \mathrm{prod} F_2) $$$

Lean4

theorem prod {C₁ C₂ : Type*} [Category C₁] [Category C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂}
    {E₁ E₂ : Type*} [Category E₁] [Category E₂] {F₁ : C₁ ⥤ E₁} {F₂ : C₂ ⥤ E₂} (h₁ : W₁.IsInvertedBy F₁)
    (h₂ : W₂.IsInvertedBy F₂) : (W₁.prod W₂).IsInvertedBy (F₁.prod F₂) := fun _ _ f hf =>
  by
  rw [isIso_prod_iff]
  exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩

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