dual_rTensor_conj_homEquiv — Mathlib

English

Same natural compatibility as in item 18946; the statement is the equality of linear maps expressing the commutativity of the dualization with rTensor under homEquiv.

Русский

Та же естественная совместимость, что и в пункте 18946; равенство линейных отображений, выражающее совместимость дуализации с rTensor через homEquiv.

LaTeX

$$$\mathrm{homEquiv}^{-1} \circ (\mathrm{dual}(f \otimes B)) \circ \mathrm{homEquiv} = f \lcomp _{R} \; $$$

Lean4

theorem dual_rTensor_conj_homEquiv (f : A →ₗ[R] A') :
    homEquiv.symm.toLinearMap ∘ₗ dual (f.rTensor B) ∘ₗ homEquiv.toLinearMap = f.lcomp R _ :=
  rfl

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