The ℤ/2-graded doubling of a category

Deligne 2.11's device: the category of super-objects over an ambient category A. An object is a pair of objects of A, the even and odd components; a morphism is a pair of component morphisms. The graded tensor product mixes the components in the usual super pattern, the braiding carries the Koszul sign -1 on the odd⊗odd block, and the odd copy of the unit provides an odd invertible object — exactly the hypothesis pair of Deligne 2.9 — to a category that may lack one.

This module mirrors, at the abstract level, the concrete SuperVect construction of RS/Definitions.lean: the same component bookkeeping, with binary biproducts in place of products of vector spaces.

The monoidal coherences are not proved by hand: the summing functor Doubled A ⥤ A, X ↦ X.even ⊞ X.odd, is faithful, and CategoryTheory.Monoidal.induced transports the pentagon and triangle from A along it. The braiding coherences, which the Koszul sign prevents from transporting, are discharged by componentwise matrix checks against the distributor calculus set up in the Distributors section.

structure RS.Doubled (A : Type u) : Type u

A super-object over A: a pair of objects of A, thought of as the even and odd graded components.

• even : A

  The even component.

• odd : A

  The odd component.

structure RS.Doubled.Hom {A : Type u} [CategoryTheory.Category.{v, u} A] (X Y : Doubled A) : Type v

A morphism of super-objects: a pair of component morphisms, preserving the grading.

• even : X.even ⟶ Y.even

  The even component of the morphism.

• odd : X.odd ⟶ Y.odd

  The odd component of the morphism.

theorem RS.Doubled.Hom.ext_iff {A : Type u} {inst✝ : CategoryTheory.Category.{v, u} A} {X Y : Doubled A} {x y : X.Hom Y} : x = y ↔ x.even = y.even ∧ x.odd = y.odd

theorem RS.Doubled.Hom.ext {A : Type u} {inst✝ : CategoryTheory.Category.{v, u} A} {X Y : Doubled A} {x y : X.Hom Y} (even : x.even = y.even) (odd : x.odd = y.odd) : x = y

@[instance_reducible]

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

Super-objects form a category with componentwise identities and composition.

Equations

• One or more equations did not get rendered due to their size.

