map_effectiveEpiFamily — Mathlib

English

If F preserves epi families, the image of an effective epi family under F is again an effective epi family.

Русский

Если F сохраняет семейства эпиморфий, образ эффективного эпиморфного семейства под F является снова эффективным семейством.

LaTeX

$$$[F.PreservesEffectiveEpiFamilies] \Rightarrow \operatorname{EffectiveEpiFamily} (F.obj\circ X) (F.map\circ \pi)$$$

Lean4

instance map_effectiveEpiFamily (F : C ⥤ D) [PreservesEffectiveEpiFamilies.{u} F] {α : Type u} {B : C} (X : α → C)
    (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] :
    EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a ↦ F.map (π a)) :=
  PreservesEffectiveEpiFamilies.preserves X π

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