instHMulAwayCoeRingHomAlgebraMap_1

English

If S1,S2,T are rings with R-algebra structures and IsLocalization.Away assumptions, localization away from x in S1 commutes with localization away from y in S2, i.e., IsLocalization.Away (algebraMap_R S1 y) T.

Русский

Если S1, S2, T — кольца с структурами R-алгебр и выполнены условия локализации away от x и away от y, то локализация away от y в T совпадает с локализацией away от x в S1, т.е. IsLocalization.Away (algebraMap_R S1 y) T.

LaTeX

$$$IsLocalization.Away (algebraMap_R S1 y) T$$$

Lean4

/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `x * y`. -/
instance (x y : R) [IsLocalization.Away x S] : IsLocalization.Away (x * y) (Localization.Away (algebraMap R S y)) :=
  IsLocalization.Away.mul' S (Localization.Away (algebraMap R S y)) _ _

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