def RS.Doubled.evenHom {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (f : X ⟶ Y) : X.even ⟶ Y.even

The even component of a morphism of super-objects.

Equations

• RS.Doubled.evenHom f = f.even

def RS.Doubled.oddHom {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (f : X ⟶ Y) : X.odd ⟶ Y.odd

The odd component of a morphism of super-objects.

Equations

• RS.Doubled.oddHom f = f.odd

theorem RS.Doubled.hom_ext {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} {f g : X ⟶ Y} (he : evenHom f = evenHom g) (ho : oddHom f = oddHom g) : f = g

Morphisms of super-objects agreeing in both components are equal.

theorem RS.Doubled.hom_ext_iff {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} {f g : X ⟶ Y} : f = g ↔ evenHom f = evenHom g ∧ oddHom f = oddHom g

def RS.Doubled.homMk {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (fe : X.even ⟶ Y.even) (fo : X.odd ⟶ Y.odd) : X ⟶ Y

A morphism of super-objects from a pair of component morphisms.

Equations

• RS.Doubled.homMk fe fo = { even := fe, odd := fo }

@[simp]

theorem RS.Doubled.evenHom_homMk {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (fe : X.even ⟶ Y.even) (fo : X.odd ⟶ Y.odd) : evenHom (homMk fe fo) = fe

@[simp]

theorem RS.Doubled.oddHom_homMk {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (fe : X.even ⟶ Y.even) (fo : X.odd ⟶ Y.odd) : oddHom (homMk fe fo) = fo

@[simp]

theorem RS.Doubled.evenHom_id {A : Type u} [CategoryTheory.Category.{v, u} A] (X : Doubled A) : evenHom (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.even

@[simp]

theorem RS.Doubled.oddHom_id {A : Type u} [CategoryTheory.Category.{v, u} A] (X : Doubled A) : oddHom (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.odd

@[simp]

theorem RS.Doubled.evenHom_comp {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y Z : Doubled A} (f : X ⟶ Y) (g : Y ⟶ Z) : evenHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (evenHom f) (evenHom g)

@[simp]

theorem RS.Doubled.oddHom_comp {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y Z : Doubled A} (f : X ⟶ Y) (g : Y ⟶ Z) : oddHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (oddHom f) (oddHom g)

def RS.Doubled.isoMk {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (e : X.even ≅ Y.even) (o : X.odd ≅ Y.odd) : X ≅ Y

An isomorphism of super-objects from a pair of component isomorphisms.

Equations

• RS.Doubled.isoMk e o = { hom := RS.Doubled.homMk e.hom o.hom, inv := RS.Doubled.homMk e.inv o.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RS.Doubled.isoMk_inv {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (e : X.even ≅ Y.even) (o : X.odd ≅ Y.odd) : (isoMk e o).inv = homMk e.inv o.inv

@[simp]

theorem RS.Doubled.isoMk_hom {A : Type u} [CategoryTheory.Category.{v, u} A] {X Y : Doubled A} (e : X.even ≅ Y.even) (o : X.odd ≅ Y.odd) : (isoMk e o).hom = homMk e.hom o.hom

@[instance_reducible]

instance RS.Doubled.homZero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (X Y : Doubled A) : Zero (X ⟶ Y)

The componentwise zero morphism.

Equations

• X.homZero Y = { zero := RS.Doubled.homMk 0 0 }

@[instance_reducible]

instance RS.Doubled.homAdd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (X Y : Doubled A) : Add (X ⟶ Y)

Componentwise addition of morphisms.

Equations

• X.homAdd Y = { add := fun (f g : X ⟶ Y) => RS.Doubled.homMk (RS.Doubled.evenHom f + RS.Doubled.evenHom g) (RS.Doubled.oddHom f + RS.Doubled.oddHom g) }

@[instance_reducible]

instance RS.Doubled.homNeg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (X Y : Doubled A) : Neg (X ⟶ Y)

Componentwise negation of morphisms.

Equations

• X.homNeg Y = { neg := fun (f : X ⟶ Y) => RS.Doubled.homMk (-RS.Doubled.evenHom f) (-RS.Doubled.oddHom f) }

@[instance_reducible]

instance RS.Doubled.homAddCommGroup {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (X Y : Doubled A) : AddCommGroup (X ⟶ Y)

The componentwise additive group of morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Doubled.evenHom_add {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} (f g : X ⟶ Y) : evenHom (f + g) = evenHom f + evenHom g

@[simp]

theorem RS.Doubled.oddHom_add {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} (f g : X ⟶ Y) : oddHom (f + g) = oddHom f + oddHom g

@[simp]

theorem RS.Doubled.evenHom_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} : evenHom 0 = 0

@[simp]

theorem RS.Doubled.oddHom_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} : oddHom 0 = 0

@[simp]

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

@[simp]

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

@[simp]

theorem RS.Doubled.evenHom_sub {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} (f g : X ⟶ Y) : evenHom (f - g) = evenHom f - evenHom g

@[simp]

theorem RS.Doubled.oddHom_sub {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] {X Y : Doubled A} (f g : X ⟶ Y) : oddHom (f - g) = oddHom f - oddHom g

@[instance_reducible]

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

The doubling of a preadditive category is preadditive, componentwise.

Equations

• RS.Doubled.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

theorem RS.Doubled.isZero {A : Type u} [CategoryTheory.Category.{v, u} A] (X : Doubled A) (he : CategoryTheory.Limits.IsZero X.even) (ho : CategoryTheory.Limits.IsZero X.odd) : CategoryTheory.Limits.IsZero X

A super-object with two zero components is a zero object.

instance RS.Doubled.instHasZeroObject {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Limits.HasZeroObject (Doubled A)

The doubling of a category with a zero object has a zero object, with both components zero.

@[instance_reducible]

instance RS.Doubled.homModule {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : Doubled A) : Module ℂ (X ⟶ Y)

The componentwise ℂ-module of morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Doubled.evenHom_smul {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] {X Y : Doubled A} (c : ℂ) (f : X ⟶ Y) : evenHom (c • f) = c • evenHom f

@[simp]

theorem RS.Doubled.oddHom_smul {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] {X Y : Doubled A} (c : ℂ) (f : X ⟶ Y) : oddHom (c • f) = c • oddHom f

@[instance_reducible]

instance RS.Doubled.instLinear {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] : CategoryTheory.Linear ℂ (Doubled A)

The doubling of a ℂ-linear category is ℂ-linear, componentwise.

Equations

• RS.Doubled.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

noncomputable def RS.Doubled.descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.MonoidalCategoryStruct.tensorObj (M ⊞ N) Z ⟶ T

The matrix map out of a right-whiskered binary biproduct.

Equations

• RS.Doubled.descRight f g = CategoryTheory.CategoryStruct.comp (RS.biprodTensorIso M N Z).hom (CategoryTheory.Limits.biprod.desc f g)

noncomputable def RS.Doubled.descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (M ⊞ N) ⟶ T

The matrix map out of a left-whiskered binary biproduct.

Equations

• RS.Doubled.descLeft f g = CategoryTheory.CategoryStruct.comp (RS.tensorBiprodIso X M N).hom (CategoryTheory.Limits.biprod.desc f g)

@[simp]

theorem RS.Doubled.inl_descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (descRight f g) = f

@[simp]

theorem RS.Doubled.inl_descRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) {Z✝ : A} (h : T ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (CategoryTheory.CategoryStruct.comp (descRight f g) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem RS.Doubled.inr_descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (descRight f g) = g

@[simp]

theorem RS.Doubled.inr_descRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) {Z✝ : A} (h : T ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (CategoryTheory.CategoryStruct.comp (descRight f g) h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem RS.Doubled.inl_descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (descLeft f g) = f

@[simp]

theorem RS.Doubled.inl_descLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) {Z : A} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp (descLeft f g) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem RS.Doubled.inr_descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (descLeft f g) = g

@[simp]

theorem RS.Doubled.inr_descLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) {Z : A} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (CategoryTheory.CategoryStruct.comp (descLeft f g) h) = CategoryTheory.CategoryStruct.comp g h

theorem RS.Doubled.inl_id_descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.id Z)) (descRight f g) = f

inl_descRight in tensor-of-morphisms shape. Not a simp lemma: ⊗ₘ 𝟙 normalises to the whiskering, where inl_descRight already applies.

theorem RS.Doubled.inl_id_descRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) {Z✝ : A} (h : T ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (descRight f g) h) = CategoryTheory.CategoryStruct.comp f h

inl_descRight in tensor-of-morphisms shape. Not a simp lemma: ⊗ₘ 𝟙 normalises to the whiskering, where inl_descRight already applies.

theorem RS.Doubled.inr_id_descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.id Z)) (descRight f g) = g

inr_descRight in tensor-of-morphisms shape. Not a simp lemma: ⊗ₘ 𝟙 normalises to the whiskering, where inr_descRight already applies.

theorem RS.Doubled.inr_id_descRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) {Z✝ : A} (h : T ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (descRight f g) h) = CategoryTheory.CategoryStruct.comp g h

inr_descRight in tensor-of-morphisms shape. Not a simp lemma: ⊗ₘ 𝟙 normalises to the whiskering, where inr_descRight already applies.

theorem RS.Doubled.id_inl_descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) CategoryTheory.Limits.biprod.inl) (descLeft f g) = f

inl_descLeft in tensor-of-morphisms shape. Not a simp lemma: 𝟙 ⊗ₘ normalises to the whiskering, where inl_descLeft already applies.

theorem RS.Doubled.id_inl_descLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) {Z : A} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp (descLeft f g) h) = CategoryTheory.CategoryStruct.comp f h

