English
From a pairwise radical-decomposed primary decomposition, one can extract a minimal decomposition whose components are pairwise nonredundant.
Русский
Из разложения в первичные с попарно различными радикалами можно выбрать минимальное разложение, не содержащее избыточных членах.
LaTeX
$$∃ t, t.inf id = I ∧ ∀ J ∈ t, J.IsPrimary ∧ (t : Set).Pairwise (≠ on radical) ∧ ∀ J ∈ t, ¬(t.erase J).inf id ≤ J$$
Lean4
theorem isPrimary_decomposition_pairwise_ne_radical {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) :=
by
classical
refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩
· rw [← hs]
refine le_antisymm ?_ ?_ <;> intro x hx
· simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter,
id_eq, and_imp] at hx ⊢
intro J hJ
exact hx J hJ J hJ rfl
· simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply,
Finset.mem_filter, and_imp] at hx ⊢
intro J _ K hK _
exact hx K hK
· simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro J hJ
refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp)
· simp [hJ]
· simp only [Finset.mem_filter, id_eq, and_imp]
intro y hy
simp [hs' hy]
· intro I hI J hJ hIJ
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
obtain ⟨I', hI', hI⟩ := hI
obtain ⟨J', hJ', hJ⟩ := hJ
simp only [Function.onFun, ne_eq]
contrapose! hIJ
suffices I'.radical = J'.radical by rw [← hI, ← hJ, this]
· rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]
