The left Freyd category and its kernel realization

This file supplies the left-handed part of the Freyd-category API that is not yet present in Mathlib. It also constructs the kernel realization used in the Auslander--Bongartz--Gabriel argument: arrows between projective-injective objects, modulo left homotopy, map to their kernels.

def CategoryTheory.Preadditive.LeftFreyd (V : Type u) [Category.{v, u} V] [Preadditive V] : Type (max u v)

The category of arrows in V, modulo left homotopy.

@[instance_reducible]

instance CategoryTheory.Preadditive.instCategoryLeftFreyd (V : Type u) [Category.{v, u} V] [Preadditive V] : Category.{v, max u v} (LeftFreyd V)

@[instance_reducible]

instance CategoryTheory.Preadditive.instLeftFreyd (V : Type u) [Category.{v, u} V] [Preadditive V] : Preadditive (LeftFreyd V)

def CategoryTheory.Preadditive.LeftFreyd.quotient (V : Type u) [Category.{v, u} V] [Preadditive V] : Functor (Arrow V) (LeftFreyd V)

The quotient functor from the arrow category to the left Freyd category.

instance CategoryTheory.Preadditive.LeftFreyd.instFullArrowQuotient (V : Type u) [Category.{v, u} V] [Preadditive V] : (quotient V).Full

instance CategoryTheory.Preadditive.LeftFreyd.instEssSurjArrowQuotient (V : Type u) [Category.{v, u} V] [Preadditive V] : (quotient V).EssSurj

instance CategoryTheory.Preadditive.LeftFreyd.instAdditiveArrowQuotient (V : Type u) [Category.{v, u} V] [Preadditive V] : (quotient V).Additive

theorem CategoryTheory.Preadditive.LeftFreyd.eq_of_leftHomotopy {V : Type u} [Category.{v, u} V] [Preadditive V] {a b : Arrow V} (f g : a ⟶ b) (h : Arrow.LeftHomotopy f g) : (quotient V).map f = (quotient V).map g

Left-homotopic squares become equal in the left Freyd category.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.homotopyOfEq {V : Type u} [Category.{v, u} V] [Preadditive V] {a b : Arrow V} (f g : a ⟶ b) (h : (quotient V).map f = (quotient V).map g) : Arrow.LeftHomotopy f g

Equality in the left Freyd category is represented by a left homotopy.

theorem CategoryTheory.Preadditive.LeftFreyd.quotient_map_eq_iff {V : Type u} [Category.{v, u} V] [Preadditive V] {a b : Arrow V} (f g : a ⟶ b) : (quotient V).map f = (quotient V).map g ↔ Nonempty (Arrow.LeftHomotopy f g)

Two squares have equal images precisely when they are left homotopic.

@[reducible, inline]

abbrev CategoryTheory.ProjectiveObject (C : Type u) [Category.{v, u} C] : Type u

The full subcategory of projective objects.

@[reducible, inline]

abbrev CategoryTheory.ProjectiveObject.ι (C : Type u) [Category.{v, u} C] : Functor (ProjectiveObject C) C

The inclusion of projective objects.

instance CategoryTheory.ProjectiveObject.instProjectiveObjIsProjective (C : Type u) [Category.{v, u} C] (X : ProjectiveObject C) : Projective X.obj

@[reducible, inline]

abbrev CategoryTheory.InjectiveObject (C : Type u) [Category.{v, u} C] : Type u

The full subcategory of injective objects.

@[reducible, inline]

abbrev CategoryTheory.InjectiveObject.ι (C : Type u) [Category.{v, u} C] : Functor (InjectiveObject C) C

The inclusion of injective objects.

instance CategoryTheory.InjectiveObject.instInjectiveObjIsInjective (C : Type u) [Category.{v, u} C] (X : InjectiveObject C) : Injective X.obj

@[reducible, inline]

abbrev CategoryTheory.ProjectiveInjectiveObject (C : Type u) [Category.{v, u} C] : Type u

The full subcategory of objects that are both projective and injective.

@[reducible, inline]

abbrev CategoryTheory.ProjectiveInjectiveObject.ι (C : Type u) [Category.{v, u} C] : Functor (ProjectiveInjectiveObject C) C

The inclusion of projective-injective objects.

instance CategoryTheory.ProjectiveInjectiveObject.instProjectiveObjAndInjective (C : Type u) [Category.{v, u} C] (X : ProjectiveInjectiveObject C) : Projective X.obj

