instReflectsEffectiveEpiFamiliesOfIsEquivalence

English

If F is an equivalence, then F reflects effective epis.

Русский

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

LaTeX

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

Lean4

instance (F : C ⥤ D) [IsEquivalence F] : F.ReflectsEffectiveEpiFamilies where
  reflects {α B} X π
    _ := by
    let i : (a : α) → X a ⟶ (inv F).obj (F.obj (X a)) := fun a ↦ (asEquivalence F).unit.app _
    have : EffectiveEpiFamily X (fun a ↦ (i a) ≫ (inv F).map (F.map (π a))) := inferInstance
    simp only [inv_fun_map, Iso.hom_inv_id_app_assoc, i] at this
    have : EffectiveEpiFamily X (fun a ↦ (π a ≫ (asEquivalence F).unit.app B) ≫ (asEquivalence F).unitInv.app _) :=
      inferInstance
    simpa

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