English
Let f_i: α_i → β_i be a family of maps and l_i a family of filters on α_i. If almost all f_i are surjective, then the map induced on the product sends the product filter ∏ l_i to the product of the pushforwards, i.e., map (Π.map f) (π l) = π (i ↦ map (f_i) (l_i)).
Русский
Пусть f_i: α_i → β_i образуют семейство отображений, а l_i — семейство фильтров на α_i. Если почти все f_i сюръективны, то отображение на произведение фильтров удовлетворяет: map (Π.map f) (π l) = π (i ↦ map (f_i) (l_i)).
LaTeX
$$$\\operatorname{map} (\\Pi.map f) (\\pi l) = \\pi (\\lambda i, \\operatorname{map} (f_i) (l_i))$$$
Lean4
/-- Given a family of maps `f i : α i → β i` and a family of filters `l i : Filter (α i)`,
if all but finitely many of `f i` are surjective,
then the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.
See also `map_piMap_pi_finite` for the case of a finite index type.
-/
theorem map_piMap_pi {α β : ι → Type*} {f : ∀ i, α i → β i} (hf : ∀ᶠ i in cofinite, Surjective (f i))
(l : ∀ i, Filter (α i)) : map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
by
refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_
refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_
rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩
classical
rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
refine univ_pi_mem_pi (fun i ↦ ?_) ?_
· by_cases hi : i ∈ I
· simpa [hi] using image_mem_map (hs i hi)
· simp [hi]
· filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
simp [hiI, hsurj.range_eq]
