prodCompExternalProduct — Mathlib

English

There is a canonical isomorphism showing that composing F₁.prod F₂ with G₁ ⊠ G₂ equals the tensor of the composed functors.

Русский

Существует канонический изоморфизм, показывающий что композиция F₁.prod F₂ с G₁ ⊠ G₂ равна тензору составленных функторов.

LaTeX

$$F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂)$$

Lean4

/-- Composing `F₁ × F₂` with `G₁ ⊠ G₂` is isomorphic to `(F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂)`. -/
@[simps!]
def prodCompExternalProduct (F₁ : I₁ ⥤ J₁) (G₁ : J₁ ⥤ C) (F₂ : I₂ ⥤ J₂) (G₂ : J₂ ⥤ C) :
    F₁.prod F₂ ⋙ G₁ ⊠ G₂ ≅ (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂) :=
  NatIso.ofComponents (fun _ ↦ Iso.refl _)

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