English
An orthogonal family with complete projections yields a direct sum decomposition of the ambient space into the subspaces V_i.
Русский
Ортогональная совокупность с полными проекции даёт разложение пространства на частичные подплощины V_i в прямой сумме.
LaTeX
$$$\\text{OrthogonalFamily.decomposition } V$$$
Lean4
/-- If a family of submodules is orthogonal and they span the whole space, then the orthogonal
projection provides a means to decompose the space into its submodules.
The projection function is `decompose V x i = (V i).orthogonalProjection x`.
See note [reducible non-instances]. -/
noncomputable abbrev decomposition [DecidableEq ι] [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ i, CompleteSpace (V i)]
(hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (h : iSup V = ⊤) : DirectSum.Decomposition V
where
decompose' x := DFinsupp.equivFunOnFintype.symm fun i => (V i).orthogonalProjection x
left_inv
x := by
dsimp only
letI := fun i => Classical.decEq (V i)
rw [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid, DFinsupp.liftAddHom_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [DFinsupp.sumAddHom_apply]; rw [DFinsupp.sum_eq_sum_fintype]
· simp_rw [Equiv.apply_symm_apply, AddSubmonoidClass.coe_subtype]
exact hV.sum_projection_of_mem_iSup _ ((h.ge :) Submodule.mem_top)
· intro i
exact map_zero _
right_inv
x := by
dsimp only
simp_rw [hV.projection_directSum_coeAddHom, DFinsupp.equivFunOnFintype_symm_coe]
