English
If I and J are disjoint index sets with a cover of the universe, there is a linear equivalence between the infimum of the kernels ker(proj_i) and a product indexed by I.
Русский
Если I и J — дизъюнкты, покрывающие всю совокупность индексов, существует линейное эквивалентное отображение между инфIMUM ядер ker(proj_i) и произведением по I.
LaTeX
$$$\\text{iInfKerProjEquiv} \\; (I,J,hd,hu):\\; (⨅ i ∈ J, ker (proj_i)) \\simeq_ℝ (i : I) → φ_i.$$$
Lean4
/-- If `I` and `J` are disjoint index sets, the product of the kernels of the `J`th projections of
`φ` is linearly equivalent to the product over `I`. -/
def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) :
(⨅ i ∈ J, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) : Submodule R ((i : ι) → φ i)) ≃ₗ[R] (i : I) → φ i :=
by
refine
LinearEquiv.ofLinear (pi fun i => (proj (i : ι)).comp (Submodule.subtype _))
(codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) ?_) ?_ ?_
· intro b
simp only [mem_iInf, mem_ker, proj_apply, pi_apply]
intro j hjJ
have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
rw [dif_neg this, zero_apply]
· simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
ext b ⟨j, hj⟩
simp only [dif_pos, LinearMap.coe_proj, LinearMap.pi_apply]
rfl
· ext1 ⟨b, hb⟩
apply Subtype.ext
ext j
have hb : ∀ i ∈ J, b i = 0 := by simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
simp only [comp_apply, pi_apply, id_apply, codRestrict_apply]
split_ifs with h
· rfl
· exact (hb _ <| (hu trivial).resolve_left h).symm
