toSkeleton_tensorObj — Mathlib

English

The mapping from a tensor product in C to the tensor product in the skeleton is compatible: toSkeleton(X ⊗ Y) = toSkeleton X * toSkeleton Y.

Русский

Гомоморфизм к скелету сохраняет тензорную структуру: toSkeleton(X ⊗ Y) = toSkeleton X * toSkeleton Y.

LaTeX

$$$\\mathrm{toSkeleton}(X \\otimes Y) = \\mathrm{toSkeleton}(X) \\;*\\; \\mathrm{toSkeleton}(Y)$$$

Lean4

theorem toSkeleton_tensorObj (X Y : C) : toSkeleton (X ⊗ Y) = toSkeleton X * toSkeleton Y :=
  let φ := (skeletonEquivalence C).symm.unitIso.app;
  Quotient.sound ⟨φ X ⊗ᵢ φ Y⟩

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