Theorems · Theorem · linear algebra

Submodule.exists_equiv_eq_graph

∀ {S : Type u_4} {H : Type u_6} {I : Type u_7} [inst : Semiring S] [inst_1 : AddCommMonoid H] [inst_2 : Module S H]
  [inst_3 : AddCommMonoid I] [inst_4 : Module S I] {G : Submodule S (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = (↑e).graph

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.

Defined in

Mathlib.LinearAlgebra.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule