English
For a submodule L ⊆ M × N, the first Goursat component viewed as a submodule of M matches the corresponding projection of L to M.
Русский
Для подмодуля L ⊆ M × N первая компонента Гурсата, рассматриваемая как подмодуль в M, совпадает с проекцией L на M.
LaTeX
$$$ (goursatFst\; L).toAddSubgroup = L.toAddSubgroup.goursatFst $$$
Lean4
/-- For `L` a submodule of `M × N`, `L.goursatFst` is the kernel of the projection map `L → N`,
considered as a submodule of `M`.
This is the first submodule appearing in Goursat's lemma. See `Subgroup.goursat`. -/
def goursatFst : Submodule R M :=
(LinearMap.ker <| (LinearMap.snd R M N).comp L.subtype).map ((LinearMap.fst R M N).comp L.subtype)