inl_descLeft in tensor-of-morphisms shape. Not a simp lemma: 𝟙 ⊗ₘ normalises to the whiskering, where inl_descLeft already applies.

theorem RS.Doubled.id_inr_descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) CategoryTheory.Limits.biprod.inr) (descLeft f g) = g

inr_descLeft in tensor-of-morphisms shape. Not a simp lemma: 𝟙 ⊗ₘ normalises to the whiskering, where inr_descLeft already applies.

theorem RS.Doubled.id_inr_descLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (g : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) {Z : A} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) CategoryTheory.Limits.biprod.inr) (CategoryTheory.CategoryStruct.comp (descLeft f g) h) = CategoryTheory.CategoryStruct.comp g h

inr_descLeft in tensor-of-morphisms shape. Not a simp lemma: 𝟙 ⊗ₘ normalises to the whiskering, where inr_descLeft already applies.

@[simp]

theorem RS.Doubled.inl_map_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N M' N' Z : A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.map f g) Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z)

@[simp]

theorem RS.Doubled.inl_map_whiskerRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N M' N' Z : A} (f : M ⟶ M') (g : N ⟶ N') {Z✝ : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (M' ⊞ N') Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.map f g) Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) h)

@[simp]

theorem RS.Doubled.inr_map_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N M' N' Z : A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.map f g) Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z)

@[simp]

theorem RS.Doubled.inr_map_whiskerRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N M' N' Z : A} (f : M ⟶ M') (g : N ⟶ N') {Z✝ : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (M' ⊞ N') Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.map f g) Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) h)

@[simp]

theorem RS.Doubled.inl_desc_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N T Z : A} (f : M ⟶ T) (g : N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.desc f g) Z) = CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z

@[simp]

theorem RS.Doubled.inl_desc_whiskerRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N T Z : A} (f : M ⟶ T) (g : N ⟶ T) {Z✝ : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj T Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.desc f g) Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h

@[simp]

theorem RS.Doubled.inr_desc_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N T Z : A} (f : M ⟶ T) (g : N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.desc f g) Z) = CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z

@[simp]

theorem RS.Doubled.inr_desc_whiskerRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N T Z : A} (f : M ⟶ T) (g : N ⟶ T) {Z✝ : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj T Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.desc f g) Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) h

@[simp]

theorem RS.Doubled.inl_map_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N M' N' : A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl)

@[simp]

theorem RS.Doubled.inl_map_whiskerLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N M' N' : A} (f : M ⟶ M') (g : N ⟶ N') {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (M' ⊞ N') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) h)

@[simp]

