generate filter

Stream: maths

[Kenny Lau]

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 _ _⟩ }

[Kenny Lau]

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

[Kenny Lau]

aha, that's the wrong definition

[Reid Barton]

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

[Kenny Lau]

/-- 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}

[Kenny Lau]

that's the right definition

[Kenny Lau]

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

[Kenny Lau]

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