Sequential circuit category

References

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

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

Category of sequential circuits.

• of :: (
• obj : ℕ

  The number of wires of this object.

• )

@[implicit_reducible]

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

Equations

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

@[inline]

def Circuit.SequentialCircuitCategory.Stream (α : Type u_1) : Type u_1

A stream of values, i.e. an infinite sequence indexed by time.

Equations

• Circuit.SequentialCircuitCategory.Stream = Stream'

@[implicit_reducible]

instance Circuit.SequentialCircuitCategory.instPreorderStream {α : Type u_1} [Preorder α] : Preorder (Stream α)

Equations

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

@[reducible, inline]

abbrev Circuit.SequentialCircuitCategory.Stream.map {α : Type u_1} {β : Type u_2} : (α → β) → Stream α → Stream β

Map a function over a stream pointwise.

Equations

• Circuit.SequentialCircuitCategory.Stream.map = Stream'.map

@[simp]

theorem Circuit.SequentialCircuitCategory.Stream'.map_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : Stream' α) (t : ℕ) : Stream'.map f s t = f (s t)

def Circuit.SequentialCircuitCategory.Causal {α : Type u_1} {β : Type u_2} (f : Stream α → Stream β) : Prop

A stream function is causal if the output at time t depends only on inputs up to time t.

Equations

• Circuit.SequentialCircuitCategory.Causal f = ∀ (x y : Circuit.SequentialCircuitCategory.Stream α) (t : ℕ), (∀ s ≤ t, x s = y s) → f x t = f y t

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

Homomorphism.

Equations

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

@[inline]

def Circuit.SequentialCircuitCategory.idVal {V : Type v} {n : ℕ} : Stream (Wires V n) → Stream (Wires V n)

The underlying identity wire-function.

Equations

• Circuit.SequentialCircuitCategory.idVal x = x

@[simp]

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

@[simp]

theorem Circuit.SequentialCircuitCategory.id_causal {V : Type v} {n : ℕ} : Causal idVal

@[inline]

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

The identity morphism.

Equations

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

@[implicit_reducible, inline]

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

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

@[reducible, inline]

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

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

Equations

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

theorem Circuit.SequentialCircuitCategory.tensorHom_take {V : Type v} {G : Type u} {X₁ X₂ : SequentialCircuitCategory 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)

@[reducible, inline]

abbrev Circuit.SequentialCircuitCategory.tensorHomEq' {V : Type v} {G : Type u} {X₁ X₂ : SequentialCircuitCategory V G} (w : Vector V (X₁.obj + X₂.obj)) : Vector V X₁.obj

The first projection used when tensoring sequential morphisms.

Equations

• Circuit.SequentialCircuitCategory.tensorHomEq' w = Vector.ofFn fun (i : Fin X₁.obj) => w.get (Fin.castAdd X₂.obj i)

theorem Circuit.SequentialCircuitCategory.tensorHom_eq {V : Type v} {G : Type u} [Preorder V] {X₁ Y₁ X₂ : SequentialCircuitCategory V G} (v : Stream (Wires V (X₁.obj + X₂.obj))) (f : X₁ ⟶ Y₁) (t : ℕ) : (↑f (Stream'.map tensorHomEq' v) t).toArray.size = Y₁.obj

theorem Circuit.SequentialCircuitCategory.tensorHom_eq_left {V : Type v} {G : Type u} [Preorder V] {X₁ Y₁ X₂ Y₂ : SequentialCircuitCategory V G} (v : Stream (Wires V (X₁.obj + X₂.obj))) (t : ℕ) (j : Fin Y₁.obj) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Vector.get (Stream'.get (tensorHomVal f g v) t) (Fin.castAdd Y₂.obj j) = Vector.get (↑f (Stream'.map tensorHomEq' v) t) j

theorem Circuit.SequentialCircuitCategory.tensorHom_eq_right {V : Type v} {G : Type u} [Preorder V] {X₁ Y₁ X₂ Y₂ : SequentialCircuitCategory V G} (v : Stream (Wires V (X₁.obj + X₂.obj))) (t : ℕ) (j : Fin Y₂.obj) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Vector.get (Stream'.get (tensorHomVal f g v) t) (Fin.natAdd Y₁.obj j) = Vector.get (↑g (Stream'.map (fun (w : Vector V (X₁.obj + X₂.obj)) => Vector.ofFn fun (i : Fin X₂.obj) => w.get (Fin.natAdd X₁.obj i)) v) t) j

