map_surjective — Mathlib

English

Exactness is preserved under QuotSMulTop.map provided appropriate exact sequences.

Русский

Точность сохраняется под QuotSMulTop.map при сочетании с точными последовательностями.

LaTeX

$$$$ map\_r f \;\text{ and } \; map\_r g \text{ form an exact ladder under appropriate hypotheses.} $$$$

Lean4

theorem map_surjective {f : M →ₗ[R] M'} (hf : Surjective f) : Surjective (map r f) :=
  have H₁ := (mkQ_surjective (r • ⊤ : Submodule R M')).comp hf
  @Surjective.of_comp _ _ _ _ (mkQ (r • ⊤ : Submodule R M)) <| by
    rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]

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