equivalenceReflectsNormalMono — Mathlib

Lean4
/-- If `F` is an equivalence and `F.map f` is a normal mono, then `f` is a normal mono. -/
def equivalenceReflectsNormalMono {D : Type u₂} [Category.{v₁} D] [HasZeroMorphisms D] (F : C ⥤ D) [F.IsEquivalence]
    {X Y : C} {f : X ⟶ Y} (hf : NormalMono (F.map f)) : NormalMono f
    where
  Z := F.objPreimage hf.Z
  g := F.preimage (hf.g ≫ (F.objObjPreimageIso hf.Z).inv)
  w :=
    F.map_injective <|
      by
      have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by rw [← Category.assoc, eq_whisker hf.w]
      simp [reassoc']
  isLimit :=
    isLimitOfReflects F <|
      IsLimit.ofConeEquiv (Cones.postcomposeEquivalence (compNatIso F)) <|
        (IsLimit.ofIsoLimit
            (IsKernel.ofCompIso _ _ (F.objObjPreimageIso hf.Z)
              (by simp only [Functor.map_preimage, Category.assoc, Iso.inv_hom_id, Category.comp_id]) hf.isLimit))
          (Fork.ext (Iso.refl _) (by simp [compNatIso, Fork.ι]))
Похожие утверждения