support_subset_preimage_comap — Mathlib

English

For an IsScalarTower R → A → M, the support over A is contained in the preimage of the support over R under the algebra map R → A.

Русский

Для тождества IsScalarTower R → A → M поддержка над A содержится в предобразе поддержки над R по отображению R → A.

LaTeX

$$$\\mathrm{Module.support}\\ A M \\subseteq \\mathrm{Preimage}(\\mathrm{algebraMap}\\ R A)^{-1} (\\mathrm{Module.support}\\ R M)$$$

Lean4

theorem support_subset_preimage_comap [IsScalarTower R A M] :
    Module.support A M ⊆ PrimeSpectrum.comap (algebraMap R A) ⁻¹' Module.support R M :=
  by
  intro x hx
  simp only [Set.mem_preimage, mem_support_iff', PrimeSpectrum.comap_asIdeal, Ideal.mem_comap, ne_eq,
    not_imp_not] at hx ⊢
  obtain ⟨m, hm⟩ := hx
  exact ⟨m, fun r e ↦ hm _ (by simpa)⟩

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