theorem RS.Doubled.inr_map_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N M' N' : A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr)

@[simp]

theorem RS.Doubled.inr_map_whiskerLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N M' N' : A} (f : M ⟶ M') (g : N ⟶ N') {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (M' ⊞ N') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) h)

@[simp]

theorem RS.Doubled.inl_desc_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : M ⟶ T) (g : N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.desc f g)) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f

@[simp]

theorem RS.Doubled.inl_desc_whiskerLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : M ⟶ T) (g : N ⟶ T) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.desc f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) h

@[simp]

theorem RS.Doubled.inr_desc_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : M ⟶ T) (g : N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.desc f g)) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g

@[simp]

theorem RS.Doubled.inr_desc_whiskerLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} (f : M ⟶ T) (g : N ⟶ T) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.desc f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) h

@[simp]

theorem RS.Doubled.whiskerLeft_lift_descLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T U : A} (f : U ⟶ M) (g : U ⟶ N) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.lift f g)) (descLeft h k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) h + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) k

@[simp]

theorem RS.Doubled.whiskerLeft_lift_descLeft_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T U : A} (f : U ⟶ M) (g : U ⟶ N) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X M ⟶ T) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj X N ⟶ T) {Z : A} (h✝ : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biprod.lift f g)) (CategoryTheory.CategoryStruct.comp (descLeft h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) h + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) k) h✝

@[simp]

theorem RS.Doubled.lift_whiskerRight_descRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T U : A} (f : U ⟶ M) (g : U ⟶ N) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.lift f g) Z) (descRight h k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) k

@[simp]

theorem RS.Doubled.lift_whiskerRight_descRight_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T U : A} (f : U ⟶ M) (g : U ⟶ N) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M Z ⟶ T) (k : CategoryTheory.MonoidalCategoryStruct.tensorObj N Z ⟶ T) {Z✝ : A} (h✝ : T ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.lift f g) Z) (CategoryTheory.CategoryStruct.comp (descRight h k) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) k) h✝

theorem RS.Doubled.tensorRight_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N Z T : A} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (M ⊞ N) Z ⟶ T} (h₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl Z) g) (h₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr Z) g) : f = g

Maps out of a right-whiskered binary biproduct are determined by their composites with the whiskered inclusions.

theorem RS.Doubled.tensorLeft_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X M N T : A} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (M ⊞ N) ⟶ T} (h₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inl) g) (h₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.biprod.inr) g) : f = g

Maps out of a left-whiskered binary biproduct are determined by their composites with the whiskered inclusions.

@[reducible, inline]

noncomputable abbrev RS.Doubled.tensorObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y : Doubled A) : Doubled A

The graded tensor product of super-objects: parities add, so each component of the product is a biproduct of two mixed blocks.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Doubled.tensorObj_even {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y : Doubled A) : (X.tensorObj Y).even = (CategoryTheory.MonoidalCategoryStruct.tensorObj X.even Y.even ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj X.odd Y.odd)

@[simp]

theorem RS.Doubled.tensorObj_odd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y : Doubled A) : (X.tensorObj Y).odd = (CategoryTheory.MonoidalCategoryStruct.tensorObj X.even Y.odd ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj X.odd Y.even)

noncomputable def RS.Doubled.tensorHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X₁ Y₁ X₂ Y₂ : Doubled A} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : X₁.tensorObj X₂ ⟶ Y₁.tensorObj Y₂

The graded tensor product of morphisms, blockwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : Doubled A) {Y₁ Y₂ : Doubled A} (g : Y₁ ⟶ Y₂) : X.tensorObj Y₁ ⟶ X.tensorObj Y₂

Left whiskering of super-objects, blockwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X₁ X₂ : Doubled A} (f : X₁ ⟶ X₂) (Y : Doubled A) : X₁.tensorObj Y ⟶ X₂.tensorObj Y

Right whiskering of super-objects, blockwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.assocEven {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y Z : Doubled A) : ((X.tensorObj Y).tensorObj Z).even ≅ (X.tensorObj (Y.tensorObj Z)).even

The even component of the associator: each of the four parity blocks re-associates through A's associator and is routed to the matching block of the right-nested product.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.assocOdd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y Z : Doubled A) : ((X.tensorObj Y).tensorObj Z).odd ≅ (X.tensorObj (Y.tensorObj Z)).odd

The odd component of the associator.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev RS.Doubled.total {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] : CategoryTheory.Functor (Doubled A) A

The summing functor X ↦ X.even ⊞ X.odd. It is faithful, and the monoidal coherences of the doubling are induced along it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Doubled.total_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : Doubled A) : total.obj X = (X.even ⊞ X.odd)

@[simp]

theorem RS.Doubled.total_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {X Y : Doubled A} (f : X ⟶ Y) : total.map f = CategoryTheory.Limits.biprod.map (evenHom f) (oddHom f)

