English
Let f : α → α′ and let s ⊆ α satisfy: for all a ∈ s and b ∈ s, f a = f b implies a = b. Then the submodule of finsupps supported on s and the kernel of the linear map lmapDomain M R f have trivial intersection; i.e., they are disjoint.
Русский
Пусть f : α → α′ и s ⊆ α удовлетворяют: для всех a ∈ s и b ∈ s, f a = f b влечёт a = b. Тогда пересечение подмодуля FinSupp, состоящего из функций с опорой в s, и ядра линейного отображения lmapDomain(M, R, f) тривиально; то есть они попарно непересекаются.
LaTeX
$$$\\operatorname{Disjoint}\\left(\\operatorname{supported} M R s, \\ker\\bigl(\\mathrm{lmapDomain} M R f\\bigr)\\right)$$$
Lean4
theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) :
Disjoint (supported M R s) (ker (lmapDomain M R f)) :=
by
rw [disjoint_iff_inf_le]
rintro l ⟨h₁, h₂⟩
rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂
simp only [mem_bot]; ext x
haveI := Classical.decPred fun x => x ∈ s
by_cases xs : x ∈ s
· have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 :=
by
rw [h₂]
rfl
rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
· simpa
· intro y hy xy
simp only [SetLike.mem_coe, mem_supported, subset_def, Finset.mem_coe, mem_support_iff] at h₁
simp [mt (H _ (h₁ _ hy) _ xs) xy]
· simp +contextual
· by_contra h
exact xs (h₁ <| Finsupp.mem_support_iff.2 h)
