algEquivOfAlgEquiv — Mathlib

English

There is at most one algHom from S to Q compatible with localization data.

Русский

Существует не более одного алгеброгомоморфизма от S к Q совместимого с данными локализации.

LaTeX

$$$\\text{Bijective}(\\,\\text{AlgHom } S Q)\\Rightarrow$ uniqueness$$

Lean4

/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M`, `T` respectively,
an isomorphism `h : R ≃ₐ[A] P` such that `h(M) = T` induces an isomorphism of localizations
`S ≃ₐ[A] Q`. -/
@[simps!]
noncomputable def algEquivOfAlgEquiv : S ≃ₐ[A] Q
    where
  __ := ringEquivOfRingEquiv S Q h.toRingEquiv H
  commutes'
    _ := by dsimp;
    rw [IsScalarTower.algebraMap_apply A R S, map_eq, RingHom.coe_coe, AlgEquiv.commutes,
      IsScalarTower.algebraMap_apply A P Q]

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