exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

English

In a Lasker ring, every ideal admits a minimal primary decomposition with pairwise distinct radical ideals.

Русский

В кольце Ласкера любое идеал обладает минимальным первичным разложением с попарно различными радикалами.

LaTeX

$$Ideal.IsLasker.minimal$$

Lean4

theorem exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition [DecidableEq (Ideal R)] {I : Ideal R}
    {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
    ∃ t : Finset (Ideal R),
      t.inf id = I ∧
        (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
          ((t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)) ∧ (∀ ⦃J⦄, J ∈ t → ¬(t.erase J).inf id ≤ J) :=
  by
  obtain ⟨t, ht, ht', ht''⟩ := isPrimary_decomposition_pairwise_ne_radical hs hs'
  obtain ⟨u, hut, hu, hu'⟩ := decomposition_erase_inf ht
  exact ⟨u, hu, fun _ hi ↦ ht' (hut hi), ht''.mono hut, hu'⟩

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