hasTensor_of_iso — Mathlib

English

Tensor structure is preserved under isomorphism of graded objects: if X1 ≅ Y1 and X2 ≅ Y2 and HasTensor X1 X2, then HasTensor Y1 Y2.

Русский

Теорема сохранения тензора при изоморфизма градуированных объектов: если X1 ≅ Y1, X2 ≅ Y2 и HasTensor X1 X2, то HasTensor Y1 Y2.

LaTeX

$$$\forall X_1,X_2,Y_1,Y_2:\, X_1\cong Y_1, X_2\cong Y_2 \Rightarrow HasTensor Y_1 Y_2$ given $HasTensor X_1 X_2$$$

Lean4

theorem hasTensor_of_iso {X₁ X₂ Y₁ Y₂ : GradedObject I C} (e₁ : X₁ ≅ Y₁) (e₂ : X₂ ≅ Y₂) [HasTensor X₁ X₂] :
    HasTensor Y₁ Y₂ :=
  by
  let e : ((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂ ≅ ((mapBifunctor (curriedTensor C) I I).obj Y₁).obj Y₂ :=
    isoMk _ _ (fun ⟨i, j⟩ ↦ (eval i).mapIso e₁ ⊗ᵢ (eval j).mapIso e₂)
  exact hasMap_of_iso e _

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