support_quotient — Mathlib

English

For any ideal I, the support of the quotient M/IM equals the intersection of the support of M with the zero locus of I: Supp_R(M/IM) = Supp_R(M) ∩ V(I).

Русский

Для любого идеала I выполнено: Supp_R(M/IM) = Supp_R(M) ∩ V(I).

LaTeX

$$$\\\\mathrm{Supp}_R\\\\bigl(M / I M\\\\bigr) = \\mathrm{Supp}_R(M) \\cap \\mathrm{V}(I)$$$

Lean4

/-- `Supp(M/IM) = Supp(M) ∩ Z(I)`. -/
@[stacks 00L3 "(1)"]
theorem support_quotient (I : Ideal R) : support R (M ⧸ (I • ⊤ : Submodule R M)) = support R M ∩ zeroLocus I :=
  by
  apply subset_antisymm
  · refine Set.subset_inter ?_ ?_
    · exact Module.support_subset_of_surjective _ (Submodule.mkQ_surjective _)
    · rw [support_eq_zeroLocus]
      apply PrimeSpectrum.zeroLocus_anti_mono_ideal
      rw [Submodule.annihilator_quotient]
      exact fun x hx ↦ Submodule.mem_colon.mpr fun p ↦ Submodule.smul_mem_smul hx
  · rintro p ⟨hp₁, hp₂⟩
    rw [Module.mem_support_iff] at hp₁ ⊢
    let Rₚ := Localization.AtPrime p.asIdeal
    let Mₚ := LocalizedModule p.asIdeal.primeCompl M
    set Mₚ' := LocalizedModule p.asIdeal.primeCompl (M ⧸ (I • ⊤ : Submodule R M))
    let Mₚ'' := Mₚ ⧸ I.map (algebraMap R Rₚ) • (⊤ : Submodule Rₚ Mₚ)
    let e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
      (localizedQuotientEquiv _ _).symm ≪≫ₗ
        Submodule.quotEquivOfEq _ _
          (by rw [Submodule.localized, Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top])
    have : Nontrivial Mₚ'' := by
      apply Submodule.Quotient.nontrivial_of_lt_top
      rw [lt_top_iff_ne_top, ne_comm]
      apply Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
      refine trans ?_ (IsLocalRing.maximalIdeal_le_jacobson _)
      rw [← Localization.AtPrime.map_eq_maximalIdeal]
      exact Ideal.map_mono hp₂
    exact e.nontrivial

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