instance CategoryTheory.ProjectiveInjectiveObject.instInjectiveObjAndProjective (C : Type u) [Category.{v, u} C] (X : ProjectiveInjectiveObject C) : Injective X.obj

instance CategoryTheory.ProjectiveInjectiveObject.instHasFiniteBiproducts (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasFiniteBiproducts C] : Limits.HasFiniteBiproducts (ProjectiveInjectiveObject C)

Finite biproducts of projective-injective objects, constructed in the ambient preadditive category, remain projective-injective.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.rawKernel {V : Type u} [Category.{v, u} V] {C : Type u'} [Category.{v', u'} C] [Preadditive C] [Limits.HasKernels C] (F : Functor V C) : Functor (Arrow V) C

Before quotienting by left homotopy, send an arrow in V to the kernel of its image under an additive functor F : V ⥤ C.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.kernelFunctor {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Preadditive C] [Limits.HasKernels C] (F : Functor V C) [F.Additive] : Functor (LeftFreyd V) C

The kernel realization of a left Freyd category along an additive functor.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.kernelFunctorCompIso {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Preadditive C] [Limits.HasKernels C] {D : Type u''} [Category.{v'', u''} D] [Preadditive D] [Limits.HasKernels D] (F : Functor V C) [F.Additive] (G : Functor C D) [G.Additive] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) G] : (kernelFunctor F).comp G ≅ kernelFunctor (F.comp G)

Applying a kernel-preserving additive functor after kernel realization is naturally isomorphic to taking kernels after applying the composite functor.

