equivalenceReflectsNormalEpi — Mathlib

Lean4

/-- If `F` is an equivalence and `F.map f` is a normal epi, then `f` is a normal epi. -/
def equivalenceReflectsNormalEpi {D : Type u₂} [Category.{v₁} D] [HasZeroMorphisms D] (F : C ⥤ D) [F.IsEquivalence]
    {X Y : C} {f : X ⟶ Y} (hf : NormalEpi (F.map f)) : NormalEpi f
    where
  W := F.objPreimage hf.W
  g := F.preimage ((F.objObjPreimageIso hf.W).hom ≫ hf.g)
  w := F.map_injective <| by simp [hf.w]
  isColimit :=
    isColimitOfReflects F <|
      IsColimit.ofCoconeEquiv (Cocones.precomposeEquivalence (compNatIso F).symm) <|
        (IsColimit.ofIsoColimit (IsCokernel.ofIsoComp _ _ (F.objObjPreimageIso hf.W).symm (by simp) hf.isColimit)
          (Cofork.ext (Iso.refl _) (by simp [compNatIso, Cofork.π])))

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