Deterministic Morphisms in Copy-Discard Categories

Morphisms that preserve the copy operation perfectly.

A morphism f : X → Y is deterministic if copying then applying f to both copies equals applying f then copying: f ≫ Δ[Y] = Δ[X] ≫ (f ⊗ f).

In probabilistic settings, these are morphisms without randomness. In cartesian categories, all morphisms are deterministic.

Main definitions

• Deterministic - Type class for morphisms that preserve copying

Main results

• Identity morphisms are deterministic
• Composition of deterministic morphisms is deterministic

Tags

deterministic, copy-discard category, comonoid morphism

@[reducible, inline]

abbrev CategoryTheory.Deterministic {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [CopyDiscardCategory C] {X Y : C} (f : X ⟶ Y) : Prop

A morphism is deterministic if it preserves the comonoid structure.

In probabilistic contexts, these are morphisms without randomness.

Equations

• CategoryTheory.Deterministic f = CategoryTheory.IsComonHom f

theorem CategoryTheory.Deterministic.copy_natural {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [CopyDiscardCategory C] {X Y : C} (f : X ⟶ Y) [Deterministic f] : CategoryStruct.comp f ComonObj.comul = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom f f)

Deterministic morphisms commute with copying.

theorem CategoryTheory.Deterministic.discard_natural {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [CopyDiscardCategory C] {X Y : C} (f : X ⟶ Y) [Deterministic f] : CategoryStruct.comp f ComonObj.counit = ComonObj.counit

Deterministic morphisms commute with discarding.