extensionUnitLeft — Mathlib

Русский

Заданы моноидальные функторы H: D → V, H': D' → V и K: E → V и естественное преобразование α: H ⇒ L ⋙ H'. Существует каноническое левое расширение для внешнего произведения: extensionUnitLeft : H ⊠ K ⇒ L.prod (𝟭 E) ⋙ H' ⊠ K, которое получено благодаря двойному произведению (бифункториальности) внешнего произведения через α и левый единичный преобразователь K.

LaTeX

$$$extensionUnitLeft : H \\boxtimes K \\longrightarrow (L.prod(\\text{Id}_E)) \\;\\circ\\; (H' \\boxtimes K)$$$

Lean4

/-- Given an extension `α : H ⟶ L ⋙ H'`, this is the canonical extension
`H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K` it induces through bifunctoriality of the external product. -/
abbrev extensionUnitLeft : H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K :=
  (externalProductBifunctor D E V).map (α ×ₘ K.leftUnitor.inv)

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