Lean4
/-- **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''`. -/
theorem goursat :
∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R M') (N'' : Submodule R N') (e :
(M' ⧸ M'') ≃ₗ[R] N' ⧸ N''), L = (e.graph.comap <| M''.mkQ.prodMap N''.mkQ).map (M'.subtype.prodMap N'.subtype) :=
by
let M' := L.map (LinearMap.fst ..)
let N' := L.map (LinearMap.snd ..)
let P : L →ₗ[R] M' := (LinearMap.fst ..).submoduleMap L
let Q : L →ₗ[R] N' := (LinearMap.snd ..).submoduleMap L
let L' : Submodule R (M' × N') := LinearMap.range (P.prod Q)
have hL₁' : Surjective (Prod.fst ∘ L'.subtype) :=
by
simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
simpa only [L', ← LinearMap.range_comp, fst_prod, range_eq_top] using (LinearMap.fst ..).submoduleMap_surjective L
have hL₂' : Surjective (Prod.snd ∘ L'.subtype) :=
by
simp only [← coe_snd (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
simpa only [L', ← LinearMap.range_comp, snd_prod, range_eq_top] using (LinearMap.snd ..).submoduleMap_surjective L
obtain ⟨e, he⟩ := goursat_surjective hL₁' hL₂'
use M', N', L'.goursatFst, L'.goursatSnd, e
rw [← he]
simp only [LinearMap.range_comp, Submodule.range_subtype, L']
rw [comap_map_eq_self]
· ext ⟨m, n⟩
constructor
· intro hmn
simp only [mem_map, LinearMap.mem_range, prod_apply, Subtype.exists, Prod.exists, coe_prodMap, coe_subtype,
Prod.map_apply, Prod.mk.injEq, exists_and_right, exists_eq_right_right, exists_eq_right, M', N', fst_apply,
snd_apply]
exact ⟨⟨n, hmn⟩, ⟨m, hmn⟩, ⟨m, n, hmn, rfl⟩⟩
· simp only [mem_map, LinearMap.mem_range, prod_apply, Subtype.exists, Prod.exists, coe_prodMap, coe_subtype,
Prod.map_apply, Prod.mk.injEq, exists_and_right, exists_eq_right_right, exists_eq_right, forall_exists_index,
Pi.prod]
rintro hm hn m₁ n₁ hm₁n₁ ⟨hP, hQ⟩
simp only [Subtype.ext_iff] at hP hQ
rwa [← hP, ← hQ]
· convert goursatFst_prod_goursatSnd_le (range <| P.prod Q)
ext ⟨m, n⟩
simp_rw [mem_ker, coe_prodMap, Prod.map_apply, Submodule.mem_prod, Prod.zero_eq_mk, Prod.ext_iff, ← mem_ker,
ker_mkQ]
