Abelianness of the doubling

RS/Classical/Deligne/Doubling.lean equips the ℤ/2-graded doubling Doubled A with componentwise binary biproducts, kernels and cokernels. This module upgrades that bookkeeping to abelianness: if A is abelian, so is Doubled A.

The route is Mathlib's coimage–image criterion CategoryTheory.Abelian.ofCoimageImageComparisonIsIso. The two component functors evenFunctor, oddFunctor : Doubled A ⥤ A preserve kernels and cokernels, because the kernel and the cokernel of a morphism of super-objects are the componentwise ones; hence they preserve abelian images, abelian coimages, and the comparison morphism between them. Downstairs that comparison is an isomorphism, so both components of the comparison upstairs are isomorphisms, and Doubled.isIso_of_components concludes.

def RS.Doubled.evenFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] : CategoryTheory.Functor (Doubled A) A

The even-component functor X ↦ X.even.

Equations

• RS.Doubled.evenFunctor = { obj := fun (X : RS.Doubled A) => X.even, map := fun {X Y : RS.Doubled A} (f : X ⟶ Y) => RS.Doubled.evenHom f, map_id := ⋯, map_comp := ⋯ }

def RS.Doubled.oddFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] : CategoryTheory.Functor (Doubled A) A

The odd-component functor X ↦ X.odd.

Equations

• RS.Doubled.oddFunctor = { obj := fun (X : RS.Doubled A) => X.odd, map := fun {X Y : RS.Doubled A} (f : X ⟶ Y) => RS.Doubled.oddHom f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.Doubled.evenFunctor_obj {A : Type u} [CategoryTheory.Category.{v, u} A] (X : Doubled A) : evenFunctor.obj X = X.even

@[simp]

theorem RS.Doubled.oddFunctor_obj {A : Type u} [CategoryTheory.Category.{v, u} A] (X : Doubled A) : oddFunctor.obj X = X.odd

@[simp]

theorem RS.Doubled.evenFunctor_map {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (f : X ⟶ Y) : evenFunctor.map f = evenHom f

@[simp]

theorem RS.Doubled.oddFunctor_map {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (f : X ⟶ Y) : oddFunctor.map f = oddHom f

instance RS.Doubled.evenFunctorPreservesZeroMorphisms {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] : evenFunctor.PreservesZeroMorphisms

The even-component functor preserves zero morphisms.

instance RS.Doubled.oddFunctorPreservesZeroMorphisms {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] : oddFunctor.PreservesZeroMorphisms

The odd-component functor preserves zero morphisms.

instance RS.Doubled.evenFunctorPreservesKernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasKernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) evenFunctor

The even-component functor preserves kernels: the kernel of a morphism of super-objects is the componentwise one.

instance RS.Doubled.oddFunctorPreservesKernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasKernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) oddFunctor

The odd-component functor preserves kernels.

instance RS.Doubled.evenFunctorPreservesCokernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasCokernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) evenFunctor

The even-component functor preserves cokernels: the cokernel of a morphism of super-objects is the componentwise one.

instance RS.Doubled.oddFunctorPreservesCokernel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasCokernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) oddFunctor

The odd-component functor preserves cokernels.

theorem RS.Doubled.isIso_evenHom_coimageImageComparison {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.IsIso (evenHom (CategoryTheory.Abelian.coimageImageComparison f))

The even component of the coimage–image comparison is an isomorphism: it is, up to the comparison isomorphisms of the even-component functor, the coimage–image comparison of evenHom f in the abelian category A.

theorem RS.Doubled.isIso_oddHom_coimageImageComparison {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.IsIso (oddHom (CategoryTheory.Abelian.coimageImageComparison f))

The odd component of the coimage–image comparison is an isomorphism, for the same reason.

theorem RS.Doubled.isIso_coimageImageComparison {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

The coimage–image comparison of a morphism of super-objects is an isomorphism, since both of its components are.

@[instance_reducible]

instance RS.Doubled.instAbelian {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] : CategoryTheory.Abelian (Doubled A)

The doubling of an abelian category is abelian, with componentwise kernels, cokernels and biproducts.

Equations

• RS.Doubled.instAbelian = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso

theorem RS.Doubled.hasFiniteBiproducts {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] : CategoryTheory.Limits.HasFiniteBiproducts (Doubled A)

The doubling has finite biproducts.