Kernel of a filter

In this file we define the kernel Filter.ker f of a filter f to be the intersection of all its sets.

We also prove that Filter.principal and Filter.ker form a Galois coinsertion and prove other basic theorems about Filter.ker.

def Filter.ker {α : Type u_2} (f : Filter α) : Set α

The kernel of a filter is the intersection of all its sets.

Equations

• Filter.ker f = ⋂₀ f.sets

theorem Filter.ker_def {α : Type u_2} (f : Filter α) : Filter.ker f = ⋂ s ∈ f, s

@[simp]

theorem Filter.mem_ker {α : Type u_2} {f : Filter α} {a : α} : a ∈ Filter.ker f ↔ ∀ s ∈ f, a ∈ s

@[simp]

theorem Filter.subset_ker {α : Type u_2} {f : Filter α} {s : Set α} : s ⊆ Filter.ker f ↔ ∀ t ∈ f, s ⊆ t

def Filter.gi_principal_ker {α : Type u_2} : GaloisCoinsertion Filter.principal Filter.ker

Filter.principal forms a Galois coinsertion with Filter.ker.

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.ker_mono {α : Type u_2} : Monotone Filter.ker

theorem Filter.ker_surjective {α : Type u_2} : Function.Surjective Filter.ker

@[simp]

theorem Filter.ker_bot {α : Type u_2} : Filter.ker ⊥ = ∅

@[simp]

theorem Filter.ker_top {α : Type u_2} : Filter.ker ⊤ = Set.univ

@[simp]

theorem Filter.ker_eq_univ {α : Type u_2} {f : Filter α} : Filter.ker f = Set.univ ↔ f = ⊤

@[simp]

theorem Filter.ker_inf {α : Type u_2} (f : Filter α) (g : Filter α) : Filter.ker (f ⊓ g) = Filter.ker f ∩ Filter.ker g

@[simp]

theorem Filter.ker_iInf {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α) : Filter.ker (⨅ (i : ι), f i) = ⨅ (i : ι), Filter.ker (f i)

@[simp]

theorem Filter.ker_sInf {α : Type u_2} (S : Set (Filter α)) : Filter.ker (sInf S) = ⨅ f ∈ S, Filter.ker f

@[simp]

theorem Filter.ker_principal {α : Type u_2} (s : Set α) : Filter.ker (Filter.principal s) = s

@[simp]

theorem Filter.ker_pure {α : Type u_2} (a : α) : Filter.ker (pure a) = {a}

@[simp]

theorem Filter.ker_comap {α : Type u_2} {β : Type u_3} (m : α → β) (f : Filter β) : Filter.ker (Filter.comap m f) = m ⁻¹' Filter.ker f