English
Given an ultrafilter U on M with idempotent U, and a large set s0 ∈ U, there exists a sequence a such that FP a ⊆ s0.
Русский
С учётом идемпотентного ультрафильтра U и большого множества s0 ∈ U существует последовательность a такая, что FP a ⊆ s0.
LaTeX
$$$\\exists a, FP(a) \\subseteq s_0.$$$$
Lean4
@[to_additive exists_FS_of_large]
theorem exists_FP_of_large {M} [Semigroup M] (U : Ultrafilter M) (U_idem : U * U = U) (s₀ : Set M) (sU : s₀ ∈ U) :
∃ a, FP a ⊆ s₀ := by
/- Informally: given a `U`-large set `s₀`, the set `s₀ ∩ { m | ∀ᶠ m' in U, m * m' ∈ s₀ }` is also
`U`-large (since `U` is idempotent). Thus in particular there is an `a₀` in this intersection. Now
let `s₁` be the intersection `s₀ ∩ { m | a₀ * m ∈ s₀ }`. By choice of `a₀`, this is again
`U`-large, so we can repeat the argument starting from `s₁`, obtaining `a₁`, `s₂`, etc.
This gives the desired infinite sequence. -/
have exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m | ∀ᶠ m' in U, m * m' ∈ s}).Nonempty := fun {s} hs =>
Ultrafilter.nonempty_of_mem (inter_mem hs <| by rwa [← U_idem] at hs)
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some
let succ : { s // s ∈ U } → { s // s ∈ U } := fun (p : { s // s ∈ U }) =>
⟨p.val ∩ {m : M | elem p * m ∈ p.val},
inter_mem p.property
(show (exists_elem p.property).some ∈ {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} from
p.val.inter_subset_right (exists_elem p.property).some_mem)⟩
use Stream'.corec elem succ (Subtype.mk s₀ sU)
suffices ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ p, a = Stream'.corec elem succ p → m ∈ p.val
by
intro m hm
exact this _ m hm ⟨s₀, sU⟩ rfl
clear sU s₀
intro a m h
induction h with
| head' b =>
rintro p rfl
rw [Stream'.corec_eq, Stream'.head_cons]
exact Set.inter_subset_left (Set.Nonempty.some_mem _)
| tail' b n h ih =>
rintro p rfl
refine Set.inter_subset_left (ih (succ p) ?_)
rw [Stream'.corec_eq, Stream'.tail_cons]
| cons' b n h ih =>
rintro p rfl
have := Set.inter_subset_right (ih (succ p) ?_)
· simpa only using this
rw [Stream'.corec_eq, Stream'.tail_cons]
