Theorems · Theorem · commutative algebra

Submodule.goursat_surjective

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Submodule R (M × N)},
  Function.Surjective (Prod.fst ∘ ⇑L.subtype) →
    Function.Surjective (Prod.snd ∘ ⇑L.subtype) →
      ∃ e, (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range = (↑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.

Defined in

Mathlib.LinearAlgebra.Goursat

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModule