English
For an orthogonal family V, the ith coordinate under the direct sum coeAddMonoidHom equals the orthogonal projection of the ith component.
Русский
Для ортогональной семьи V i-й координатный компонент равен ортогональной проекции i-й компоненты.
LaTeX
$$$(V_i)^{\\perp}\\mathrm{projection}(DirectSum) = x_i$$$
Lean4
/-- If a family of submodules is orthogonal, then the `orthogonalProjection` on a direct sum
is just the coefficient of that direct sum. -/
theorem projection_directSum_coeAddHom [DecidableEq ι] {V : ι → Submodule 𝕜 E}
(hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (x : ⨁ i, V i) (i : ι) [CompleteSpace (V i)] :
(V i).orthogonalProjection (DirectSum.coeAddMonoidHom V x) = x i := by
induction x using DirectSum.induction_on with
| zero => simp
| of j
x =>
simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
-- Need to unfold `DirectSum` to see through the defeq abuse.
DirectSum, DFinsupp.singleAddHom_apply]
obtain rfl | hij := Decidable.eq_or_ne i j
· rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
· rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, DFinsupp.single_eq_of_ne hij]
exact hV.isOrtho hij.symm x.prop
| add x y hx hy =>
simp_rw [map_add]
exact congr_arg₂ (· + ·) hx hy
