instEpiTopCatBaseπ — Mathlib

English

For any parallel pair f,g in the category of SheafedSpaces, the base map of the coequalizer projection is an epimorphism.

Русский

Для любой пары параллельных стрелок f,g в категории SheafedSpace базовый отображатель коэквализатора является эпиморфизмом.

LaTeX

$$epi\left((\mathrm{coequalizer}.\pi\ f\ g).\text{base}\right)$$

Lean4

instance [HasLimits C] {X Y : SheafedSpace C} (f g : X ⟶ Y) : Epi (coequalizer.π f g).base :=
  by
  rw [← show _ = (coequalizer.π f g).base from ι_comp_coequalizerComparison f g (SheafedSpace.forget C), ←
    PreservesCoequalizer.iso_hom]
  apply epi_comp

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