English
If each component map f_n is epi and certain countable biproduct and product hypotheses hold, then the transition map functorMap f n is an epimorphism.
Русский
Если каждый компонент отображения f_n является эпиморфизмом и выполняются некоторые условия по счетным бипроизведениям и произведениям, то переходное отображение functorMap f n является эпиморфизмом.
LaTeX
$$$\\forall n,\\;\\mathrm{epi}(\\mathrm{functorMap}\\ f\\ n)$$$
Lean4
theorem functorMap_epi (n : ℕ) : Epi (functorMap f n) :=
by
rw [functorMap, Pi.map_eq_prod_map (P := fun m : ℕ ↦ m < n + 1)]
apply (config := { allowSynthFailures := true }) epi_comp
apply (config := { allowSynthFailures := true }) epi_comp
apply (config := { allowSynthFailures := true }) prod.map_epi
· apply (config := { allowSynthFailures := true }) Pi.map_epi
intro ⟨_, _⟩
split
all_goals infer_instance
· apply (config := { allowSynthFailures := true }) IsIso.epi_of_iso
apply (config := { allowSynthFailures := true }) Pi.map_isIso
intro ⟨_, _⟩
split
all_goals infer_instance
