Combinational circuit category

References

• [Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits][Ghica2025]

structure Circuit.CombinationalCircuitCategory (V : Type u_1) (G : Type u_2) : Type

Category of combinational circuits.

• of :: (
• obj : ℕ

  The number of wires of this object.

• )

@[implicit_reducible]

instance Circuit.instOfNatCombinationalCircuitCategory {V : Type u_1} {G : Type u_2} {n : ℕ} : OfNat (CombinationalCircuitCategory V G) n

Equations

• Circuit.instOfNatCombinationalCircuitCategory = { ofNat := { obj := n } }

def Circuit.CombinationalCircuitCategory.Hom {G : Type u} (V : Type v) [Preorder V] (I O : CombinationalCircuitCategory V G) : Type v

Homomorphism.

Equations

• Circuit.CombinationalCircuitCategory.Hom V I O = { f : Circuit.Wires V I.obj → Circuit.Wires V O.obj // Monotone f }

@[inline]

def Circuit.CombinationalCircuitCategory.idVal {V : Type v} {n : ℕ} : Wires V n → Wires V n

The underlying identity wire-function.

Equations

• Circuit.CombinationalCircuitCategory.idVal x = x

@[simp]

theorem Circuit.CombinationalCircuitCategory.id_monotone {V : Type v} {n : ℕ} [Preorder V] : Monotone idVal

@[inline]

def Circuit.CombinationalCircuitCategory.id {V : Type v} {G✝ : Type u_1} {X : CombinationalCircuitCategory V G✝} [Preorder V] : Hom V X X

The identity morphism.

Equations

• Circuit.CombinationalCircuitCategory.id = ⟨Circuit.CombinationalCircuitCategory.idVal, ⋯⟩

@[implicit_reducible, inline]

instance Circuit.CombinationalCircuitCategory.instCategoryOfPreorder {V : Type v} {G : Type u} [Preorder V] : CategoryTheory.Category.{v, 0} (CombinationalCircuitCategory V G)

Equations

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

@[simp]

theorem Circuit.CombinationalCircuitCategory.id_coe_apply {V : Type v} {G : Type u} [Preorder V] (X : CombinationalCircuitCategory V G) (v : Wires V X.obj) : ↑(CategoryTheory.CategoryStruct.id X) v = v

@[inline]

def Circuit.CombinationalCircuitCategory.fork {V : Type v} (w : Wires V 1) : Wires V 2

The wire-function that duplicates its single input wire.

Equations

• Circuit.CombinationalCircuitCategory.fork w = #v[Vector.get w 0, Vector.get w 0]

@[simp]

theorem Circuit.CombinationalCircuitCategory.fork_monotone {V : Type v} [Preorder V] : Monotone fork

@[inline]

def Circuit.CombinationalCircuitCategory.join {V : Type v} [SemilatticeSup V] (w : Wires V 2) : Wires V 1

The wire-function that joins two input wires by taking their supremum.

Equations

• Circuit.CombinationalCircuitCategory.join w = #v[Vector.get w 0 ⊔ Vector.get w 1]

@[simp]

theorem Circuit.CombinationalCircuitCategory.join_monotone {V : Type v} [SemilatticeSup V] : Monotone join

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.tensorObj {V : Type v} {G : Type u} (X Y : CombinationalCircuitCategory V G) : CombinationalCircuitCategory V G

The monoidal product of two objects, adding their wire counts.

Equations

• X.tensorObj Y = { obj := X.obj + Y.obj }

@[implicit_reducible, inline]

instance Circuit.CombinationalCircuitCategory.instCircuitCategoryOfBot {V : Type v} {G : Type u} [SemilatticeSup V] [Gate V G] [Bot V] : CircuitCategory V G (CombinationalCircuitCategory V G)

Equations

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

theorem Circuit.CombinationalCircuitCategory.tensorHom_val_add {V : Type v} {G : Type u} {X₁ X₂ : CombinationalCircuitCategory V G} : min X₁.obj (X₁.obj + X₂.obj) = X₁.obj

theorem Circuit.CombinationalCircuitCategory.tensorHom_val_sub {V : Type v} {G : Type u} {X₁ X₂ : CombinationalCircuitCategory V G} : X₁.obj + X₂.obj - X₁.obj = X₂.obj

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.tensorHomVal {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (v : Wires V (X₁.obj + X₂.obj)) : Wires V (Y₁.obj + Y₂.obj)

The underlying wire-function of the monoidal product of two morphisms.

Equations

• Circuit.CombinationalCircuitCategory.tensorHomVal f g v = Vector.append (↑f (Vector.cast ⋯ (Vector.take v X₁.obj))) (↑g (Vector.cast ⋯ (Vector.drop v X₁.obj)))

theorem Circuit.CombinationalCircuitCategory.tensorHom_eq {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ : CombinationalCircuitCategory V G} (a : Wires V (X₁.obj + X₂.obj)) (f : X₁ ⟶ Y₁) : (↑f (Vector.ofFn fun (i : Fin X₁.obj) => Vector.get a (Fin.castAdd X₂.obj i))).toArray.size = Y₁.obj

theorem Circuit.CombinationalCircuitCategory.tensorHom_take {V : Type v} {G : Type u} {X₁ X₂ : CombinationalCircuitCategory V G} (a : Wires V (X₁.obj + X₂.obj)) : Vector.cast ⋯ (Vector.take a X₁.obj) = Vector.ofFn fun (i : Fin X₁.obj) => Vector.get a (Fin.castAdd X₂.obj i)

theorem Circuit.CombinationalCircuitCategory.tensorHom_eq_left {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (a : Wires V (X₁.obj + X₂.obj)) (j : Fin Y₁.obj) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Vector.get (tensorHomVal f g a) (Fin.castAdd Y₂.obj j) = Vector.get (↑f (Vector.ofFn fun (i : Fin X₁.obj) => Vector.get a (Fin.castAdd X₂.obj i))) j

theorem Circuit.CombinationalCircuitCategory.tensorHom_eq_right {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (a : Wires V (X₁.obj + X₂.obj)) (j : Fin Y₂.obj) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Vector.get (tensorHomVal f g a) (Fin.natAdd Y₁.obj j) = Vector.get (↑g (Vector.ofFn fun (i : Fin X₂.obj) => Vector.get a (Fin.natAdd X₁.obj i))) j

theorem Circuit.CombinationalCircuitCategory.tensorHom_get {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) (w : Wires V (X₁.obj + X₂.obj)) (i : Fin (Y₁.obj + Y₂.obj)) : Vector.get (tensorHomVal f g w) i = if h : ↑i < Y₁.obj then Vector.get (↑f (Vector.ofFn fun (k : Fin X₁.obj) => Vector.get w (Fin.castAdd X₂.obj k))) ⟨↑i, h⟩ else Vector.get (↑g (Vector.ofFn fun (k : Fin X₂.obj) => Vector.get w (Fin.natAdd X₁.obj k))) ⟨↑i - Y₁.obj, ⋯⟩

@[simp]

theorem Circuit.CombinationalCircuitCategory.tensorHom_monotone {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Monotone (tensorHomVal f g)

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.tensorHom {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ X₂ Y₂ : CombinationalCircuitCategory V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : X₁.tensorObj X₂ ⟶ Y₁.tensorObj Y₂

The monoidal product of two morphisms.

Equations

• Circuit.CombinationalCircuitCategory.tensorHom f g = ⟨Circuit.CombinationalCircuitCategory.tensorHomVal f g, ⋯⟩

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.isoHomVal {V : Type v} {n m : ℕ} (h : n = m) : Wires V n → Wires V m

The underlying wire-function of the forward direction of a wire-count isomorphism.

Equations

• Circuit.CombinationalCircuitCategory.isoHomVal h x✝ = Vector.cast h x✝

@[simp]

theorem Circuit.CombinationalCircuitCategory.iso_hom_monotone {V : Type v} [SemilatticeSup V] {n m : ℕ} (h : n = m) : Monotone (isoHomVal h)

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.isoHom {V : Type v} [SemilatticeSup V] {n m : ℕ} (h : n = m) : { f : Wires V n → Wires V m // Monotone f }

The forward direction of a wire-count isomorphism.

Equations

• Circuit.CombinationalCircuitCategory.isoHom h = ⟨Circuit.CombinationalCircuitCategory.isoHomVal h, ⋯⟩

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.isoInvVal {V : Type v} {n m : ℕ} (h : n = m) : Wires V m → Wires V n

The underlying wire-function of the inverse direction of a wire-count isomorphism.

Equations

• Circuit.CombinationalCircuitCategory.isoInvVal h x✝ = Vector.cast ⋯ x✝

theorem Circuit.CombinationalCircuitCategory.iso_inv_monotone {V : Type v} [SemilatticeSup V] {n m : ℕ} (h : n = m) : Monotone (isoInvVal h)

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.isoInv {V : Type v} [SemilatticeSup V] {n m : ℕ} (h : n = m) : { f : Wires V m → Wires V n // Monotone f }

The inverse direction of a wire-count isomorphism.

Equations

• Circuit.CombinationalCircuitCategory.isoInv h = ⟨Circuit.CombinationalCircuitCategory.isoInvVal h, ⋯⟩

@[simp]

theorem Circuit.CombinationalCircuitCategory.iso_hom_inv_id {V : Type v} {G : Type u} [SemilatticeSup V] {n m : ℕ} (h : n = m) : CategoryTheory.CategoryStruct.comp (isoHom h) (isoInv h) = CategoryTheory.CategoryStruct.id (OfNat.ofNat n)

theorem Circuit.CombinationalCircuitCategory.iso_inv_hom_id {V : Type v} {G : Type u} [SemilatticeSup V] {n m : ℕ} (h : n = m) : CategoryTheory.CategoryStruct.comp (isoInv h) (isoHom h) = CategoryTheory.CategoryStruct.id (OfNat.ofNat m)

@[inline]

def Circuit.CombinationalCircuitCategory.iso {V : Type v} {G : Type u} [SemilatticeSup V] {n m : ℕ} (h : n = m) : { obj := n } ≅ { obj := m }

The isomorphism between objects with equal wire counts.

Equations

• Circuit.CombinationalCircuitCategory.iso h = { hom := Circuit.CombinationalCircuitCategory.isoHom h, inv := Circuit.CombinationalCircuitCategory.isoInv h, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Circuit.CombinationalCircuitCategory.whisker {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X.tensorObj Y)

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.whiskerLeft {V : Type v} {G : Type u} [SemilatticeSup V] (X : CombinationalCircuitCategory V G) {Y₁ Y₂ : CombinationalCircuitCategory V G} : (Y₁ ⟶ Y₂) → (X.tensorObj Y₁ ⟶ X.tensorObj Y₂)

Left whiskering of a morphism by a fixed object.

Equations

• X.whiskerLeft = Circuit.CombinationalCircuitCategory.tensorHom (CategoryTheory.CategoryStruct.id X)

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.whiskerRight {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ X₂ : CombinationalCircuitCategory V G} (f : X₁ ⟶ X₂) (Y : CombinationalCircuitCategory V G) : X₁.tensorObj Y ⟶ X₂.tensorObj Y

Right whiskering of a morphism by a fixed object.

Equations

• Circuit.CombinationalCircuitCategory.whiskerRight f Y = Circuit.CombinationalCircuitCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)

@[simp]

theorem Circuit.CombinationalCircuitCategory.tensorHom_def {V : Type v} {G : Type u} [SemilatticeSup V] {W X Y Z : CombinationalCircuitCategory V G} (f : W ⟶ X) (g : Y ⟶ Z) : tensorHom f g = CategoryTheory.CategoryStruct.comp (whiskerRight f Y) (X.whiskerLeft g)

@[simp]

theorem Circuit.CombinationalCircuitCategory.id_tensorHom_id {V : Type v} {G : Type u} [SemilatticeSup V] (X₁ X₂ : CombinationalCircuitCategory V G) : tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (X₁.tensorObj X₂)

@[simp]

theorem Circuit.CombinationalCircuitCategory.tensorHom_comp_tensorHom {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CombinationalCircuitCategory V G} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryTheory.CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)

@[inline]

def Circuit.CombinationalCircuitCategory.tensorUnit {V : Type v} {G : Type u} : CombinationalCircuitCategory V G

The monoidal unit, the object with no wires.

Equations

• Circuit.CombinationalCircuitCategory.tensorUnit = { obj := 0 }

@[simp]

theorem Circuit.CombinationalCircuitCategory.associator_eq {V : Type v} {G : Type u} (X Y Z : CombinationalCircuitCategory V G) : X.obj + Y.obj + Z.obj = X.obj + (Y.obj + Z.obj)

@[inline]

def Circuit.CombinationalCircuitCategory.associator {V : Type v} {G : Type u} [SemilatticeSup V] (X Y Z : CombinationalCircuitCategory V G) : (X.tensorObj Y).tensorObj Z ≅ X.tensorObj (Y.tensorObj Z)

The associator isomorphism of the monoidal structure.

Equations

• X.associator Y Z = Circuit.CombinationalCircuitCategory.iso ⋯

theorem Circuit.CombinationalCircuitCategory.associator_naturality {V : Type v} {G : Type u} [SemilatticeSup V] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CombinationalCircuitCategory V G} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (Y₁.associator Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (X₁.associator X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

theorem Circuit.CombinationalCircuitCategory.pentagon {V : Type v} {G : Type u} [SemilatticeSup V] (W X Y Z : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (whiskerRight (W.associator X Y).hom Z) (CategoryTheory.CategoryStruct.comp (W.associator (X.tensorObj Y) Z).hom (W.whiskerLeft (X.associator Y Z).hom)) = CategoryTheory.CategoryStruct.comp ((W.tensorObj X).associator Y Z).hom (W.associator X (Y.tensorObj Z)).hom

theorem Circuit.CombinationalCircuitCategory.leftUnitor_eq {V : Type v} {G : Type u} (X : CombinationalCircuitCategory V G) : tensorUnit.obj + X.obj = X.obj

theorem Circuit.CombinationalCircuitCategory.rightUnitor_eq {V : Type v} {G : Type u} (X : CombinationalCircuitCategory V G) : X.obj + tensorUnit.obj = X.obj

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.leftUnitor {V : Type v} {G : Type u} [SemilatticeSup V] (X : CombinationalCircuitCategory V G) : tensorUnit.tensorObj X ≅ X

The left unitor isomorphism of the monoidal structure.

Equations

• X.leftUnitor = Circuit.CombinationalCircuitCategory.iso ⋯

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.rightUnitor {V : Type v} {G : Type u} [SemilatticeSup V] (X : CombinationalCircuitCategory V G) : X.tensorObj tensorUnit ≅ X

The right unitor isomorphism of the monoidal structure.

Equations

• X.rightUnitor = Circuit.CombinationalCircuitCategory.iso ⋯

theorem Circuit.CombinationalCircuitCategory.leftUnitor_naturality {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (tensorUnit.whiskerLeft f) Y.leftUnitor.hom = CategoryTheory.CategoryStruct.comp X.leftUnitor.hom f

theorem Circuit.CombinationalCircuitCategory.rightUnitor_naturality {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (whiskerRight f tensorUnit) Y.rightUnitor.hom = CategoryTheory.CategoryStruct.comp X.rightUnitor.hom f

theorem Circuit.CombinationalCircuitCategory.triangle {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (X.associator tensorUnit Y).hom (X.whiskerLeft Y.leftUnitor.hom) = whiskerRight X.rightUnitor.hom Y

@[implicit_reducible, inline]

instance Circuit.CombinationalCircuitCategory.instMonoidalCategory {V : Type v} {G : Type u} [SemilatticeSup V] : CategoryTheory.MonoidalCategory (CombinationalCircuitCategory V G)

Equations

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

@[simp]

theorem Circuit.CombinationalCircuitCategory.monoidal_tensorObj_obj {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = X.obj + Y.obj

@[simp]

theorem Circuit.CombinationalCircuitCategory.monoidal_tensorUnit_obj {V : Type v} {G : Type u} [SemilatticeSup V] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CombinationalCircuitCategory V G)).obj = 0

@[simp]

theorem Circuit.CombinationalCircuitCategory.id_hom_apply {V : Type v} {G : Type u} [SemilatticeSup V] (X : CombinationalCircuitCategory V G) (v : Wires V X.obj) : ↑(CategoryTheory.CategoryStruct.id X) v = v

theorem Circuit.CombinationalCircuitCategory.sub_eq {V : Type v} {G : Type u} {X Y : CombinationalCircuitCategory V G} : X.obj + Y.obj - X.obj = Y.obj

@[simp]

theorem Circuit.CombinationalCircuitCategory.associator_hom_apply {V : Type v} {G : Type u} [SemilatticeSup V] (X Y Z : CombinationalCircuitCategory V G) (v : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).obj) : ↑(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom v = Vector.cast ⋯ v

@[simp]

theorem Circuit.CombinationalCircuitCategory.associator_inv_apply {V : Type v} {G : Type u} [SemilatticeSup V] (X Y Z : CombinationalCircuitCategory V G) (v : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).obj) : ↑(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv v = Vector.cast ⋯ v

theorem Circuit.CombinationalCircuitCategory.braiding_hom_eq {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj - X.obj + min X.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).obj

@[reducible, inline]

abbrev Circuit.CombinationalCircuitCategory.braidingHomVal {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) (v : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj) : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).obj

The underlying wire-function of the braiding, swapping two blocks of wires.

Equations

• X.braidingHomVal Y v = Vector.cast ⋯ ((Vector.drop v X.obj).append (Vector.take v X.obj))

theorem Circuit.CombinationalCircuitCategory.braiding_hom_lt {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} {j : Fin Y.obj} : X.obj + ↑j < (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj

theorem Circuit.CombinationalCircuitCategory.braiding_hom_ge {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} {j : Fin X.obj} : ↑j < (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj

@[simp]

theorem Circuit.CombinationalCircuitCategory.braiding_hom_monotone {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} : Monotone (X.braidingHomVal Y)

@[inline]

def Circuit.CombinationalCircuitCategory.braidingHom {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

The braiding morphism, swapping two blocks of wires.

Equations

• X.braidingHom Y = ⟨X.braidingHomVal Y, ⋯⟩

theorem Circuit.CombinationalCircuitCategory.braiding_hom_inv_id {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} : CategoryTheory.CategoryStruct.comp (X.braidingHom Y) (Y.braidingHom X) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

@[inline]

def Circuit.CombinationalCircuitCategory.braiding {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

The braiding isomorphism of the symmetric monoidal structure.

Equations

• X.braiding Y = { hom := X.braidingHom Y, inv := Y.braidingHom X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem Circuit.CombinationalCircuitCategory.braiding_naturality_left {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} (f : X ⟶ Y) (Z : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (Y.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)

theorem Circuit.CombinationalCircuitCategory.braiding_eq {V : Type v} {G : Type u} [SemilatticeSup V] {X Y Z : CombinationalCircuitCategory V G} {f : Y ⟶ Z} {v : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj} {j : Fin X.obj} : Vector.get (↑(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (X.braiding Z).hom) v) (Fin.natAdd Z.obj j) = Vector.get (↑(CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) v) (Fin.natAdd Z.obj j)

theorem Circuit.CombinationalCircuitCategory.braiding_naturality_right {V : Type v} {G : Type u} [SemilatticeSup V] (X : CombinationalCircuitCategory V G) {Y Z : CombinationalCircuitCategory V G} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (X.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)

theorem Circuit.CombinationalCircuitCategory.braiding_add {V : Type v} {G : Type u} {i : ℕ} {X Y : CombinationalCircuitCategory V G} (h : i < Y.obj) : X.obj + i < X.obj + Y.obj

theorem Circuit.CombinationalCircuitCategory.braiding_sub {V : Type v} {G : Type u} [SemilatticeSup V] {X Y : CombinationalCircuitCategory V G} {i : Fin (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).obj} : ↑i - Y.obj < (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj

theorem Circuit.CombinationalCircuitCategory.braiding_get_ge {V : Type v} {G : Type u} {X Y : CombinationalCircuitCategory V G} {j : Fin X.obj} : ¬Y.obj + ↑j < Y.obj

theorem Circuit.CombinationalCircuitCategory.braiding_get {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) (v : Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj) (i : Fin (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).obj) : Vector.get (↑(X.braiding Y).hom v) i = if h : ↑i < Y.obj then Vector.get v ⟨X.obj + ↑i, ⋯⟩ else Vector.get v ⟨↑i - Y.obj, ⋯⟩

theorem Circuit.CombinationalCircuitCategory.braiding_get_castAdd {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) (v : Wires V (X.obj + Y.obj)) (j : Fin Y.obj) : Vector.get (↑(X.braiding Y).hom v) (Fin.castAdd X.obj j) = Vector.get v (Fin.natAdd X.obj j)

theorem Circuit.CombinationalCircuitCategory.braiding_get_natAdd {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) (v : Wires V (X.obj + Y.obj)) (j : Fin X.obj) : Vector.get (↑(X.braiding Y).hom v) (Fin.natAdd Y.obj j) = Vector.get v (Fin.castAdd Y.obj j)

theorem Circuit.CombinationalCircuitCategory.hexagon_forward {V : Type v} {G : Type u} [SemilatticeSup V] (X Y Z : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (X.braiding Z).hom))

theorem Circuit.CombinationalCircuitCategory.hexagon_reverse {V : Type v} {G : Type u} [SemilatticeSup V] (X Y Z : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (Y.braiding Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Z).hom Y))

theorem Circuit.CombinationalCircuitCategory.symmetry {V : Type v} {G : Type u} [SemilatticeSup V] (X Y : CombinationalCircuitCategory V G) : CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (Y.braiding X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

@[implicit_reducible, inline]

instance Circuit.CombinationalCircuitCategory.instSymmetricCategory {V : Type v} {G : Type u} [SemilatticeSup V] : CategoryTheory.SymmetricCategory (CombinationalCircuitCategory V G)

Equations

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