English
Let X1 and X2 be graded objects in a monoidal category, and for any index k in I and any family of arrows f(i1,i2) : X1(i1) ⊗ X2(i2) → A indexed by pairs with i1 + i2 = k, the canonical iota map from the tensor object to A followed by the object-level description recovers the component f(i1,i2;k).
Русский
Пусть X1 и X2 — градуированные объекты в моноидальной категории, для любого индекса k ∈ I и любой семейства морфиков f(i1,i2) : X1(i1) ⊗ X2(i2) → A, индексируемого парами с условием i1 + i2 = k, каноническое отображение iota из тензорного объекта в A, затем описанное на уровне элементов, восстанавливает компоненту f(i1,i2;k).
LaTeX
$$$\iotaTensorObj X_1 X_2 i_1 i_2 k hi \circ \tensorObjDesc f = f(i_1,i_2,hi).$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_tensorObjDesc {A : C} {k : I} (f : ∀ (i₁ i₂ : I) (_ : i₁ + i₂ = k), X₁ i₁ ⊗ X₂ i₂ ⟶ A) (i₁ i₂ : I)
(hi : i₁ + i₂ = k) : ιTensorObj X₁ X₂ i₁ i₂ k hi ≫ tensorObjDesc f = f i₁ i₂ hi := by apply ι_mapBifunctorMapObjDesc