structure CategoryTheory.Preadditive.LeftFreyd.KernelPresentationAlong {V : Type u} [Category.{v, u} V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) (X : C) : Type (max (max u v) v')

A two-term presentation of X as the kernel of the image under F of an arrow in the source category.

• left : V
• right : V
• augmentation : X ⟶ F.obj self.left
• differential : self.left ⟶ self.right
• zero : CategoryStruct.comp self.augmentation (F.map self.differential) = 0
• augmentation_mono : Mono self.augmentation
• exact : { X₁ := X, X₂ := F.obj self.left, X₃ := F.obj self.right, f := self.augmentation, g := F.map self.differential, zero := ⋯ }.Exact

def CategoryTheory.Preadditive.LeftFreyd.KernelPresentationAlong.arrow {V : Type u} [Category.{v, u} V] {C : Type u'} [Category.{v', u'} C] [Abelian C] {F : Functor V C} {X : C} (I : KernelPresentationAlong F X) : Arrow V

The source arrow of a kernel presentation.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.KernelPresentationAlong.kernelIso {V : Type u} [Category.{v, u} V] {C : Type u'} [Category.{v', u'} C] [Abelian C] {F : Functor V C} {X : C} (I : KernelPresentationAlong F X) : Limits.kernel (F.map I.differential) ≅ X

The chosen exact monomorphism identifies the formal kernel with the presented object.

theorem CategoryTheory.Preadditive.LeftFreyd.kernelFunctor_essSurj_of_kernelPresentations {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] (h : ∀ (X : C), Nonempty (KernelPresentationAlong F X)) : (kernelFunctor F).EssSurj

Kernel presentations of every target object make the kernel realization essentially surjective.

theorem CategoryTheory.Preadditive.LeftFreyd.kernelFunctor_full_of_injective_objects {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] [F.Full] [F.Faithful] (hI : ∀ (X : V), Injective (F.obj X)) : (kernelFunctor F).Full

Kernel realization along a fully faithful functor with injective values is full.

theorem CategoryTheory.Preadditive.LeftFreyd.kernelFunctor_faithful_of_injective_objects {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] [F.Full] [F.Faithful] (hI : ∀ (X : V), Injective (F.obj X)) : (kernelFunctor F).Faithful

Kernel realization along a fully faithful functor with injective values is faithful.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Preadditive.LeftFreyd.projectiveInjectiveKernelFunctor (C : Type u) [Category.{v, u} C] [Abelian C] : Functor (LeftFreyd (ProjectiveInjectiveObject C)) C

The kernel realization for arrows between projective-injective objects.

instance CategoryTheory.Preadditive.LeftFreyd.instFullProjectiveInjectiveObjectProjectiveInjectiveKernelFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : (projectiveInjectiveKernelFunctor C).Full

instance CategoryTheory.Preadditive.LeftFreyd.instFaithfulProjectiveInjectiveObjectProjectiveInjectiveKernelFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : (projectiveInjectiveKernelFunctor C).Faithful

theorem CategoryTheory.Preadditive.LeftFreyd.kernel_projective_of_projectiveDimensionLE_two {C : Type u} [Category.{v, u} C] [Abelian C] {P₀ P₁ : C} [Projective P₀] [Projective P₁] (d : P₀ ⟶ P₁) (hglobal : ∀ (X : C), HasProjectiveDimensionLE X 2) : Projective (Limits.kernel d)

In global dimension at most two, the kernel of a map between projectives is projective.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.projectiveInjectiveKernelFunctorToProjectives {C : Type u} [Category.{v, u} C] [Abelian C] (hglobal : ∀ (X : C), HasProjectiveDimensionLE X 2) : Functor (LeftFreyd (ProjectiveInjectiveObject C)) (ProjectiveObject C)

Under a global-dimension-two hypothesis, the kernel realization lands in the full subcategory of projective objects.

instance CategoryTheory.Preadditive.LeftFreyd.instFullProjectiveInjectiveObjectProjectiveObjectProjectiveInjectiveKernelFunctorToProjectives {C : Type u} [Category.{v, u} C] [Abelian C] (hglobal : ∀ (X : C), HasProjectiveDimensionLE X 2) : (projectiveInjectiveKernelFunctorToProjectives hglobal).Full

instance CategoryTheory.Preadditive.LeftFreyd.instFaithfulProjectiveInjectiveObjectProjectiveObjectProjectiveInjectiveKernelFunctorToProjectives {C : Type u} [Category.{v, u} C] [Abelian C] (hglobal : ∀ (X : C), HasProjectiveDimensionLE X 2) : (projectiveInjectiveKernelFunctorToProjectives hglobal).Faithful

structure CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation {C : Type u} [Category.{v, u} C] [Abelian C] (P : C) : Type (max u v)

A two-term projective-injective copresentation of an object. Exactness and monicity identify the object with the kernel of the displayed differential.

• I₀ : ProjectiveInjectiveObject C
• I₁ : ProjectiveInjectiveObject C
• augmentation : P ⟶ self.I₀.obj
• differential : self.I₀ ⟶ self.I₁
• zero : CategoryStruct.comp self.augmentation self.differential.hom = 0
• augmentation_mono : Mono self.augmentation
• exact : { X₁ := P, X₂ := self.I₀.obj, X₃ := self.I₁.obj, f := self.augmentation, g := self.differential.hom, zero := ⋯ }.Exact

def CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation.arrow {C : Type u} [Category.{v, u} C] [Abelian C] {P : C} (I : ProjectiveInjectiveCopresentation P) : Arrow (ProjectiveInjectiveObject C)

The arrow between projective-injectives underlying a copresentation.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation.kernelIso {C : Type u} [Category.{v, u} C] [Abelian C] {P : C} (I : ProjectiveInjectiveCopresentation P) : Limits.kernel I.differential.hom ≅ P

The kernel of the displayed differential is the copresented object.

def CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation.ofIso {C : Type u} [Category.{v, u} C] [Abelian C] {P Q : C} (I : ProjectiveInjectiveCopresentation P) (e : P ≅ Q) : ProjectiveInjectiveCopresentation Q

Transport a projective-injective copresentation across an isomorphism of the copresented object.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation.biproduct {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type} [Fintype J] [Limits.HasFiniteBiproducts C] (P : J → C) (I : (j : J) → ProjectiveInjectiveCopresentation (P j)) : ProjectiveInjectiveCopresentation (⨁ P)

Finite biproducts of two-term projective-injective copresentations.

noncomputable def CategoryTheory.Preadditive.LeftFreyd.auslanderBongartzGabrielEquivalence {C : Type u} [Category.{v, u} C] [Abelian C] (hglobal : ∀ (X : C), HasProjectiveDimensionLE X 2) (hcopresentation : ∀ (P : ProjectiveObject C), Nonempty (ProjectiveInjectiveCopresentation P.obj)) : LeftFreyd (ProjectiveInjectiveObject C) ≌ ProjectiveObject C

The Auslander--Bongartz--Gabriel kernel equivalence under global dimension at most two and two-term projective-injective copresentations of all projectives.