externalProductBifunctor — Mathlib

English

There is a natural isomorphism between two swapped external product constructions, natural in both factors.

Русский

Существует естественный изоморфизм между двумя переставленными конструкциями внешнего произведения, естественный по обоим множителям.

LaTeX

$$externalProductSwap \\;\\text{(NatIso)}$$

Lean4

/-- The external product bifunctor: given diagrams
`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`. -/
@[simps!]
def externalProductBifunctor : ((J₁ ⥤ C) × (J₂ ⥤ C)) ⥤ J₁ × J₂ ⥤ C :=
  uncurry.obj <| (Functor.postcompose₂.obj <| uncurry).obj <| externalProductBifunctorCurried J₁ J₂ C

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