English
The tensorObj is the presheaf defined by (tensorObj(M1,M2))(X) = M1(X) ⊗ M2(X) with structure maps given by tensorObjMap.
Русский
Тензорный объект — прешефа, для которого (tensorObj(M1,M2))(X) = M1(X) ⊗ M2(X) и переходы заданы tensorObjMap.
LaTeX
$$$(\mathrm{tensorObj}(M_1,M_2))(X) = M_1(X) \\otimes M_2(X),\\quad (\mathrm{tensorObj}(M_1,M_2))(f) = \\mathrm{tensorObjMap}_{X,Y,f}.$$$
Lean4
/-- The tensor product of two presheaves of modules. -/
@[simps obj]
noncomputable def tensorObj : PresheafOfModules (R ⋙ forget₂ _ _)
where
obj X := M₁.obj X ⊗ M₂.obj X
map f := tensorObjMap M₁ M₂ f
map_id
X :=
ModuleCat.MonoidalCategory.tensor_ext
(by
intro m₁ m₂
dsimp [tensorObjMap]
simp
rfl) -- `ModuleCat.restrictScalarsId'App_inv_apply` doesn't get picked up due to type mismatch
map_comp f
g :=
ModuleCat.MonoidalCategory.tensor_ext
(by
intro m₁ m₂
dsimp [tensorObjMap]
simp)