instance RS.Doubled.instFaithfulTotal {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] : total.Faithful

The summing functor is faithful: both components are recovered as matrix entries.

@[reducible, inline]

noncomputable abbrev RS.Doubled.unit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasZeroObject A] : Doubled A

The monoidal unit of the doubling: the unit of A in even degree, the zero object in odd degree.

Equations

• RS.Doubled.unit = { even := CategoryTheory.MonoidalCategoryStruct.tensorUnit A, odd := 0 }

theorem RS.Doubled.isZero_zeroTensor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasZeroObject A] (M : A) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj 0 M)

A left tensor factor which is the zero object kills the product.

theorem RS.Doubled.isZero_tensorZero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasZeroObject A] (M : A) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj M 0)

A right tensor factor which is the zero object kills the product.

noncomputable def RS.Doubled.leftUnitorComp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (M M' : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) M ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj 0 M' ≅ M

Collapse of a unit block against a zero block, in the shape of the left unitor components.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.rightUnitorComp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (M M' : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj M' 0 ≅ M

Collapse of a unit block against a zero block, in the shape of the even right unitor component.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.rightUnitorCompOdd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (M M' : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj M' 0 ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) ≅ M

Collapse of a unit block against a zero block, in the shape of the odd right unitor component.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instMonoidalCategoryStruct {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalCategoryStruct (Doubled A)

The monoidal skeleton of the doubling: graded tensor product, unit (𝟙_ A, 0), blockwise structural isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

Components of the monoidal notation

@[simp]

theorem RS.Doubled.unit_even {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A)).even = CategoryTheory.MonoidalCategoryStruct.tensorUnit A

@[simp]

theorem RS.Doubled.unit_odd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A)).odd = 0

@[simp]

theorem RS.Doubled.tensor_even {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : Doubled A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).even = (CategoryTheory.MonoidalCategoryStruct.tensorObj X.even Y.even ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj X.odd Y.odd)

@[simp]

theorem RS.Doubled.tensor_odd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : Doubled A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).odd = (CategoryTheory.MonoidalCategoryStruct.tensorObj X.even Y.odd ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj X.odd Y.even)

@[simp]

theorem RS.Doubled.evenHom_tensor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ Y₁ X₂ Y₂ : Doubled A} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : evenHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (evenHom f) (evenHom g)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (oddHom f) (oddHom g))

@[simp]

theorem RS.Doubled.oddHom_tensor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ Y₁ X₂ Y₂ : Doubled A} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : oddHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (evenHom f) (oddHom g)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (oddHom f) (evenHom g))

@[simp]

theorem RS.Doubled.evenHom_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) {Y₁ Y₂ : Doubled A} (g : Y₁ ⟶ Y₂) : evenHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.even (evenHom g)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.odd (oddHom g))

@[simp]

theorem RS.Doubled.oddHom_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) {Y₁ Y₂ : Doubled A} (g : Y₁ ⟶ Y₂) : oddHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.even (oddHom g)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.odd (evenHom g))

@[simp]

theorem RS.Doubled.evenHom_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ X₂ : Doubled A} (f : X₁ ⟶ X₂) (Y : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (evenHom f) Y.even) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (oddHom f) Y.odd)

@[simp]

theorem RS.Doubled.oddHom_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ X₂ : Doubled A} (f : X₁ ⟶ X₂) (Y : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = CategoryTheory.Limits.biprod.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (evenHom f) Y.odd) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (oddHom f) Y.even)

@[simp]

theorem RS.Doubled.evenHom_associator_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = (X.assocEven Y Z).hom

@[simp]

theorem RS.Doubled.oddHom_associator_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = (X.assocOdd Y Z).hom

@[simp]

theorem RS.Doubled.evenHom_associator_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = (X.assocEven Y Z).inv

@[simp]

theorem RS.Doubled.oddHom_associator_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = (X.assocOdd Y Z).inv

@[simp]

theorem RS.Doubled.evenHom_leftUnitor_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = (leftUnitorComp X.even X.odd).hom

@[simp]

theorem RS.Doubled.oddHom_leftUnitor_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = (leftUnitorComp X.odd X.even).hom

@[simp]

theorem RS.Doubled.evenHom_leftUnitor_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = (leftUnitorComp X.even X.odd).inv

@[simp]

theorem RS.Doubled.oddHom_leftUnitor_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = (leftUnitorComp X.odd X.even).inv

@[simp]

theorem RS.Doubled.evenHom_rightUnitor_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = (rightUnitorComp X.even X.odd).hom

@[simp]

theorem RS.Doubled.oddHom_rightUnitor_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = (rightUnitorCompOdd X.odd X.even).hom

@[simp]

theorem RS.Doubled.evenHom_rightUnitor_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : evenHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = (rightUnitorComp X.even X.odd).inv

@[simp]

