English
Pullback (comap) of an ultrafilter along an injection with large range is defined to be an ultrafilter on the domain whose underlying filter is the comap of the target ultrafilter along the injection.
Русский
Стягивание ультрафильтра через вложение с большой областью определения задаёт ульрафильтр на области, основанный на фильтре comap по отображению.
LaTeX
$$$ {m : \alpha \to \beta} (u : Ultrafilter \beta) \ toFilter := comap m u \;\Rightarrow\; \text{ultrafilter on } \alpha $$$
Lean4
/-- The pullback of an ultrafilter along an injection whose range is large with respect to the given
ultrafilter. -/
nonrec def comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) : Ultrafilter α
where
toFilter := comap m u
neBot' := u.neBot'.comap_of_range_mem large
le_of_le g hg hgu := by simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]
