Zulip Chat Archive

Stream: maths

Topic: generate filter


view this post on Zulip Kenny Lau (Apr 28 2018 at 04:50):

def generate {α : Type u} (s :set (set α)) : filter α :=
{ sets := { A |  t  s, ⋂₀ t  A },
  univ := , set.empty_subset s, @set.sInter_empty α  set.subset.refl _⟩,
  up   := λ x t, ht1, ht2 y H2, t, ht1, set.subset.trans ht2 H2,
  down := λ x t, ht1, ht2 y u, hu1, hu2, x  y,
      t  u, set.union_subset ht1 hu1, (set.sInter_union t u).symm 
        set.subset_inter
          (set.subset.trans (set.inter_subset_left _ _) ht2)
          (set.subset.trans (set.inter_subset_right _ _) hu2),
    set.inter_subset_left _ _, set.inter_subset_right _ _⟩ }

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:50):

in mathlib it's done by taking the infimum of the principal filters lol

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:55):

aha, that's the wrong definition

view this post on Zulip Reid Barton (Apr 28 2018 at 04:56):

Those mathlib-style definitions are actually quite convenient because you can immediately use them with lemmas like vmap_infi, vmap_principal, etc.

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:17):

/-- The filter generated by a set of sets. -/
def generate (s :set (set α)) : filter α :=
{ sets  := { A |  t  s, set.finite t  ⋂₀ t  A },
  univ  := , set.empty_subset s, set.finite_empty, @set.sInter_empty α  set.subset.refl _⟩,
  up    := λ x t, ht1, ht2, ht3 y H2, t, ht1, ht2, set.subset.trans ht3 H2,
  inter := λ x t, ht1, ht2, ht3 y u, hu1, hu2, hu3,
    t  u, set.union_subset ht1 hu1, set.finite_union ht2 hu2,
    (set.sInter_union t u).symm  set.subset_inter
      (set.subset.trans (set.inter_subset_left _ _) ht3)
      (set.subset.trans (set.inter_subset_right _ _) hu3) }

/-- The filter generated contains the original sets. -/
theorem generate.subset (s :set (set α)) : s  (generate s).sets :=
λ A HA, {A}, set.singleton_subset_iff.2 HA, set.finite_singleton A,
  (set.sInter_singleton A).symm  set.subset.refl A

/-- The filter generated is the smallest filter containing the original sets. -/
theorem generate.min (s :set (set α)) {f : filter α} (H : s  f.sets) :
  (generate s).sets  f.sets :=
λ A t, ht1, ht2, ht3, (set.finite.induction_on ht2
  (λ A _ HA, have H1 : A = set.univ,
    from set.eq_univ_of_univ_subset $ @set.sInter_empty α  HA,
    H1.symm  f.univ)
  (λ B t _ _ ih A ht1 ht3, f.up (⋂₀ insert B t)
    ((set.sInter_insert B t).symm 
      f.inter B (H $ ht1 $ set.mem_insert _ _)
      (⋂₀ t) (ih _ (set.insert_subset.1 ht1).2 (set.subset.refl _))) _ ht3)) A ht1 ht3

/-- The filter generated by one element. -/
def principal {α : Type u} (s : set α) : filter α :=
generate {s}

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:18):

that's the right definition

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:18):

and I learnt how to use set.finite.induction_on :P

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:19):

@Kevin Buzzard do you think that's enough interface?


Last updated: May 09 2021 at 09:11 UTC