theorem RS.Doubled.oddHom_rightUnitor_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : oddHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = (rightUnitorCompOdd X.odd X.even).inv

noncomputable def RS.Doubled.muIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : Doubled A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (total.obj X) (total.obj Y) ≅ total.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The multiplicative comparison of the summing functor: double distribution followed by the parity shuffle.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.epsIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ total.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A))

The unit comparison of the summing functor.

Equations

• RS.Doubled.epsIso = { hom := CategoryTheory.Limits.biprod.inl, inv := CategoryTheory.Limits.biprod.fst, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.Doubled.total_tensorHom_muIso_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ Y₁ X₂ Y₂ : Doubled A} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.CategoryStruct.comp (total.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (Y₁.muIso Y₂).inv = CategoryTheory.CategoryStruct.comp (X₁.muIso X₂).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (total.map f) (total.map g))

The summing functor intertwines the graded tensor of morphisms with the ambient tensor, through the comparison muIso.

theorem RS.Doubled.total_tensorHom_muIso_inv_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ Y₁ X₂ Y₂ : Doubled A} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Y₁.even ⊞ Y₁.odd) (Y₂.even ⊞ Y₂.odd) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (evenHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (oddHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))) (CategoryTheory.CategoryStruct.comp (Y₁.muIso Y₂).inv h) = CategoryTheory.CategoryStruct.comp (X₁.muIso X₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.biprod.map (evenHom f) (oddHom f)) (CategoryTheory.Limits.biprod.map (evenHom g) (oddHom g))) h)

The summing functor intertwines the graded tensor of morphisms with the ambient tensor, through the comparison muIso.

theorem RS.Doubled.total_whiskerLeft_muIso_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) {Y₁ Y₂ : Doubled A} (g : Y₁ ⟶ Y₂) : CategoryTheory.CategoryStruct.comp (total.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)) (X.muIso Y₂).inv = CategoryTheory.CategoryStruct.comp (X.muIso Y₁).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (total.obj X) (total.map g))

The summing functor intertwines graded left whiskering with ambient left whiskering, through the comparison muIso.

theorem RS.Doubled.total_whiskerLeft_muIso_inv_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) {Y₁ Y₂ : Doubled A} (g : Y₁ ⟶ Y₂) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.even ⊞ X.odd) (Y₂.even ⊞ Y₂.odd) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (evenHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)) (oddHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))) (CategoryTheory.CategoryStruct.comp (X.muIso Y₂).inv h) = CategoryTheory.CategoryStruct.comp (X.muIso Y₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.even ⊞ X.odd) (CategoryTheory.Limits.biprod.map (evenHom g) (oddHom g))) h)

The summing functor intertwines graded left whiskering with ambient left whiskering, through the comparison muIso.

theorem RS.Doubled.total_whiskerRight_muIso_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ X₂ : Doubled A} (f : X₁ ⟶ X₂) (Y : Doubled A) : CategoryTheory.CategoryStruct.comp (total.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)) (X₂.muIso Y).inv = CategoryTheory.CategoryStruct.comp (X₁.muIso Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (total.map f) (total.obj Y))

The summing functor intertwines graded right whiskering with ambient right whiskering, through the comparison muIso.

theorem RS.Doubled.total_whiskerRight_muIso_inv_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] {X₁ X₂ : Doubled A} (f : X₁ ⟶ X₂) (Y : Doubled A) {Z : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X₂.even ⊞ X₂.odd) (Y.even ⊞ Y.odd) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (evenHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)) (oddHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))) (CategoryTheory.CategoryStruct.comp (X₂.muIso Y).inv h) = CategoryTheory.CategoryStruct.comp (X₁.muIso Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biprod.map (evenHom f) (oddHom f)) (Y.even ⊞ Y.odd)) h)

The summing functor intertwines graded right whiskering with ambient right whiskering, through the comparison muIso.

theorem RS.Doubled.total_associator_muIso_inv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) : CategoryTheory.CategoryStruct.comp (total.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) (CategoryTheory.CategoryStruct.comp (X.muIso (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (total.obj X)) (Y.muIso Z).inv)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).muIso Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.muIso Y).inv (CategoryTheory.CategoryStruct.id (total.obj Z))) (CategoryTheory.MonoidalCategoryStruct.associator (total.obj X) (total.obj Y) (total.obj Z)).hom)

The summing functor intertwines the graded associator with the ambient associator, through the comparison muIso.

theorem RS.Doubled.total_associator_muIso_inv_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y Z : Doubled A) {Z✝ : A} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.even ⊞ X.odd) (CategoryTheory.MonoidalCategoryStruct.tensorObj (Y.even ⊞ Y.odd) (Z.even ⊞ Z.odd)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (evenHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) (oddHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) (CategoryTheory.CategoryStruct.comp (X.muIso (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (X.even ⊞ X.odd)) (Y.muIso Z).inv) h)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).muIso Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.muIso Y).inv (CategoryTheory.CategoryStruct.id (Z.even ⊞ Z.odd))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X.even ⊞ X.odd) (Y.even ⊞ Y.odd) (Z.even ⊞ Z.odd)).hom h))

