Documentation

Mathlib.Order.Filter.Ker

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.

source
theorem Filter.ker_def {α : Type u_2} (f : Filter α) :
f.ker = ⋂ s ∈ f, s
source
@[simp]
theorem Filter.mem_ker {α : Type u_2} {f : Filter α} {a : α} :
a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s
source
@[simp]
theorem Filter.subset_ker {α : Type u_2} {f : Filter α} {s : Set α} :
s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t
source
def Filter.giPrincipalKer {α : Type u_2} :
GaloisCoinsertion principal ker

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

Equations
Instances For
    source
    @[deprecated Filter.giPrincipalKer (since := "2026-07-18")]
    def Filter.gi_principal_ker {α : Type u_2} :
    GaloisCoinsertion principal ker

    Alias of Filter.giPrincipalKer.

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

    Equations
    Instances For
      source
      theorem Filter.ker_mono {α : Type u_2} :
      Monotone ker
      source
      theorem Filter.ker_surjective {α : Type u_2} :
      Function.Surjective ker
      source
      @[simp]
      theorem Filter.ker_bot {α : Type u_2} :
      ⊥.ker = ∅
      source
      @[simp]
      theorem Filter.ker_top {α : Type u_2} :
      ⊤.ker = Set.univ
      source
      @[simp]
      theorem Filter.ker_eq_univ {α : Type u_2} {f : Filter α} :
      f.ker = Set.univ ↔ f = ⊤
      source
      @[simp]
      theorem Filter.ker_inf {α : Type u_2} (f g : Filter α) :
      (f ⊓ g).ker = f.ker ∩ g.ker
      source
      @[simp]
      theorem Filter.ker_iInf {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α) :
      (⨅ (i : ι), f i).ker = ⋂ (i : ι), (f i).ker
      source
      @[simp]
      theorem Filter.ker_sInf {α : Type u_2} (S : Set (Filter α)) :
      (sInf S).ker = ⋂ f ∈ S, f.ker
      source
      @[simp]
      theorem Filter.ker_principal {α : Type u_2} (s : Set α) :
      (principal s).ker = s
      source
      @[simp]
      theorem Filter.ker_pure {α : Type u_2} (a : α) :
      (pure a).ker = {a}
      source
      @[simp]
      theorem Filter.ker_comap {α : Type u_2} {β : Type u_3} (m : α → β) (f : Filter β) :
      (comap m f).ker = m ⁻¹' f.ker
      source
      @[simp]
      theorem Filter.ker_iSup {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α) :
      (⨆ (i : ι), f i).ker = ⋃ (i : ι), (f i).ker
      source
      @[simp]
      theorem Filter.ker_sSup {α : Type u_2} (S : Set (Filter α)) :
      (sSup S).ker = ⋃ f ∈ S, f.ker
      source
      @[simp]
      theorem Filter.ker_sup {α : Type u_2} (f g : Filter α) :
      (f ⊔ g).ker = f.ker ∪ g.ker
      source
      @[simp]
      theorem Filter.ker_prod {α : Type u_2} {β : Type u_3} (f : Filter α) (g : Filter β) :
      (f ×ˢ g).ker = f.ker ×ˢ g.ker
      source
      @[simp]
      theorem Filter.ker_pi {ι : Type u_4} {α : ι → Type u_5} (f : (i : ι) → Filter (α i)) :
      (pi f).ker = Set.univ.pi fun (i : ι) => (f i).ker