mapₐ_surjective_of_surjective — Mathlib

English

If f: A → B is surjective, then the induced map mapₐ is surjective.

Русский

Если f: A → B сюръективно, тогда mapₐ сюръективно.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow \\text{Surjective}(\\text{map}_{A_p,B_p,f})$$$

Lean4

theorem mapₐ_surjective_of_surjective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Surjective f) :
    Function.Surjective (mapₐ Aₚ Bₚ f a) :=
  have : IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ :=
    by
    simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]
    infer_instance
  IsLocalization.map_surjective_of_surjective _ _ _ hf

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