hasStrongEpiMonoFactorisations_imp_of_isEquivalence

English

If F: C ⥤ D is an equivalence and C has strong epi-mono factorisations, then D has strong epi-mono factorisations.

Русский

Если F: C ⥤ D есть эквивалентность и в C существуют сильные_epi-монo факторизации, то в D существуют такие факторизации.

LaTeX

$$$\text{HasStrongEpiMonoFactorisations}(D)$$$

Lean4

theorem hasStrongEpiMonoFactorisations_imp_of_isEquivalence (F : C ⥤ D) [IsEquivalence F]
    [h : HasStrongEpiMonoFactorisations C] : HasStrongEpiMonoFactorisations D :=
  ⟨fun {X} {Y} f =>
    by
    let em : StrongEpiMonoFactorisation (F.inv.map f) := (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
    haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
    haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
    exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc, MonoFactorisation.fac, fun_inv_map,
              id_obj, Iso.inv_hom_id_app, Category.comp_id, Iso.inv_hom_id_app_assoc] }⟩

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