# 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 : ) :
Set α

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

Equations
Instances For
theorem Filter.ker_def {α : Type u_2} (f : ) :
f.ker = sf, s
@[simp]
theorem Filter.mem_ker {α : Type u_2} {f : } {a : α} :
a f.ker sf, a s
@[simp]
theorem Filter.subset_ker {α : Type u_2} {f : } {s : Set α} :
s f.ker tf, 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
• Filter.gi_principal_ker =
Instances For
theorem Filter.ker_mono {α : Type u_2} :
Monotone Filter.ker
@[simp]
theorem Filter.ker_bot {α : Type u_2} :
.ker =
@[simp]
theorem Filter.ker_top {α : Type u_2} :
.ker = Set.univ
@[simp]
theorem Filter.ker_eq_univ {α : Type u_2} {f : } :
f.ker = Set.univ f =
@[simp]
theorem Filter.ker_inf {α : Type u_2} (f : ) (g : ) :
(f g).ker = f.ker g.ker
@[simp]
theorem Filter.ker_iInf {ι : Sort u_1} {α : Type u_2} (f : ι) :
(⨅ (i : ι), f i).ker = ⨅ (i : ι), (f i).ker
@[simp]
theorem Filter.ker_sInf {α : Type u_2} (S : Set (Filter α)) :
(sInf S).ker = fS, f.ker
@[simp]
theorem Filter.ker_principal {α : Type u_2} (s : Set α) :
.ker = s
@[simp]
theorem Filter.ker_pure {α : Type u_2} (a : α) :
(pure a).ker = {a}
@[simp]
theorem Filter.ker_comap {α : Type u_2} {β : Type u_3} (m : αβ) (f : ) :
(Filter.comap m f).ker = m ⁻¹' f.ker