Mathlib.Order.Filter.Ker

Filter.ker_def theorem

(f : Filter α) : f.ker = ⋂ s ∈ f, s

Full source

lemma ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s := sInter_eq_biInter

Definition of Filter Kernel as Intersection of All Sets in the Filter

Informal description

For any filter $f$ on a type $\alpha$, the kernel of $f$, denoted $\ker(f)$, is equal to the intersection of all sets in $f$, i.e., $\ker(f) = \bigcap_{s \in f} s$.

Filter.mem_ker theorem

: a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s

Full source

@[simp] lemma mem_ker : a ∈ f.kera ∈ f.ker ↔ ∀ s ∈ f, a ∈ s := mem_sInter

Characterization of Kernel Membership in a Filter

Informal description

For any element $a$ of type $\alpha$ and any filter $f$ on $\alpha$, the element $a$ belongs to the kernel of $f$ if and only if $a$ belongs to every set $s$ in the filter $f$.

Filter.subset_ker theorem

: s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t

Full source

@[simp] lemma subset_ker : s ⊆ f.kers ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_sInter_iff

Characterization of Subset Relation with Filter Kernel: $s \subseteq \ker(f) \leftrightarrow \forall t \in f, s \subseteq t$

Informal description

For any set $s$ and any filter $f$ on a type $\alpha$, the set $s$ is contained in the kernel $\ker(f)$ if and only if $s$ is contained in every set $t$ belonging to the filter $f$.

Filter.gi_principal_ker definition

: GaloisCoinsertion (𝓟 : Set α → Filter α) ker

Full source

/-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/
def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker :=
  GaloisConnection.toGaloisCoinsertion (fun s f ↦ by simp [principal_le_iff]) <| by
    simp only [le_iff_subset, subset_def, mem_ker, mem_principal]; aesop

Galois coinsertion between principal filters and kernels

Informal description

The pair of functions `𝓟 : Set α → Filter α` (which maps a set to the principal filter it generates) and `ker : Filter α → Set α` (which maps a filter to its kernel, the intersection of all its sets) form a Galois coinsertion. This means they satisfy the Galois connection property `𝓟 s ≤ f ↔ s ⊆ ker f` for all sets `s` and filters `f`, and additionally `ker (𝓟 s) = s` for all sets `s`.

Filter.ker_mono theorem

: Monotone (ker : Filter α → Set α)

Full source

lemma ker_mono : Monotone (ker : Filter α → Set α) := gi_principal_ker.gc.monotone_u

Monotonicity of Filter Kernel

Informal description

The kernel function $\ker : \text{Filter } \alpha \to \text{Set } \alpha$, which maps a filter to the intersection of all its sets, is monotone. That is, for any filters $f_1, f_2$ on $\alpha$, if $f_1 \leq f_2$ in the filter ordering, then $\ker(f_1) \subseteq \ker(f_2)$.

Filter.ker_surjective theorem

: Surjective (ker : Filter α → Set α)

Full source

lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_ker.u_surjective

Surjectivity of Filter Kernel Function

Informal description

The kernel function $\ker : \text{Filter } \alpha \to \text{Set } \alpha$, which maps a filter to the intersection of all its sets, is surjective. That is, for every set $s \subseteq \alpha$, there exists a filter $f$ on $\alpha$ such that $\ker(f) = s$.

Filter.ker_bot theorem

: ker (⊥ : Filter α) = ∅

Full source