The summing functor intertwines the graded associator with the ambient associator, through the comparison muIso.

noncomputable def RS.Doubled.totalInducingData {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Monoidal.InducingFunctorData total

The inducing data exhibiting the graded structural morphisms as the images of A's structural morphisms under the parity distributors.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instMonoidalCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalCategory (Doubled A)

The doubling of a monoidal category is monoidal, with the graded tensor product: the coherences are induced along the faithful summing functor.

Equations

• RS.Doubled.instMonoidalCategory = CategoryTheory.Monoidal.induced RS.Doubled.total RS.Doubled.totalInducingData

@[instance_reducible]

noncomputable instance RS.Doubled.instMonoidalTotal {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : total.Monoidal

The summing functor is monoidal.

Equations

• RS.Doubled.instMonoidalTotal = CategoryTheory.Monoidal.fromInducedMonoidal RS.Doubled.total RS.Doubled.totalInducingData

instance RS.Doubled.instMonoidalPreadditive {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalPreadditive (Doubled A)

The doubling of a monoidal preadditive category is monoidal preadditive, componentwise. Each component equation is restated (show) with its objects in literal biproduct form, so that the ambient simp lemmas apply.

instance RS.Doubled.instMonoidalLinear {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalLinear ℂ A] : CategoryTheory.MonoidalLinear ℂ (Doubled A)

The doubling of a monoidal ℂ-linear category is monoidal ℂ-linear, componentwise.

noncomputable def RS.Doubled.braidingEven {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] (X Y : Doubled A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).even ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).even

The even component of the Koszul braiding: A's braiding on each parity block, with the sign -1 on the odd⊗odd block.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.braidingOdd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] (X Y : Doubled A) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).odd ≅ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).odd

The odd component of the Koszul braiding: the two mixed blocks swap through A's braiding, with no sign.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instBraidedCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] : CategoryTheory.BraidedCategory (Doubled A)

The doubling of a symmetric category is braided, with the Koszul-signed braiding.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instSymmetricCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] : CategoryTheory.SymmetricCategory (Doubled A)

The doubling of a symmetric category is symmetric: the Koszul sign squares away.

Equations

• RS.Doubled.instSymmetricCategory = { toBraidedCategory := RS.Doubled.instBraidedCategory, symmetry := ⋯ }

theorem RS.Doubled.isZero_biprod {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] {M N : A} (hM : CategoryTheory.Limits.IsZero M) (hN : CategoryTheory.Limits.IsZero N) : CategoryTheory.Limits.IsZero (M ⊞ N)

A biproduct of two zero objects is a zero object.

@[reducible, inline]

noncomputable abbrev RS.Doubled.evenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Functor A (Doubled A)

The even embedding X ↦ (X, 0).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Doubled.evenEmbed_obj_even {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] (X : A) : (evenEmbed.obj X).even = X

@[simp]

theorem RS.Doubled.evenEmbed_obj_odd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] (X : A) : (evenEmbed.obj X).odd = 0

@[simp]

theorem RS.Doubled.evenHom_evenEmbed_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] {X Y : A} (f : X ⟶ Y) : evenHom (evenEmbed.map f) = f

instance RS.Doubled.instFaithfulEvenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed.Faithful

The even embedding is faithful.

instance RS.Doubled.instFullEvenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed.Full

The even embedding is full.

instance RS.Doubled.instAdditiveEvenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed.Additive

The even embedding is additive.

instance RS.Doubled.instLinearComplexEvenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.Linear ℂ A] : CategoryTheory.Functor.Linear ℂ evenEmbed

The even embedding is ℂ-linear.

noncomputable def RS.Doubled.evenEmbedTensorIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (evenEmbed.obj X) (evenEmbed.obj Y) ≅ evenEmbed.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The even embedding is monoidal up to isomorphism: the graded tensor of two even objects collapses to the even tensor.

Equations

• RS.Doubled.evenEmbedTensorIso X Y = RS.Doubled.isoMk (CategoryTheory.Limits.isoBiprodZero ⋯).symm (⋯.iso ⋯)

theorem RS.Doubled.evenEmbedTensorIso_braided {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] (X Y : A) : CategoryTheory.CategoryStruct.comp (β_ (evenEmbed.obj X) (evenEmbed.obj Y)).hom (evenEmbedTensorIso Y X).hom = CategoryTheory.CategoryStruct.comp (evenEmbedTensorIso X Y).hom (evenEmbed.map (β_ X Y).hom)

The even embedding intertwines the braidings through evenEmbedTensorIso.

noncomputable def RS.Doubled.evenEmbedUnitIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A) ≅ evenEmbed.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

