exists_range_eq_graph — Mathlib

English

Under surjectivity of the projection maps onto both factors and a compatibility condition, the image of a product map f is the graph of a linear isomorphism e: H ≃ I.

Русский

При условии сюръективности проекций на обе величины и совместимости, образ отображения f равен графику линейного изоморфизма e: H ≃ I.

LaTeX

$$$\\exists e:\\, H \\simeq I,\\quad \\operatorname{range} f = e^{\\!\\mathrm{toLinearMap}}\\;\\text{graph}$$$

Lean4

/-- **Vertical line test** for linear maps.

Let `f : G → H × I` be a linear (or semilinear) map to a product. Assume that `f` is surjective on
the first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at
most once. Then the image of `f` is the graph of some linear map `f' : H → I`. -/
theorem exists_range_eq_graph {f : G →ₛₗ[σ] H × I} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →ₗ[S] I, LinearMap.range f = LinearMap.graph f' :=
  by
  obtain ⟨f', hf'⟩ := AddMonoidHom.exists_mrange_eq_mgraph (G := G) (H := H) (I := I) (f := f) hf₁ hf
  simp only [SetLike.ext_iff, AddMonoidHom.mem_mrange, AddMonoidHom.coe_coe, AddMonoidHom.mem_mgraph] at hf'
  use {
      toFun := f'.toFun
      map_add' := f'.map_add'
      map_smul' := by
        intro s h
        simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
        refine (hf' (s • h, _)).mp ?_
        rw [← Prod.smul_mk, ← LinearMap.mem_range]
        apply Submodule.smul_mem
        rw [LinearMap.mem_range, hf'] }
  ext x
  simpa only [mem_range, Eq.comm, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_graph_iff, coe_mk,
    AddHom.coe_mk, AddMonoidHom.coe_coe, Set.mem_range] using hf' x

Похожие утверждения