tensorObj_map_tmul — Mathlib

English

The tensor product of morphisms is given by tensorHom(f,g) with components (tensorHom f g)_X = f.app X ⊗ g.app X.

Русский

ТensorHom для отображений определяется как (tensorHom f g)_X = f.app X ⊗ g.app X.

LaTeX

$$$\\mathrm{tensorHom}(f,g)_X = f.app X \\otimes g.app X$.$$

Lean4

@[simp]
theorem tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂ : M₂.obj X) :
    DFunLike.coe (α := (M₁.obj X ⊗ M₂.obj X :)) (β := fun _ ↦
        (ModuleCat.restrictScalars (R.map f).hom).obj (M₁.obj Y ⊗ M₂.obj Y))
        (ModuleCat.Hom.hom (R := ↑(R.obj X)) ((tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[R.obj X] m₂) =
      M₁.map f m₁ ⊗ₜ[R.obj Y] M₂.map f m₂ :=
  rfl

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