localize_algebraMap — Mathlib

English

On elements coming from the ambient ring S, the localized Frobenius matches the action of φ; i.e., the localization interchanges with φ on base elements.

Русский

На элементы, приходящие из кольца S, локализованный Фробениус совпадает с действием φ; локализация допускает взаимодействие с φ на базовых элементах.

LaTeX

$$H.localize (algebraMap _ _ x) = algebraMap _ _ (φ x)$$

Lean4

@[simp]
theorem localize_algebraMap [Q.IsPrime] (x : S) : H.localize (algebraMap _ _ x) = algebraMap _ _ (φ x) :=
  Localization.localRingHom_to_map _ _ _ H.comap_eq.symm _

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