Lean4
/-- If `C` is an additive category, `D` is an abelian category,
we have `F : C ⥤ D` `G : D ⥤ C` (with `G` preserving zero morphisms),
`G` is left exact (that is, preserves finite limits),
and further we have `adj : G ⊣ F` and `i : F ⋙ G ≅ 𝟭 C`,
then `C` is also abelian. -/
@[stacks 03A3]
def abelianOfAdjunction {C : Type u₁} [Category.{v₁} C] [Preadditive C] [HasFiniteProducts C] {D : Type u₂}
[Category.{v₂} D] [Abelian D] (F : C ⥤ D) (G : D ⥤ C) [Functor.PreservesZeroMorphisms G] [PreservesFiniteLimits G]
(i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) : Abelian C :=
by
haveI := hasKernels F G i
haveI := hasCokernels F G i adj
have : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f) :=
by
intro X Y f
let arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor _ _).mapIso i).app (Arrow.mk f)
have : PreservesColimits G := adj.leftAdjoint_preservesColimits
let iso :
Arrow.mk (G.map (Abelian.coimageImageComparison (F.map f))) ≅ Arrow.mk (Abelian.coimageImageComparison f) :=
Abelian.PreservesCoimageImageComparison.iso G (F.map f) ≪≫ Abelian.coimageImageComparisonFunctor.mapIso arrowIso
rw [Arrow.isIso_iff_isIso_of_isIso iso.inv]
infer_instance
apply Abelian.ofCoimageImageComparisonIsIso
