submoduleComap_surjective_of_surjective

English

If f is surjective, then f.submoduleComap q is surjective onto q.

Русский

Если f сюръективно отображает, то f.submoduleComap q сюръективно отображает на q.

LaTeX

$$$ Surjective (f.submoduleComap q) $$$

Lean4

theorem submoduleComap_surjective_of_surjective (f : M →ₗ[R] M₁) (q : Submodule R M₁) (hf : Surjective f) :
    Surjective (f.submoduleComap q) := fun y ↦ by
  obtain ⟨x, hx⟩ := hf y
  use ⟨x, Submodule.mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

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