equivTensorQuot_naturality_mk — Mathlib

English

Naturality of the equivalence between M and M′ via mk and tensoring by R/(r).

Русский

Естественная совместимость эквивалентности между QuotSMulTop и тензором с R/(r) через mk.

LaTeX

$$$$ EquivQuotTensor(r,M') \circ QuotSMulTop\_map f = (f\otimes 1) \circ EquivQuotTensor(r,M). $$$$

Lean4

theorem equivTensorQuot_naturality_mk (f : M →ₗ[R] M') (x : M) :
    equivTensorQuot r M' (map r f (Submodule.Quotient.mk x)) =
      f.rTensor (R ⧸ Ideal.span { r }) (equivTensorQuot r M (Submodule.Quotient.mk x)) :=
  (LinearMap.rTensor_tmul (R ⧸ Ideal.span { r }) f 1 x).symm

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