instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies

English

If F reflects finite effective epi families, then F reflects effective epis.

Русский

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

LaTeX

$$$\\forall {C} [\\mathbf{Category} C] {D} [\\mathbf{Category} D] (F : C \\to D) [ReflectsFiniteEffectiveEpiFamilies F], \\operatorname{ReflectsEffectiveEpis} F$$

Lean4

instance (F : C ⥤ D) [ReflectsFiniteEffectiveEpiFamilies F] : ReflectsEffectiveEpis F where
  reflects _
    h := by
    rw [effectiveEpi_iff_effectiveEpiFamily] at h
    have := F.finite_effectiveEpiFamily_of_map _ _ h
    infer_instance

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