The splitting along a complement and the horizontal subspace #
Mathlib's Submodule.prodEquivOfIsCompl identifies p × q with E when q is a complement of
p. This file records that it carries the horizontal subspace of p × q, the kernel of the second
projection, onto p.
Main results #
Submodule.map_ker_snd_prodEquivOfIsCompl: the splitting carries the kernel of the second projection ontop.
theorem
Submodule.map_ker_snd_prodEquivOfIsCompl
{R : Type u_1}
{E : Type u_2}
[Ring R]
[AddCommGroup E]
[Module R E]
(p q : Submodule R E)
(h : IsCompl p q)
:
The splitting of E along a complement of p carries the kernel of the second projection of
p × q onto p.