instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis

English

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

Русский

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

LaTeX

$$$[F.PreservesEffectiveEpis] \Rightarrow F.PreservesFiniteEffectiveEpiFamilies$$$

Lean4

instance [F.PreservesEffectiveEpis] : F.PreservesFiniteEffectiveEpiFamilies where
  preserves {α _ B} X π
    h := by
    simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]
    convert (inferInstance : EffectiveEpi ((sigmaComparison F X) ≫ (F.map (Sigma.desc π))))
    simp

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