decomposeProdAdjoint — Mathlib

English

The elements of a star module split into a pair of self-adjoint and skew-adjoint parts, forming a linear equivalence A ≃ selfAdjoint A × skewAdjoint A.

Русский

Элементы звёздового модуля разлагаются на пару самосопряжённых и космодружённых частей, образуя линейное взаимодополнение A ≃ selfAdjoint A × skewAdjoint A.

LaTeX

$$$A \simeq_{\mathrm{lin}} \mathrm{selfAdjoint} A \times \mathrm{skewAdjoint} A$$$

Lean4

/-- The decomposition of elements of a star module into their self- and skew-adjoint parts,
as a linear equivalence. -/
@[simps!]
def decomposeProdAdjoint : A ≃ₗ[R] selfAdjoint A × skewAdjoint A :=
  by
  refine
    LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R))
      (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype) ?_
      (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)
        -- Note: with https://github.com/leanprover-community/mathlib4/pull/6965 `Submodule.coe_subtype` doesn't fire in `dsimp` or `simp`

  ext x <;> dsimp <;> erw [Submodule.coe_subtype, Submodule.coe_subtype] <;> simp

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