extensionUnitRight — Mathlib

Русский

При тех же данных существует каноническое правое расширение: extensionUnitRight : K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H'.

LaTeX

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

Lean4

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

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