English
For a finite index set I, the infimum of kernels indexed by I equals the supremum of ranges indexed by I under a partition with J.
Русский
Для конечного множества индексов I инфимум ядер по I равен супремум образов по I при разбиении на J.
LaTeX
$$$\\bigwedge_{i\\in I} \\ker(\\mathrm{proj}_i) = \\bigwedge_{i\\in J} \\mathrm{range}(\\text{single } i).$$$
Lean4
theorem iSup_range_single_eq_iInf_ker_proj {I J : Set ι} (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J)
(hI : Set.Finite I) : ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) :=
by
refine le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
refine le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)
rw [Set.Finite.mem_toFinset]
