comap_annihilator — Mathlib

English

The annihilator of M as an R-module, pulled back along an algebra map R0 → R, equals the annihilator of M as an R0-module.

Русский

Аннигилятор M как R-модуля, вытянутый обратно по несущему алгебра-отображению R0 → R, совпадает с аннигилятором M как R0-модуля.

LaTeX

$$$ (\\operatorname{Ann}_R(M))^{\\mathrm{comap}(\\operatorname{algebraMap}_{R_0 \\to R})} = \\operatorname{Ann}_{R_0}(M). $$$

Lean4

theorem comap_annihilator {R₀} [CommSemiring R₀] [Module R₀ M] [Algebra R₀ R] [IsScalarTower R₀ R M] :
    (Module.annihilator R M).comap (algebraMap R₀ R) = Module.annihilator R₀ M :=
  by
  ext x
  simp [mem_annihilator]

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