@[simp]

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

@[simp]

theorem Circuit.SequentialCircuitCategory.tensorHom_causal {V : Type v} {G : Type u} [Preorder V] {X₁ Y₁ X₂ Y₂ : SequentialCircuitCategory V G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Causal (tensorHomVal f g)

@[reducible, inline]

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

The monoidal product of two morphisms.

Equations

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

@[reducible, inline]

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

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

Equations

• Circuit.SequentialCircuitCategory.isoHomVal h = Stream'.map fun (x : Circuit.Wires V n) => Vector.cast h x

@[simp]

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

@[simp]

theorem Circuit.SequentialCircuitCategory.iso_hom_causal {V : Type v} {n m : ℕ} (h : n = m) : Causal (isoHomVal h)

@[reducible, inline]

abbrev Circuit.SequentialCircuitCategory.isoHom {V : Type v} [Preorder V] {n m : ℕ} (h : n = m) : { f : Stream (Wires V n) → Stream (Wires V m) // Monotone f ∧ Causal f }

The forward direction of a wire-count isomorphism.

Equations

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

@[reducible, inline]

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

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

Equations

• Circuit.SequentialCircuitCategory.isoInvVal h = Stream'.map fun (x : Circuit.Wires V m) => Vector.cast ⋯ x

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

theorem Circuit.SequentialCircuitCategory.iso_inv_causal {V : Type v} {n m : ℕ} (h : n = m) : Causal (isoInvVal h)

@[reducible, inline]

abbrev Circuit.SequentialCircuitCategory.isoInv {V : Type v} [Preorder V] {n m : ℕ} (h : n = m) : { f : Stream (Wires V m) → Stream (Wires V n) // Monotone f ∧ Causal f }

The inverse direction of a wire-count isomorphism.

Equations

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

@[simp]

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

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

@[simp]

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

@[inline]

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

The isomorphism between objects with equal wire counts.

Equations

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

@[simp]

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

@[reducible, inline]

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

Left whiskering of a morphism by a fixed object.

Equations

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

@[reducible, inline]

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

Right whiskering of a morphism by a fixed object.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem Circuit.SequentialCircuitCategory.tensorHom_comp_tensorHom {V : Type v} {G : Type u} [Preorder V] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : SequentialCircuitCategory 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.SequentialCircuitCategory.tensorUnit {V : Type v} {G : Type u} : SequentialCircuitCategory V G

The monoidal unit, the object with no wires.

Equations

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

@[simp]

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

@[inline]

def Circuit.SequentialCircuitCategory.associator {V : Type v} {G : Type u} [Preorder V] (X Y Z : SequentialCircuitCategory 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.SequentialCircuitCategory.iso ⋯

theorem Circuit.SequentialCircuitCategory.associator_naturality {V : Type v} {G : Type u} [Preorder V] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : SequentialCircuitCategory 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.SequentialCircuitCategory.pentagon {V : Type v} {G : Type u} [Preorder V] (W X Y Z : SequentialCircuitCategory 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.SequentialCircuitCategory.leftUnitor_eq {V : Type v} {G : Type u} (X : SequentialCircuitCategory V G) : tensorUnit.obj + X.obj = X.obj

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

@[reducible, inline]

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

The left unitor isomorphism of the monoidal structure.

Equations

• X.leftUnitor = Circuit.SequentialCircuitCategory.iso ⋯

@[reducible, inline]

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

The right unitor isomorphism of the monoidal structure.

Equations

• X.rightUnitor = Circuit.SequentialCircuitCategory.iso ⋯

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

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

theorem Circuit.SequentialCircuitCategory.triangle {V : Type v} {G : Type u} [Preorder V] (X Y : SequentialCircuitCategory 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.SequentialCircuitCategory.instMonoidalCategory {V : Type v} {G : Type u} [Preorder V] : CategoryTheory.MonoidalCategory (SequentialCircuitCategory V G)

Equations

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

@[simp]

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

theorem Circuit.SequentialCircuitCategory.braiding_hom_eq {V : Type v} {G : Type u} [Preorder V] {X Y : SequentialCircuitCategory 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.SequentialCircuitCategory.braidingHomVal {V : Type v} {G : Type u} [Preorder V] (X Y : SequentialCircuitCategory V G) : Stream (Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj) → Stream (Wires V (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X).obj)

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

Equations

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

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

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

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

theorem Circuit.SequentialCircuitCategory.braiding_hom_causal {V : Type v} {G : Type u} [Preorder V] {X Y : SequentialCircuitCategory V G} : Causal (X.braidingHomVal Y)

@[inline]

def Circuit.SequentialCircuitCategory.braidingHom {V : Type v} {G : Type u} [Preorder V] (X Y : SequentialCircuitCategory 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.SequentialCircuitCategory.braiding_hom_inv_id {V : Type v} {G : Type u} [Preorder V] {X Y : SequentialCircuitCategory V G} : CategoryTheory.CategoryStruct.comp (X.braidingHom Y) (Y.braidingHom X) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

@[inline]

def Circuit.SequentialCircuitCategory.braiding {V : Type v} {G : Type u} [Preorder V] (X Y : SequentialCircuitCategory 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.SequentialCircuitCategory.braiding_naturality_left {V : Type v} {G : Type u} [Preorder V] {X Y : SequentialCircuitCategory V G} (f : X ⟶ Y) (Z : SequentialCircuitCategory 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.SequentialCircuitCategory.braiding_naturality_right {V : Type v} {G : Type u} [Preorder V] (X : SequentialCircuitCategory V G) {Y Z : SequentialCircuitCategory 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.SequentialCircuitCategory.braiding_add {V : Type v} {G : Type u} {i : ℕ} {X Y : SequentialCircuitCategory V G} (h : i < Y.obj) : X.obj + i < X.obj + Y.obj

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

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

theorem Circuit.SequentialCircuitCategory.iso_hom_get {V : Type v} {n m : ℕ} (h : n = m) (v : Stream (Wires V n)) (t : ℕ) (i : Fin m) : Vector.get (isoHomVal h v t) i = Vector.get (v t) ⟨↑i, ⋯⟩

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

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

theorem Circuit.SequentialCircuitCategory.tensorObj_size_eq_forward {V : Type v} {G : Type u} {t : ℕ} {X Y Z : SequentialCircuitCategory V G} (v : Stream (Wires V ((X.tensorObj Y).tensorObj Z).obj)) : (v t).toArray.size = ((X.tensorObj Y).tensorObj Z).obj

theorem Circuit.SequentialCircuitCategory.hexagon_forward {V : Type v} {G : Type u} [Preorder V] (X Y Z : SequentialCircuitCategory 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.SequentialCircuitCategory.tensorObj_size_eq_reverse {V : Type v} {G : Type u} {t : ℕ} {X Y Z : SequentialCircuitCategory V G} (v : Stream (Wires V (X.tensorObj (Y.tensorObj Z)).obj)) : (v t).toArray.size = (X.tensorObj (Y.tensorObj Z)).obj

theorem Circuit.SequentialCircuitCategory.hexagon_reverse {V : Type v} {G : Type u} [Preorder V] (X Y Z : SequentialCircuitCategory 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.SequentialCircuitCategory.symmetry {V : Type v} {G : Type u} [Preorder V] (X Y : SequentialCircuitCategory 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.SequentialCircuitCategory.instSymmetricCategory {V : Type v} {G : Type u} [Preorder V] : CategoryTheory.SymmetricCategory (SequentialCircuitCategory V G)

Equations

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