decomposeLinearEquiv_symm_comp_lof

English

The symm of the isomorphism composes correctly with the lof maps on components, yielding the expected componentwise subtype maps. (Technical: compatibility with lof).

Русский

Обратный композит разложения согласуется с вложениями каждой компоненты, давая ожидаемые отображения подмножества компонент.

LaTeX

$$$ (\operatorname{decomposeLinearEquiv} \mathcal{M})^{\mathrm{symm}}(\operatorname{lof} \! R \! ι (\mathcal{M} \cdot) i) = (\mathcal{M} i).\text{subtype}$$$

Lean4

@[simp]
theorem decomposeLinearEquiv_symm_comp_lof (i : ι) : (decomposeLinearEquiv ℳ).symm ∘ₗ lof R ι (ℳ ·) i = (ℳ i).subtype :=
  LinearMap.ext <| decompose_symm_of _

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