Goursat's lemma for submodules

Let M, N be modules over a ring R. If L is a submodule of M × N which projects fully on to both factors, then there exist submodules M' ≤ M and N' ≤ N such that M' × N' ≤ L and the image of L in (M ⧸ M') × (N ⧸ N') is the graph of an isomorphism M ⧸ M' ≃ₗ[R] N ⧸ N'. Equivalently, L is equal to the preimage in M × N of the graph of this isomorphism M ⧸ M' ≃ₗ[R] N ⧸ N'.

M' and N' can be explicitly constructed as Submodule.goursatFst L and Submodule.goursatSnd L respectively.

def Submodule.goursatFst {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (L : Submodule R (M × N)) : Submodule R M

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.

Equations

• L.goursatFst = Submodule.map (LinearMap.fst R M N ∘ₗ L.subtype) (LinearMap.ker (LinearMap.snd R M N ∘ₗ L.subtype))

def Submodule.goursatSnd {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (L : Submodule R (M × N)) : Submodule R N

For L a subgroup of M × N, L.goursatSnd is the kernel of the projection map L → M, considered as a subgroup of N.

This is the second subgroup appearing in Goursat's lemma. See Subgroup.goursat.

Equations

• L.goursatSnd = Submodule.map (LinearMap.snd R M N ∘ₗ L.subtype) (LinearMap.ker (LinearMap.fst R M N ∘ₗ L.subtype))

theorem Submodule.goursatFst_toAddSubgroup {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {L : Submodule R (M × N)} : L.goursatFst.toAddSubgroup = L.toAddSubgroup.goursatFst

theorem Submodule.goursatSnd_toAddSubgroup {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {L : Submodule R (M × N)} : L.goursatSnd.toAddSubgroup = L.toAddSubgroup.goursatSnd

theorem Submodule.goursatFst_prod_goursatSnd_le {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (L : Submodule R (M × N)) : L.goursatFst.prod L.goursatSnd ≤ L

theorem Submodule.goursat_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {L : Submodule R (M × N)} (hL₁ : Function.Surjective (Prod.fst ∘ ⇑L.subtype)) (hL₂ : Function.Surjective (Prod.snd ∘ ⇑L.subtype)) : ∃ (e : (M ⧸ L.goursatFst) ≃ₗ[R] N ⧸ L.goursatSnd), LinearMap.range (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype) = (↑e).graph

Goursat's lemma for a submodule of a product with surjective projections.

If L is a submodule of M × N which projects fully on both factors, then there exist submodules M' ≤ M and N' ≤ N such that M' × N' ≤ L and the image of L in (M ⧸ M') × (N ⧸ N') is the graph of an isomorphism of R-modules (M ⧸ M') ≃ (N ⧸ N').

M and N can be explicitly constructed as L.goursatFst and L.goursatSnd respectively.

theorem Submodule.goursat {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {L : Submodule R (M × N)} : ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R ↥M') (N'' : Submodule R ↥N') (e : (↥M' ⧸ M'') ≃ₗ[R] ↥N' ⧸ N''), L = Submodule.map (M'.subtype.prodMap N'.subtype) (Submodule.comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Goursat's lemma for an arbitrary submodule of a product.

If L is a submodule of M × N, then there exist submodules M'' ≤ M' ≤ M and N'' ≤ N' ≤ N such that L ≤ M' × N', and L is (the image in M × N of) the preimage of the graph of an R-linear isomorphism M' ⧸ M'' ≃ N' ⧸ N''.