mapPiLocalization_bijective — Mathlib

English

If f is bijective, then mapPiLocalization is bijective.

Русский

Если отображение биективно, то отображение PiLocalization биективно.

LaTeX

$$$\mathrm{mapPiLocalization}\ f \text{ is bijective given bijective } f$$$

Lean4

theorem mapPiLocalization_bijective (hf : Function.Bijective f) : Function.Bijective (mapPiLocalization f) :=
  by
  let f := RingEquiv.ofBijective f hf
  let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_
  · exact e.bijective
  · rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]
  · rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

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