English
For a map m: α → β and a filter f on α, kernMap m f is the filter on β generated by the images under m of sets in f. Equivalently, a subset s ⊆ β belongs to kernMap m f iff there exists t ∈ f with s = kernImage m t (or, equivalently, tᶜ ∈ f and sᶜ = m '' t).
Русский
Для отображения m: α → β и фильтра f на α, kernMap m f есть фильтр на β, порожденный образами подмножест сф от m от множеств из f. Эквивалентно: множество s ⊆ β принадлежит kernMap m f тогда и только тогда, когда существует t ∈ f такое, что s = kernImage m t (или эквивалентно tᶜ ∈ f и sᶜ = m '' t).
LaTeX
$$$\\operatorname{kernMap}(m,f)\\;\\text{ is defined by }\\; s \\in \\operatorname{kernMap}(m,f) \\iff \\exists t \\in f,\\ \\operatorname{kernImage}(m,t) = s$$$
Lean4
/-- The analog of `Set.kernImage` for filters.
A set `s` belongs to `Filter.kernMap m f` if either of the following equivalent conditions hold.
1. There exists a set `t ∈ f` such that `s = Set.kernImage m t`. This is used as a definition.
2. There exists a set `t` such that `tᶜ ∈ f` and `sᶜ = m '' t`, see `Filter.mem_kernMap_iff_compl`
and `Filter.compl_mem_kernMap`.
This definition is useful because it gives a right adjoint to `Filter.comap`, and because it has a
nice interpretation when working with `co-` filters (`Filter.cocompact`, `Filter.cofinite`, ...).
For example, `kernMap m (cocompact α)` is the filter generated by the complements of the sets
`m '' K` where `K` is a compact subset of `α`. -/
def kernMap (m : α → β) (f : Filter α) : Filter β
where
sets := (kernImage m) '' f.sets
univ_sets := ⟨univ, f.univ_sets, by simp [kernImage_eq_compl]⟩
sets_of_superset := by
rintro _ t ⟨s, hs, rfl⟩ hst
refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩
rw [kernImage_union_preimage, union_eq_right.mpr hst]
inter_sets := by
rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩
exact ⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩
