tensorFunc_obj_map — Mathlib

English

The tensorFunc map on an object Z commutes with the projection/inclusion structure, mapping f through the inclusion maps to the tensor level.

Русский

Тождество отображения tensorFunc на объекте Z согласуется с инклюзией и отображением f через вложение в тензорную структуру.

LaTeX

$$$ ((tensorFunc C).obj Z).map f = inclusion.map f \;\vg Z $$$

Lean4

theorem tensorFunc_obj_map (Z : F C) {n n' : N C} (f : n ⟶ n') : ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z :=
  by
  cases n
  cases n'
  rcases f with ⟨⟨h⟩⟩
  dsimp at h
  subst h
  simp

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