equivQuotTensor_naturality_mk — Mathlib

English

Natural equality for mk x under the quotient–tensor equivalence with respect to f.

Русский

Ещё одна натуральная равенство для mk x относительно эквивалентности квотирования и тензора по f.

LaTeX

$$$$ EquivQuotTensor(r,M')( [x] ) = (f\otimes 1) (EquivQuotTensor(r,M)([x])) $$$$

Lean4

theorem equivQuotTensor_naturality_mk (f : M →ₗ[R] M') (x : M) :
    equivQuotTensor r M' (map r f (Submodule.Quotient.mk x)) =
      f.lTensor (R ⧸ Ideal.span { r }) (equivQuotTensor r M (Submodule.Quotient.mk x)) :=
  (LinearMap.lTensor_tmul (R ⧸ Ideal.span { r }) f 1 x).symm

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