exists_idempotent_ultrafilter_le_FP

English

There exists an idempotent ultrafilter U with U * U = U and such that U concentrates FP a (i.e., ∀ᶠ m in U, m ∈ FP a).

Русский

Существует идемпотентный ультрафильтр U, удовлетворяющий U*U = U, и U «сосредоточен» в FP a, т.е. ∀ᶠ m in U, m ∈ FP a.

LaTeX

$$$\\exists U: Ultrafilter(M), U * U = U \\\\wedge \\\\forallᶠ m \\\\in U, m \\\\in FP(a).$$$

Lean4

@[to_additive exists_idempotent_ultrafilter_le_FS]
theorem exists_idempotent_ultrafilter_le_FP {M} [Semigroup M] (a : Stream' M) :
    ∃ U : Ultrafilter M, U * U = U ∧ ∀ᶠ m in U, m ∈ FP a :=
  by
  let S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ m in U, m ∈ FP (a.drop n)}
  have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
  · rcases h with ⟨U, hU, U_idem⟩
    refine ⟨U, U_idem, ?_⟩
    convert Set.mem_iInter.mp hU 0
  · exact Ultrafilter.continuous_mul_left
  · apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
    · intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _
    · intro n
      exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
    · exact (ultrafilter_isClosed_basic _).isCompact
    · intro n
      apply ultrafilter_isClosed_basic
  · exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)
  · intro U hU V hV
    rw [Set.mem_iInter] at *
    intro n
    rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
    filter_upwards [hU n] with m hm
    obtain ⟨n', hn⟩ := FP.mul hm
    filter_upwards [hV (n' + n)] with m' hm'
    apply hn
    simpa only [Stream'.drop_drop, add_comm] using hm'

Похожие утверждения