mulMap_op — Mathlib

English

A technical identity expressing mulMap under opposites, with opposite linear equivalences and a commutation correction.

Русский

Техническое тождество для mulMap в противоположных структурах, с учетом противоположного линейного эквивалентного отображения и исправления коммутации.

LaTeX

$$$mulMap (equivOpposite.symm (MulOpposite.op M)) (equivOpposite.symm (MulOpposite.op N)) = (MulOpposite.opLinearEquiv R).toLinearMap \circ mulMap N M \circ (TensorProduct.congr (LinearEquiv.ofSubmodule' (MulOpposite.opLinearEquiv R).symm M) (LinearEquiv.ofSubmodule' (MulOpposite.opLinearEquiv R).symm N) \\n ≪≫_l TensorProduct.comm R M N).toLinearMap$$$

Lean4

theorem mulMap_op :
    mulMap (equivOpposite.symm (MulOpposite.op M)) (equivOpposite.symm (MulOpposite.op N)) =
      (MulOpposite.opLinearEquiv R).toLinearMap ∘ₗ
        mulMap N M ∘ₗ
          (TensorProduct.congr (LinearEquiv.ofSubmodule' (MulOpposite.opLinearEquiv R).symm M)
                (LinearEquiv.ofSubmodule' (MulOpposite.opLinearEquiv R).symm N) ≪≫ₗ
              TensorProduct.comm R M N).toLinearMap :=
  TensorProduct.ext' fun _ _ ↦ rfl

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