English
There is a canonical bilinear map that sends an element of M and a point of eqLocus f g to their tensor product in the target equalizer-locus, encapsulating the natural action of tensoring with M.
Русский
Существует каноническая билинейная отображение, которое отправляет элемент M и точку из eqLocus f g в их тензорный произведение в целевом равноположении, отображая естественное тензорное действие.
LaTeX
$$$\text{tensorEqLocusBil} : M \to_\text{S} (eqLocus\, f\, g) \to_\text{R} eqLocus( lTensor_S M f, lTensor_S M g )$$$
Lean4
/-- The bilinear map corresponding to `LinearMap.tensorEqLocus`. -/
def tensorEqLocusBil :
M →ₗ[S]
LinearMap.eqLocus f g →ₗ[R]
LinearMap.eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g)
where
toFun
m :=
{ toFun := fun a ↦ ⟨m ⊗ₜ a, by simp [show f a = g a from a.property]⟩
map_add' := fun x y ↦ by simp [tmul_add]
map_smul' := fun r x ↦ by simp }
map_add' x
y := by
ext
simp [add_tmul]
map_smul' r
x := by
ext
simp [smul_tmul']
