Theorems · Theorem · linear algebra

LinearMap.exists_linearEquiv_eq_graph

∀ {R : Type u_3} {S : Type u_4} {G : Type u_5} {H : Type u_6} {I : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : R →+* S} [inst_2 : RingHomSurjective σ] [inst_3 : AddCommMonoid G] [inst_4 : Module R G]
  [inst_5 : AddCommMonoid H] [inst_6 : Module S H] [inst_7 : AddCommMonoid I] [inst_8 : Module S I]
  {f : G →ₛₗ[σ] H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, f.range = (↑e).graph

Line test for module isomorphisms. Let f : G → H × I be a linear (or semilinear) map to a product of modules. Assume that f is surjective onto both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some module isomorphism f' : H ≃ I.

Defined in

Mathlib.LinearAlgebra.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringSemiringRingHomSurjectiveAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModule