Kernel duality on epimorphic right-Freyd presentations

For an epimorphism g : B ⟶ C in an abelian category, its kernel inclusion ker(g) ⟶ B becomes an epimorphism in the opposite category. A square of epimorphisms induces a square of the opposite kernel inclusions in the reverse direction. Right homotopies are carried to right homotopies, so the construction descends to right Freyd categories.

def CategoryTheory.Preadditive.RightFreyd.IsEpiArrow (C : Type u) [Category.{v, u} C] [Abelian C] : ObjectProperty (RightFreyd C)

Right-Freyd objects represented by epimorphisms.

@[reducible, inline]

abbrev CategoryTheory.Preadditive.RightFreyd.EpiCategory (C : Type u) [Category.{v, u} C] [Abelian C] : Type (max u v)

The full subcategory of the right Freyd category on epimorphic presentations.

noncomputable def CategoryTheory.Preadditive.RightFreyd.kernelMap {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} (s : b ⟶ a) : Limits.kernel b.hom ⟶ Limits.kernel a.hom

The map between kernels induced by a square of arrows.

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelMap_comp_ι {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} (s : b ⟶ a) : CategoryStruct.comp (kernelMap s) (Limits.kernel.ι a.hom) = CategoryStruct.comp (Limits.kernel.ι b.hom) (Arrow.Hom.left s)

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelMap_comp_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} (s : b ⟶ a) {Z : C} (h : a.left ⟶ Z) : CategoryStruct.comp (kernelMap s) (CategoryStruct.comp (Limits.kernel.ι a.hom) h) = CategoryStruct.comp (Limits.kernel.ι b.hom) (CategoryStruct.comp (Arrow.Hom.left s) h)

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelMap_id {C : Type u} [Category.{v, u} C] [Abelian C] (a : Arrow C) : kernelMap (CategoryStruct.id a) = CategoryStruct.id (Limits.kernel a.hom)

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelMap_comp {C : Type u} [Category.{v, u} C] [Abelian C] {a b c : Arrow C} (s : c ⟶ b) (t : b ⟶ a) : kernelMap (CategoryStruct.comp s t) = CategoryStruct.comp (kernelMap s) (kernelMap t)

noncomputable def CategoryTheory.Preadditive.RightFreyd.kernelOpMapRepresentative {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} (s : b ⟶ a) : Arrow.mk (Limits.kernel.ι a.hom).op ⟶ Arrow.mk (Limits.kernel.ι b.hom).op

A square b ⟶ a gives a reversed square between the opposite kernel inclusions.

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelOpMapRepresentative_id {C : Type u} [Category.{v, u} C] [Abelian C] (a : Arrow C) : kernelOpMapRepresentative (CategoryStruct.id a) = CategoryStruct.id (Arrow.mk (Limits.kernel.ι a.hom).op)

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.kernelOpMapRepresentative_comp {C : Type u} [Category.{v, u} C] [Abelian C] {a b c : Arrow C} (s : c ⟶ b) (t : b ⟶ a) : kernelOpMapRepresentative (CategoryStruct.comp s t) = CategoryStruct.comp (kernelOpMapRepresentative t) (kernelOpMapRepresentative s)

noncomputable def CategoryTheory.Preadditive.RightFreyd.kernelOpRightHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} (s t : b ⟶ a) (H : Arrow.RightHomotopy s t) : Arrow.RightHomotopy (kernelOpMapRepresentative s) (kernelOpMapRepresentative t)

Right-homotopic squares induce right-homotopic reversed kernel squares.

noncomputable def CategoryTheory.Preadditive.RightFreyd.kernelOp {C : Type u} [Category.{v, u} C] [Abelian C] : Functor (EpiCategory C)ᵒᵖ (EpiCategory Cᵒᵖ)

Taking the opposite kernel inclusion descends to a contravariant functor between the epimorphic parts of the two right Freyd categories.

noncomputable def CategoryTheory.Preadditive.RightFreyd.rightHomotopyOfKernelOpRightHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {a b : Arrow C} [Epi b.hom] (s t : b ⟶ a) (H : Arrow.RightHomotopy (kernelOpMapRepresentative s) (kernelOpMapRepresentative t)) : Arrow.RightHomotopy s t

For epimorphic presentations, a right homotopy between the reversed kernel squares comes from a right homotopy between the original squares.

instance CategoryTheory.Preadditive.RightFreyd.kernelOp_faithful {C : Type u} [Category.{v, u} C] [Abelian C] : kernelOp.Faithful

Kernel reversal is faithful on epimorphic right-Freyd presentations.

instance CategoryTheory.Preadditive.RightFreyd.kernelOp_full {C : Type u} [Category.{v, u} C] [Abelian C] : kernelOp.Full

Kernel reversal is full on epimorphic right-Freyd presentations.

instance CategoryTheory.Preadditive.RightFreyd.kernelOp_essSurj {C : Type u} [Category.{v, u} C] [Abelian C] : kernelOp.EssSurj

Every epimorphic presentation in the opposite category is, up to isomorphism, the opposite kernel presentation of an epimorphism.

instance CategoryTheory.Preadditive.RightFreyd.kernelOp_isEquivalence {C : Type u} [Category.{v, u} C] [Abelian C] : kernelOp.IsEquivalence

noncomputable def CategoryTheory.Preadditive.RightFreyd.kernelOpEquivalence {C : Type u} [Category.{v, u} C] [Abelian C] : (EpiCategory C)ᵒᵖ ≌ EpiCategory Cᵒᵖ

The anti-equivalence between epimorphic presentations and opposite kernel presentations.