splitEpiCategoryImpOfIsEquivalence

English

If F is an equivalence and C is a SplitEpiCategory, then D is a SplitEpiCategory.

Русский

Если F — эквивалентность, и C является SplitEpiCategory, то D тоже является SplitEpiCategory.

LaTeX

$$$$ \\mathrm{IsEquivalence}(F) \\Rightarrow (\\mathrm{SplitEpiCategory}(C) \\Rightarrow \\mathrm{SplitEpiCategory}(D)). $$$$

Lean4

/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `split_epi_category`,
then `D` also is. -/
theorem splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] : SplitEpiCategory D :=
  ⟨fun {X} {Y} f => by
    intro
    rw [← F.inv.isSplitEpi_iff f]
    apply isSplitEpi_of_epi⟩

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