@[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := sInter_eq_empty_iff.2 fun _ ↦ ⟨∅, trivial, id⟩

Kernel of Bottom Filter is Empty Set

Informal description

The kernel of the bottom filter $\bot$ (the filter containing all subsets of $\alpha$) is the empty set, i.e., $\ker(\bot) = \emptyset$.

Filter.ker_top theorem

: ker (⊤ : Filter α) = univ

Full source

@[simp] lemma ker_top : ker (⊤ : Filter α) = univ := gi_principal_ker.gc.u_top

Kernel of Top Filter is Universal Set

Informal description

The kernel of the top filter $\top$ (the filter containing only the universal set) is equal to the universal set, i.e., $\ker(\top) = \text{univ}$.

Filter.ker_eq_univ theorem

: ker f = univ ↔ f = ⊤

Full source

@[simp] lemma ker_eq_univ : kerker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp

Characterization of Top Filter via Kernel: $\ker f = \text{univ} \leftrightarrow f = \top$

Informal description

For any filter $f$ on a type $\alpha$, the kernel of $f$ (the intersection of all sets in $f$) equals the universal set if and only if $f$ is the top filter (the filter containing only the universal set). In symbols: $$ \ker f = \text{univ} \leftrightarrow f = \top $$

Filter.ker_inf theorem

(f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g

Full source

@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = kerker f ∩ ker g := gi_principal_ker.gc.u_inf

Kernel of Filter Infimum Equals Intersection of Kernels

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the kernel of their infimum $f \sqcap g$ (the intersection of all sets in $f \sqcap g$) is equal to the intersection of their individual kernels, i.e., $\ker(f \sqcap g) = \ker f \cap \ker g$.

Filter.ker_iInf theorem

(f : ι → Filter α) : ker (⨅ i, f i) = ⋂ i, ker (f i)

Full source

@[simp] lemma ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⋂ i, ker (f i) :=
  gi_principal_ker.gc.u_iInf

Kernel of Infimum of Filters Equals Intersection of Kernels

Informal description

For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the kernel of their infimum equals the intersection of their kernels. That is, \[ \ker\left(\bigsqcap_{i} f_i\right) = \bigcap_{i} \ker(f_i). \]

Filter.ker_sInf theorem

(S : Set (Filter α)) : ker (sInf S) = ⋂ f ∈ S, ker f

Full source

@[simp] lemma ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⋂ f ∈ S, ker f :=
  gi_principal_ker.gc.u_sInf

Kernel of Infimum of Filters Equals Intersection of Kernels

Informal description

For any collection $S$ of filters on a type $\alpha$, the kernel of the infimum of $S$ is equal to the intersection of the kernels of all filters in $S$, i.e., \[ \ker\left(\bigsqcap S\right) = \bigcap_{f \in S} \ker f. \]

Filter.ker_principal theorem

(s : Set α) : ker (𝓟 s) = s

Full source

@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := gi_principal_ker.u_l_eq _

Kernel of Principal Filter Equals Original Set

Informal description

For any set $s$ in a type $\alpha$, the kernel of the principal filter generated by $s$ is equal to $s$ itself, i.e., \[ \ker(\mathcal{P}(s)) = s. \]

Filter.ker_pure theorem

(a : α) : ker (pure a) = { a }

Full source

@[simp] lemma ker_pure (a : α) : ker (pure a) = {a} := by rw [← principal_singleton, ker_principal]

Kernel of Pure Filter is Singleton Set

Informal description

For any element $a$ of a type $\alpha$, the kernel of the pure filter generated by $a$ is equal to the singleton set $\{a\}$, i.e., \[ \ker(\mathrm{pure}\, a) = \{a\}. \]

Filter.ker_comap theorem

(m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f

Full source

@[simp] lemma ker_comap (m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f := by
  ext a
  simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_swap (Set α), mem_preimage]
  exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

Kernel of Preimage Filter Equals Preimage of Kernel

Informal description

For any function $m : \alpha \to \beta$ and any filter $f$ on $\beta$, the kernel of the preimage filter $\operatorname{comap} m f$ is equal to the preimage under $m$ of the kernel of $f$, i.e., \[ \ker(\operatorname{comap} m f) = m^{-1}(\ker f). \]

Filter.ker_iSup theorem

(f : ι → Filter α) : ker (⨆ i, f i) = ⋃ i, ker (f i)

Full source

@[simp]
theorem ker_iSup (f : ι → Filter α) : ker (⨆ i, f i) = ⋃ i, ker (f i) := by
  refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup
  simp only [mem_iUnion, mem_ker] at hx ⊢
  contrapose! hx
  choose s hsf hxs using hx
  refine ⟨⋃ i, s i, ?_, by simpa⟩
  exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

Kernel of Filter Supremum Equals Union of Kernels

Informal description

For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the kernel of their supremum is equal to the union of their individual kernels, i.e., \[ \ker\left(\bigsqcup_{i \in \iota} f_i\right) = \bigcup_{i \in \iota} \ker(f_i). \]

Filter.ker_sSup theorem

(S : Set (Filter α)) : ker (sSup S) = ⋃ f ∈ S, ker f

Full source

@[simp]
theorem ker_sSup (S : Set (Filter α)) : ker (sSup S) = ⋃ f ∈ S, ker f := by
  simp [sSup_eq_iSup]

Kernel of Filter Supremum Equals Union of Kernels

Informal description

For any set $S$ of filters on a type $\alpha$, the kernel of the supremum of $S$ is equal to the union of the kernels of all filters in $S$, i.e., \[ \ker\left(\bigvee S\right) = \bigcup_{f \in S} \ker(f). \]

Filter.ker_sup theorem

(f g : Filter α) : ker (f ⊔ g) = ker f ∪ ker g

Full source

@[simp]
theorem ker_sup (f g : Filter α) : ker (f ⊔ g) = kerker f ∪ ker g := by
  rw [← sSup_pair, ker_sSup, biUnion_pair]

Kernel of Supremum of Two Filters Equals Union of Kernels

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the kernel of their supremum $f \sqcup g$ is equal to the union of their individual kernels, i.e., \[ \ker(f \sqcup g) = \ker(f) \cup \ker(g). \]