English
Let s be a finite set of indices, with ideals f(i) for i ∈ s. If i ∈ s, each f(i) is primary, and the radicals rad(f(i)) are all equal to rad(f(i0)) for some i0 ∈ s, then inf_{i∈s} f(i) is primary.
Русский
Пусть s — конечный набор индексов; f(i) — идеалы; если i0 ∈ s, все f(i) примарны и rad(f(i)) совпадают, то inf_{i∈s} f(i) примарен.
LaTeX
$$$\\text{If } i \\in s,\\forall i\\in s:\\; f(i) \\text{ IsPrimary} \\,\\land \\\\ \\forall i\\in s:\\; \\operatorname{rad}(f(i)) = \\operatorname{rad}(f(i_0)) \\Rightarrow \\bigwedge_{i\\in s} f(i) \\text{ IsPrimary}.$$$
Lean4
theorem isPrimary_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
(hs : ∀ ⦃y⦄, y ∈ s → (f y).IsPrimary) (hs' : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) : IsPrimary (s.inf f) :=
by
classical
induction s using Finset.induction_on generalizing i with
| empty => simp at hi
| insert a s ha IH =>
rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
· simp only [insert_empty_eq, mem_singleton] at hi
simpa [hi] using hs
simp only [inf_insert]
have H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical :=
by
intro x hx
rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
refine isPrimary_inf (hs (by simp)) (IH hy ?_ H) ?_
· intro x hx
exact hs (by simp [hx])
· rw [radical_finset_inf hy H, hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
