epi_map_0_of_epi — Mathlib

English

If f is epi in the underlying category, then the induced map on the 0th level of cycles is epi in the module category.

Русский

Если f является эпиморфизмом в базовой категории, то индуцированное отображение на нулевом уровне циклов является эпиморфизмом в категорию модулей.

LaTeX

$$$\text{Epi}\, f \Rightarrow \text{Epi} \big(\mathrm{cyclesMap}(f, \phi, 0)\big)$$$

Lean4

instance epi_map_0_of_epi {A B : Rep k G} (f : A ⟶ B) [Epi f] : Epi (map (MonoidHom.id G) f 0) where
  left_cancellation g h
    hgh := by
    simp only [← cancel_epi (H0π A)] at hgh
    simp_all [cancel_epi]

Похожие утверждения