English
The family of submodules given by the Archimedean strata is iSup-independent: their pairwise suprema intersect trivially in a strong sense.
Русский
Семейство подмодулей, заданных слоями Архимедова типа, образует iSup-независимое семейство: их попарные наибольшие суммы имеют тривиальные общие части.
LaTeX
$$iSupIndep u.stratum$$
Lean4
theorem iSupIndep_stratum : iSupIndep u.stratum := by
intro c
rw [Submodule.disjoint_def']
intro a ha b hb hab
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb
obtain hf' := congrArg ArchimedeanClass.mk hf
contrapose! hf' with h0
rw [← hab, DFinsupp.sum]
by_cases hnonempty : f.support.Nonempty
· have hmem (x : ArchimedeanClass M) : (f x).val ∈ u.stratum x := Set.mem_of_mem_of_subset (f x).prop (by simp)
have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support :=
by
intro x hx y hy hxy
change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val
rw [u.archimedeanClassMk_of_mem_stratum (hmem x) (by simpa using hx)]
rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]
exact hxy
rw [mk_sum hnonempty hmono]
rw [u.archimedeanClassMk_of_mem_stratum (hmem _) (by simpa using Finset.min'_mem f.support hnonempty)]
by_contra!
obtain h := this ▸ Finset.min'_mem f.support hnonempty
contrapose! h
rw [DFinsupp.notMem_support_iff, u.archimedeanClassMk_of_mem_stratum ha h0]
simpa using (f c).prop
· rw [Finset.not_nonempty_iff_eq_empty.mp hnonempty]
symm
simpa using h0
