Affine Monoidal Categories

An affine monoidal category has a natural "discard" morphism del X : X ⟶ 𝟙_ C for every object, satisfying naturality (f ≫ del Y = del X). This is the dual notion to having a "copy" morphism; in a cocartesian setting it means every computation can be discarded.

Main definitions

• AffineMonoidalCategory — abstract class with del morphism
• KlSPComp instance — discard by mapping to SDistr.fail

Duality

• Every SemiCartesianMonoidalCategory is affine (via toUnit)
• Every SemiCocartesianMonoidalCategory has a dual "co-affine" structure (fromUnit)

class CategoryTheory.AffineMonoidalCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : Type (max u v)

An affine monoidal category has a natural discard morphism del X : X ⟶ 𝟙_ C for every object. Naturality means f ≫ del Y = del X.

• del (X : C) : X ⟶ MonoidalCategoryStruct.tensorUnit C

  The discard morphism.

• del_unit : del (MonoidalCategoryStruct.tensorUnit C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

  Discarding the unit is the identity.

• del_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (del Y) = del X

  Discard is natural: composing with any morphism then discarding equals discarding directly.

@[simp]

theorem CategoryTheory.AffineMonoidalCategory.del_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [AffineMonoidalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (del Y) = del X

@[simp]

theorem CategoryTheory.AffineMonoidalCategory.del_comp_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [AffineMonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (del Y) h) = CategoryStruct.comp (del X) h

@[simp]

theorem CategoryTheory.AffineMonoidalCategory.del_unit' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [AffineMonoidalCategory C] : del (MonoidalCategoryStruct.tensorUnit C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

Duality: SemiCartesian → Affine

@[implicit_reducible]

noncomputable instance CategoryTheory.AffineMonoidalCategory.ofSemiCartesian (C : Type u) [Category.{v, u} C] [SemiCartesianMonoidalCategory C] : AffineMonoidalCategory C

Every semicartesian monoidal category is affine (del = toUnit).

Equations

• CategoryTheory.AffineMonoidalCategory.ofSemiCartesian C = { del := CategoryTheory.SemiCartesianMonoidalCategory.toUnit, del_unit := ⋯, del_naturality := ⋯ }

Concrete instance: KlSPComp is affine

noncomputable def CatCrypt.Core.KlSPComp.klDel (α : KlSPComp) : α ⟶ have this := Empty; this

Discard morphism: maps any value to the failing computation on Empty.

Equations

• α.klDel x✝ = CatCrypt.Core.SPComp.fail

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instAffineMonoidalCategory : CategoryTheory.AffineMonoidalCategory KlSPComp

Equations

• CatCrypt.Core.KlSPComp.instAffineMonoidalCategory = { del := CatCrypt.Core.KlSPComp.klDel, del_unit := CatCrypt.Core.KlSPComp.klDel_unit✝, del_naturality := ⋯ }