instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis

English

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

Русский

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

LaTeX

$$$[F.ReflectsEffectiveEpis] \Rightarrow F.ReflectsFiniteEffectiveEpiFamilies$$$

Lean4

instance [F.ReflectsEffectiveEpis] : F.ReflectsFiniteEffectiveEpiFamilies where
  reflects {α _ B} X π
    h := by
    simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]
    apply F.effectiveEpi_of_map
    convert (inferInstance : EffectiveEpi (inv (sigmaComparison F X) ≫ (Sigma.desc (fun a ↦ F.map (π a)))))
    simp

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