map_finite_effectiveEpiFamily — Mathlib

English

If F preserves finite effective epi families, then the image of a finite effective epi family is again an effective epi family.

Русский

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

LaTeX

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

Lean4

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

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