@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryBiproductData.mkOfMaps {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroMorphisms C] (P Q pt : C) (fst : pt ⟶ P) (snd : pt ⟶ Q) (inl : P ⟶ pt) (inr : Q ⟶ pt) (pair : (X : C) → (X ⟶ P) → (X ⟶ Q) → (X ⟶ pt)) (copair : (X : C) → (P ⟶ X) → (Q ⟶ X) → (pt ⟶ X)) (inl_fst : CategoryStruct.comp inl fst = CategoryStruct.id P := by aesop) (inl_snd : CategoryStruct.comp inl snd = 0 := by aesop) (inr_fst : CategoryStruct.comp inr fst = 0 := by aesop) (inr_snd : CategoryStruct.comp inr snd = CategoryStruct.id Q := by aesop) (pair_fst : ∀ (X : C) (f : X ⟶ P) (g : X ⟶ Q), CategoryStruct.comp (pair X f g) fst = f := by aesop) (pair_snd : ∀ (X : C) (f : X ⟶ P) (g : X ⟶ Q), CategoryStruct.comp (pair X f g) snd = g := by aesop) (inl_copair : ∀ (X : C) (f : P ⟶ X) (g : Q ⟶ X), CategoryStruct.comp inl (copair X f g) = f := by aesop) (inr_copair : ∀ (X : C) (f : P ⟶ X) (g : Q ⟶ X), CategoryStruct.comp inr (copair X f g) = g := by aesop) (pair_eta : ∀ (X : C) (h : X ⟶ pt), pair X (CategoryStruct.comp h fst) (CategoryStruct.comp h snd) = h := by aesop) (copair_eta : ∀ (X : C) (h : pt ⟶ X), copair X (CategoryStruct.comp inl h) (CategoryStruct.comp inr h) = h := by aesop) : BinaryBiproductData P Q

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryBiproductData.mkOfProduct {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (P Q pt : C) (fst : pt ⟶ P) (snd : pt ⟶ Q) (pair : (X : C) → (X ⟶ P) → (X ⟶ Q) → (X ⟶ pt)) (pair_fst : ∀ (X : C) (f : X ⟶ P) (g : X ⟶ Q), CategoryStruct.comp (pair X f g) fst = f := by aesop) (pair_snd : ∀ (X : C) (f : X ⟶ P) (g : X ⟶ Q), CategoryStruct.comp (pair X f g) snd = g := by aesop) (pair_eta : ∀ (X : C) (h : X ⟶ pt), pair X (CategoryStruct.comp h fst) (CategoryStruct.comp h snd) = h := by aesop) : BinaryBiproductData P Q

In a preadditive category, you can construct a binary biproduct out of a product.

Equations

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

class ComputableBinaryBiproduct (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Type (max u_1 u_2)

• computableBinaryBiproductData (P Q : C) : CategoryTheory.Limits.BinaryBiproductData P Q

instance instHasBinaryBiproducts_aInfinity {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] : CategoryTheory.Limits.HasBinaryBiproducts C

If C has computable biproducuts, it also has noncomputable biproducts.

@[reducible, inline]

abbrev cbicone {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] (X Y : C) : CategoryTheory.Limits.BinaryBicone X Y

Equations

• cbicone X Y = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).bicone

@[simp]

theorem ComputableBinaryBiproduct.bicone_computableBinaryBiproductData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] (X Y : C) : (computableBinaryBiproductData X Y).bicone = cbicone X Y

def isBilimit_cbicone {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] (X Y : C) : (cbicone X Y).IsBilimit

Equations

• isBilimit_cbicone X Y = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).isBilimit

def cbiprod {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] (X Y : C) : C

Computable version of CategoryTheory.Limits.biprod.

Equations

• X ⊞ᶜ Y = (cbicone X Y).pt

def «term_⊞ᶜ_» : Lean.TrailingParserDescr

Computable version of CategoryTheory.Limits.biprod.

Equations

• «term_⊞ᶜ_» = Lean.ParserDescr.trailingNode `«term_⊞ᶜ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊞ᶜ ") (Lean.ParserDescr.cat `term 66))

@[reducible, inline]

abbrev cbiprod.fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] {X Y : C} : X ⊞ᶜ Y ⟶ X

Equations

• cbiprod.fst = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).bicone.fst

@[reducible, inline]

abbrev cbiprod.snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] {X Y : C} : X ⊞ᶜ Y ⟶ Y

Equations

• cbiprod.snd = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).bicone.snd

@[reducible, inline]

abbrev cbiprod.inl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] {X Y : C} : X ⟶ X ⊞ᶜ Y

Equations

• cbiprod.inl = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).bicone.inl

@[reducible, inline]

abbrev cbiprod.inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] {X Y : C} : Y ⟶ X ⊞ᶜ Y

Equations

• cbiprod.inr = (ComputableBinaryBiproduct.computableBinaryBiproductData X Y).bicone.inr

noncomputable def cbiprod_iso_biprod {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] (X Y : C) : X ⊞ᶜ Y ≅ X ⊞ Y

Equations

• cbiprod_iso_biprod X Y = sorry

class HasExplicitZeroObject (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Type (max u_1 u_2)

• zero : C
• uniqueTo (Y : C) : Unique (𝟎 ⟶ Y)
• uniqueFrom (Y : C) : Unique (Y ⟶ 𝟎)

def «term𝟎» : Lean.ParserDescr

Equations

• «term𝟎» = Lean.ParserDescr.node `«term𝟎» 1024 (Lean.ParserDescr.symbol "𝟎")

@[implicit_reducible]

instance instUniqueHomZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] (Y : C) : Unique (𝟎 ⟶ Y)

Equations

• instUniqueHomZero Y = HasExplicitZeroObject.uniqueTo Y

@[implicit_reducible]

instance instUniqueHomZero_1 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] (Y : C) : Unique (Y ⟶ 𝟎)

Equations

• instUniqueHomZero_1 Y = HasExplicitZeroObject.uniqueFrom Y

def explicitZeroTo {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] (Y : C) : 𝟎 ⟶ Y

Equations

• explicitZeroTo Y = default

def explicitZeroFrom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] (Y : C) : Y ⟶ 𝟎

Equations

• explicitZeroFrom Y = default

theorem explicitZeroTo_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Y : C) : explicitZeroTo Y = 0

theorem explicitZeroFrom_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Y : C) : explicitZeroFrom Y = 0

theorem isZero_explicitZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] : CategoryTheory.Limits.IsZero 𝟎

@[reducible, inline]

abbrev HasExplicitZeroObject.mkOfPreadditive (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] (zero : C) (h₁ : ∀ (Y : C) (h : zero ⟶ Y), h = 0) (h₂ : ∀ (Y : C) (h : Y ⟶ zero), h = 0) : HasExplicitZeroObject C

Special constructor for preadditive categories

Equations

• HasExplicitZeroObject.mkOfPreadditive C zero h₁ h₂ = { zero := zero, uniqueTo := fun (Y : C) => { default := 0, uniq := ⋯ }, uniqueFrom := fun (Y : C) => { default := 0, uniq := ⋯ } }

instance instHasZeroObject_aInfinity {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [HasExplicitZeroObject C] : CategoryTheory.Limits.HasZeroObject C

def List.cbiprod {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [ComputableBinaryBiproduct C] [HasExplicitZeroObject C] : List C → C

Equations

• List.cbiprod = List.foldl (fun (x1 x2 : C) => x1 ⊞ᶜ x2) 𝟎