English
If a linear map f: G → σ(H × I) satisfies surjectivity on the first coordinate and a matching condition across the components, then there exists f' with range f = graph f'.
Русский
Пусть линейное отображение f: G → σ(H × I) удовлетворяет сюръективности по первой координате и условию согласованности; существует f' такой, что range f = graph f'.
LaTeX
$$$\\exists f': H \\to I,\\; \\operatorname{range} f = \\operatorname{graph}(f')$$$
Lean4
/-- **Vertical line test** for linear maps.
Let `G ≤ H × I` be a submodule of a product of modules. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some linear map `f : H →ₗ[R] I`. -/
theorem exists_eq_graph {G : Submodule S (H × I)} (hf₁ : Bijective (Prod.fst ∘ G.subtype)) :
∃ f : H →ₗ[S] I, G = LinearMap.graph f := by
simpa only [range_subtype] using
LinearMap.exists_range_eq_graph hf₁.surjective (fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hf₁.injective h))
