bijective — Mathlib

English

The inverse of algEquivOfAlgEquiv corresponds to the reversed roles of the localizations S and Q.

Русский

Обратное отображение algEquivOfAlgEquiv соответствует обратным ролям локализаций S и Q.

LaTeX

$$$(\\mathrm{algEquivOfAlgEquiv}\\;S\\;Q\\;h\\;H)^{-1} = \\mathrm{algEquivOfAlgEquiv}\\;Q\\;S\\;h^{\\mathrm{symm}}\\;H^{\\mathrm{symm}}$$$

Lean4

protected theorem bijective (f : S →+* Q) (hf : f.comp (algebraMap R S) = algebraMap R Q) : Function.Bijective f :=
  (show f = IsLocalization.algEquiv M S Q by apply IsLocalization.ringHom_ext M; rw [hf]; ext; simp) ▸
    (IsLocalization.algEquiv M S Q).toEquiv.bijective

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