submodule_map_involute_eq_comap — Mathlib

English

For any Q and any submodule p of CliffordAlgebra Q, the image of p under involute equals the comap of p under involute.

Русский

Для любого Q и подмодуля p клиффордовой алгебры, образ p через involute равен сопряжению p через involute.

LaTeX

$$$ p.map (involute.toLinearMap) = p.comap (involute.toLinearMap) $$$

Lean4

theorem submodule_map_involute_eq_comap (p : Submodule R (CliffordAlgebra Q)) :
    p.map (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap =
      p.comap (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap :=
  Submodule.map_equiv_eq_comap_symm involuteEquiv.toLinearEquiv _

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