of_isLocalizedModule — Mathlib

English

If f is a localized module map and reg is IsSMulRegular on K, then the base-changed map satisfies IsSMulRegular on M via algebraMap.

Русский

Если f локализованный модульный гомоморфизм и reg является IsSMulRegular на K, то после изменения базы условие IsSMulRegular переносится на M через алгебраическое отображение.

LaTeX

$$$IsSMulRegular(K,x) \\Rightarrow IsSMulRegular(M, f(x))$$$

Lean4

theorem of_isLocalizedModule {K : Type*} [AddCommMonoid K] [Module R K] (f : K →ₗ[R] M) [IsLocalizedModule p f] {x : R}
    (reg : IsSMulRegular K x) : IsSMulRegular M (algebraMap R S x) :=
  have : Module.Flat R S := IsLocalization.flat S p
  reg.of_flat_of_isBaseChange (IsLocalizedModule.isBaseChange p S f)

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