English
Goursat's lemma for modules: if two projections from a submodule G ⊆ H × I are bijective, then G is the graph of a linear isomorphism H ≃ I.
Русский
Лемма Гурсота для модулей: если две проекции из подпроизведения G ⊆ H × I биективны, то G является графиком линейного изоморфизма H ≃ I.
LaTeX
$$$\\exists e:\\, H \\simeq I,\\; G = e^{\\mathrm{toLinearMap}}\\;\\text{graph}$$$
Lean4
/-- **Goursat's lemma** for module isomorphisms.
Let `G ≤ H × I` be a submodule of a product of modules. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some module isomorphism `f : H ≃ I`. -/
theorem exists_equiv_eq_graph {G : Submodule S (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype))
(hG₂ : Bijective (Prod.snd ∘ G.subtype)) : ∃ e : H ≃ₗ[S] I, G = e.toLinearMap.graph := by
simpa only [range_subtype] using
LinearMap.exists_linearEquiv_eq_graph hG₁.surjective hG₂.surjective fun _ _ ↦
hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm
