English
Equality of the supremum of ranges of singles over I and the infimum of kernels over J holds under the stated disjointness and cover conditions.
Русский
Сохранение равенства между верхней границей образов одиночных отображений по I и нижней границей ядер по J при заданных условиях дизъюнктности и покрытия.
LaTeX
$$$⨆ i∈I,\\; \\mathrm{range}(\\text{single } i) = ⨅ i∈J, \\ker(\\mathrm{proj}_i).$$$
Lean4
theorem iInf_ker_proj_le_iSup_range_single {I : Finset ι} {J : Set ι} (hu : Set.univ ⊆ ↑I ∪ J) :
⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) ≤ ⨆ i ∈ I, range (single R φ i) :=
SetLike.le_def.2
(by
intro b hb
simp only [mem_iInf, mem_ker, proj_apply] at hb
rw [←
show (∑ i ∈ I, Pi.single i (b i)) = b by
ext i
rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
intro hiI
rw [Pi.single_eq_same]
exact hb _ ((hu trivial).resolve_left hiI)]
exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i))
