English
A Frobenius element at Q restricts to an endomorphism of the localized ring S_Q; in particular, the Frobenius extends to the localization at the prime Q.
Русский
Элемент Фробениуса по Q ограничивает отображение на локализацию S_Q; то есть Фробениус продолжается к локализации в точке Q.
LaTeX
$$There is an algebra endomorphism $H.localize: R\text{-algebra} Localization.AtPrime(Q) \to Localization.AtPrime(Q)$$$
Lean4
/-- A Frobenius element at `Q` restricts to an automorphism of `S_Q`. -/
noncomputable def localize [Q.IsPrime] : Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q
where
toRingHom := Localization.localRingHom _ _ φ H.comap_eq.symm
commutes' x := by simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime Q), Localization.localRingHom_to_map]