The unit comparison of the even embedding: definitional.

Equations

• RS.Doubled.evenEmbedUnitIso = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (RS.Doubled A))

@[reducible, inline]

noncomputable abbrev RS.Doubled.oddUnit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasZeroObject A] : Doubled A

The odd unit: the unit of A placed in odd degree. Together with oddUnitSq and braiding_oddUnit this is exactly the invertible odd object required by Deligne 2.9.

Equations

• RS.Doubled.oddUnit = { even := 0, odd := CategoryTheory.MonoidalCategoryStruct.tensorUnit A }

@[simp]

theorem RS.Doubled.oddUnit_even {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasZeroObject A] : oddUnit.even = 0

@[simp]

theorem RS.Doubled.oddUnit_odd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasZeroObject A] : oddUnit.odd = CategoryTheory.MonoidalCategoryStruct.tensorUnit A

noncomputable def RS.Doubled.oddUnitSq {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.MonoidalCategoryStruct.tensorObj oddUnit oddUnit ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (Doubled A)

The odd unit squares to the monoidal unit.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Doubled.braiding_oddUnit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] : (β_ oddUnit oddUnit).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj oddUnit oddUnit)

The braiding of the odd unit with itself is -1: the Koszul sign made visible on a single object.

noncomputable def RS.Doubled.binaryBicone {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X Y : Doubled A) : CategoryTheory.Limits.BinaryBicone X Y

The componentwise binary bicone on a pair of super-objects.

Equations

• One or more equations did not get rendered due to their size.

instance RS.Doubled.instHasBinaryBiproducts {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] : CategoryTheory.Limits.HasBinaryBiproducts (Doubled A)

The doubling has componentwise binary biproducts.

instance RS.Doubled.instHasFiniteProducts {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Limits.HasFiniteProducts (Doubled A)

The doubling has finite products: it has a zero object and componentwise binary biproducts.

noncomputable def RS.Doubled.decomposition {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X : Doubled A) : X ≅ evenEmbed.obj X.even ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj oddUnit (evenEmbed.obj X.odd)

Every super-object is the biproduct of its even part and the odd-unit twist of its odd part: the decomposition through which Schur-vanishing transports from A to the doubling.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.kernelFork {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasKernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.KernelFork f

The componentwise kernel fork of a morphism of super-objects.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.kernelForkIsLimit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasKernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.IsLimit (kernelFork f)

The componentwise kernel fork is limiting.

Equations

• One or more equations did not get rendered due to their size.

instance RS.Doubled.instHasKernels {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasKernels A] : CategoryTheory.Limits.HasKernels (Doubled A)

The doubling has componentwise kernels.

noncomputable def RS.Doubled.cokernelCofork {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasCokernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.CokernelCofork f

The componentwise cokernel cofork of a morphism of super-objects.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Doubled.cokernelCoforkIsColimit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasCokernels A] {X Y : Doubled A} (f : X ⟶ Y) : CategoryTheory.Limits.IsColimit (cokernelCofork f)

The componentwise cokernel cofork is colimiting.

Equations

• One or more equations did not get rendered due to their size.

instance RS.Doubled.instHasCokernels {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasCokernels A] : CategoryTheory.Limits.HasCokernels (Doubled A)

The doubling has componentwise cokernels.

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

A morphism of super-objects whose two components are isomorphisms is an isomorphism.

@[reducible]

noncomputable def RS.Doubled.exactPairing {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (P Q : Doubled A) [CategoryTheory.ExactPairing P.even Q.even] [CategoryTheory.ExactPairing P.odd Q.odd] : CategoryTheory.ExactPairing P Q

Componentwise exact pairings pair the doubled objects: the evaluations and coevaluations act blockwise on matching parities, and the odd components vanish.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instRightRigidCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.RightRigidCategory A] : CategoryTheory.RightRigidCategory (Doubled A)

The doubling of a right rigid category is right rigid, with componentwise duals.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.Doubled.instLeftRigidCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.LeftRigidCategory A] : CategoryTheory.LeftRigidCategory (Doubled A)

The doubling of a left rigid category is left rigid, with componentwise duals.

Equations

• RS.Doubled.instLeftRigidCategory = { leftDual := fun (X : RS.Doubled A) => { leftDual := { even := ᘁX.even, odd := ᘁX.odd }, exact := { even := ᘁX.even, odd := ᘁX.odd }.exactPairing X } }

@[instance_reducible]

noncomputable instance RS.Doubled.instRigidCategory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.RigidCategory A] : CategoryTheory.RigidCategory (Doubled A)

The doubling of a rigid category is rigid.

Equations

• RS.Doubled.instRigidCategory = { toRightRigidCategory := RS.Doubled.instRightRigidCategory, toLeftRigidCategory := RS.Doubled.instLeftRigidCategory }