English
Localization is preserved under the inverse isomorphism.
Русский
Локализация сохраняется под обратным изоморфизмом.
LaTeX
$$$ f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k $$$
Lean4
/-- Given a surjective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is surjective.
-/
@[to_additive /-- Given a surjective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is surjective. -/
]
theorem map_surjective_of_surjective (hg : Surjective g) (k : LocalizationMap (S.map g) Q) :
Surjective (map f (apply_coe_mem_map g S) k) := fun z ↦
by
obtain ⟨y, ⟨y', s, hs, rfl⟩, rfl⟩ := k.mk'_surjective z
obtain ⟨x, rfl⟩ := hg y
use f.mk' x ⟨s, hs⟩
rw [map_mk']
