ImplementationCategory

Difficulty: optional — 10 definitions, 5 abbreviations, 29 lemmas, 4 theorems.

definition abbreviation lemma theorem

legend

Component.Impl forms a PROP: a category whose objects are the natural numbers (here, wire counts) and whose morphisms compose the way Component.Impl.sequential already does, with Component.Impl.parallel giving it a monoidal (side-by-side) structure and Component.Impl.symmetry a braiding on top. We formalize this using Mathlib’s own category theory: this is what lets us reuse Mathlib’s BimonObj/IsCommMonObj/IsCommComonObj machinery (bicommutative bimonoids) for signal-flow-graph work later, instead of re-deriving it all from scratch.

This file is marked @[difficulty "optional"]: it consolidates the advanced, formalism-heavy proof that Component.Impl genuinely forms a Category/MonoidalCategory/ BraidedCategory in Mathlib’s own sense. None of the rest of the course depends on reading it — it’s here for whoever wants to see the categorical structure made precise, not required reading.

The central obstacle throughout: Component.Impl.sequential/Component.Impl.parallel are only associative/unital up to InformationSystem.equivalent, not on the nose (composing changes the state type via nested products, so e.g. (A × B) × C is a different type from A × (B × C)), but Mathlib’s Category/MonoidalCategory classes need composition to be associative/unital as a literal Eq. The standard fix: quotient Component.Impl.Arrow by InformationSystem.equivalent into genuine Hom-sets (Component.Impl.Hom), and show the operations are well-defined on the quotient (comp/tensor respecting the equivalence) and satisfy the category/monoidal/braided laws as genuine equalities there (via Quotient.sound).

Since the objects of this category are literally natural numbers, the associator and unitors are built from Mathlib’s eqToIso, applied to Nat.add_assoc/Nat.zero_add/Nat.add_zero — in this category eqToHom h is exactly Component.Impl.Hom.recast rfl h (Component.Impl.Hom.id Wire _) (Component.Impl.Hom.eqToHom_eq_recast_id), which lets most coherence laws (naturality, pentagon, triangle) reduce, via a handful of recast-manipulation lemmas, to an equation between two eqToHoms of the same underlying Nat equality — true automatically by proof irrelevance. leftUnitor_naturality/rightUnitor_naturality need one genuine extra fact beyond that (that Component.Impl.id Wire 0 and Component.Impl.empty Wire Wire are InformationSystem.equivalent — a real, if easy, induction).

The two hexagon axioms (for the braiding) are a genuinely different kind of argument: unlike pentagon/triangle, a hexagon mixes eqToHom (the associator) with Component.Impl.symmetry (a genuine data permutation, not a reindexing), so the recast/eqToHom-only toolkit doesn’t reach far enough. Instead, hexagon_forward_arrow/hexagon_reverse_arrow compute directly at the Fin-index level (in the style of Component.Impl.parallel_comm/parallel_assoc), helped by Fin.append_eval: a version of Fin.append_left/Fin.append_right stated in terms of the raw Nat value rather than requiring the index to be a syntactic castAdd/natAdd — the associator reindexing wraps every index in Fin.casts, which defeats the ordinary castAdd/natAdd-shaped simp lemmas even though the values work out.

Component.Impl forms a PROP

An “arrow” bundles a component together with the specific state it is in — since a component’s observable behaviour depends on its current state, not just its type, that bundle (not the bare component) is what plays the role of a PROP arrow.

NoteComponent.Impl.Arrow

An arrow from n wires to m wires: a component (over some existentially-quantified state type) together with the state it is currently in.

structure Component.Impl.Arrow (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : Nat) where
  State : Type
  nonempty : Nonempty State
  size : Norm State
  component : Component.Impl State Wire Wire n m
  state : State

Outer dependencies: (none)

Inner dependencies: Component.Impl, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Fin, HEq, Nat, Nonempty, SizeOf, eq_of_heq

Used by: Component.Impl.Arrow.Equiv, Component.Impl.Arrow.setoid, Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.comp_id, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id, Component.Impl.Hom.id_comp, Component.Impl.Hom.recast, Component.Impl.Hom.recast_recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor, Component.Impl.Hom.tensorUnit, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_comp, Component.Impl.monoidalCategory

NoteComponent.Impl.Arrow.Equiv

When two arrows (bundled components) count as “the same”: their underlying components are InformationSystem.equivalent at their respective states.

abbrev Component.Impl.Arrow.Equiv (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : Nat)
    (f g : Component.Impl.Arrow Wire n m) : Prop :=
  letI := f.nonempty; letI := f.size; letI := g.nonempty; letI := g.size
  InformationSystem.equivalent f.component g.component f.state g.state

Outer dependencies: Component.Impl.Arrow

Inner dependencies: InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: Component.Impl.Arrow.setoid

ImportantComponent.Impl.Arrow.setoid

instance Component.Impl.Arrow.setoid (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : Nat) :
    Setoid (Component.Impl.Arrow Wire n m) where
  r := Component.Impl.Arrow.Equiv Wire n m
  iseqv := by
    refine ⟨fun f => ?_, fun {f g} h => ?_, fun {f g h} h1 h2 => ?_⟩
    · letI := f.nonempty; letI := f.size
      exact fun _ => rfl
    · letI := f.nonempty; letI := f.size; letI := g.nonempty; letI := g.size
      exact fun is => (h is).symm
    · letI := f.nonempty; letI := f.size; letI := g.nonempty; letI := g.size
      letI := h.nonempty; letI := h.size
      exact fun is => (h1 is).trans (h2 is)

Outer dependencies: Component.Impl.Arrow

Inner dependencies: Component.Impl.Arrow.Equiv, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq.symm, Eq.trans, Fin, List, Nat, Nonempty, Setoid, rfl

Used by: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.comp_id, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id, Component.Impl.Hom.id_comp, Component.Impl.Hom.recast, Component.Impl.Hom.recast_recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor, Component.Impl.Hom.tensorUnit, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_comp, Component.Impl.monoidalCategory

NoteComponent.Impl.Hom

An arrow from n wires to m wires, up to InformationSystem.equivalent: the genuine Hom-set a real category needs, in place of the bare (existentially-quantified) Arrow.

abbrev Component.Impl.Hom (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : Nat) :=
  Quotient (Component.Impl.Arrow.setoid Wire n m)

Outer dependencies: (none)

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Quotient

Used by: Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.comp_id, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id, Component.Impl.Hom.id_comp, Component.Impl.Hom.recast, Component.Impl.Hom.recast_eqToHom, Component.Impl.Hom.recast_recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor, Component.Impl.Hom.tensorUnit, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_comp, Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.category, Component.Impl.monoidalCategory

NoteComponent.Impl.Hom.id

The identity arrow on n wires, as a Hom-set element.

abbrev Component.Impl.Hom.id (Wire : Type) [Nonempty Wire] [Norm Wire] (n : Nat) :
    Component.Impl.Hom Wire n n :=
  Quotient.mk _ ⟨Unit, inferInstance, inferInstance, Component.Impl.id Wire n, ()⟩

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.id, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance

Used by: Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.comp_id, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id_comp, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.toSpec_id, Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.category, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct

NoteComponent.Impl.Hom.comp

Composing two arrows in sequence, lifted to Hom-sets: well-defined by Component.Impl.sequential_congr.

def Component.Impl.Hom.comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p : Nat} :
    Component.Impl.Hom Wire n m → Component.Impl.Hom Wire m p → Component.Impl.Hom Wire n p :=
  Quotient.map₂
    (fun f g =>
      letI := f.nonempty; letI := f.size; letI := g.nonempty; letI := g.size
      (⟨f.State × g.State, inferInstance, inferInstance,
        Component.Impl.sequential f.component g.component, (f.state, g.state)⟩ :
        Component.Impl.Arrow Wire n p))
    (by
      intro f f' hf g g' hg
      letI := f.nonempty; letI := f.size; letI := f'.nonempty; letI := f'.size
      letI := g.nonempty; letI := g.size; letI := g'.nonempty; letI := g'.size
      exact Component.Impl.sequential_congr hf hg)

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.sequential, Component.Impl.sequential_congr, instNormProd_computerNetworks

Mathlib dependencies: Norm, Quotient.map₂

Lean core dependencies: Nat, Nonempty, Prod, inferInstance

Used by: Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.comp_id, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id_comp, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.toSpec_comp, Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.category, Component.Impl.monoidalCategory

NoteComponent.Impl.Hom.tensor

Placing two arrows in parallel, lifted to Hom-sets: well-defined by Component.Impl.parallel_congr.

def Component.Impl.Hom.tensor {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2 : Nat} :
    Component.Impl.Hom Wire n1 m1 → Component.Impl.Hom Wire n2 m2 →
      Component.Impl.Hom Wire (n1 + n2) (m1 + m2) :=
  Quotient.map₂
    (fun f g =>
      letI := f.nonempty; letI := f.size; letI := g.nonempty; letI := g.size
      (⟨f.State × g.State, inferInstance, inferInstance,
        Component.Impl.parallel f.component g.component, (f.state, g.state)⟩ :
        Component.Impl.Arrow Wire (n1 + n2) (m1 + m2)))
    (by
      intro f f' hf g g' hg
      letI := f.nonempty; letI := f.size; letI := f'.nonempty; letI := f'.size
      letI := g.nonempty; letI := g.size; letI := g'.nonempty; letI := g'.size
      exact Component.Impl.parallel_congr hf hg)

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.parallel, Component.Impl.parallel_congr, instNonemptyForallFin_computerNetworks, instNormProd_computerNetworks

Mathlib dependencies: Norm, Quotient.map₂

Lean core dependencies: Nat, Nonempty, Prod, inferInstance

Used by: Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comm, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct

NoteComponent.Impl.Hom.recast

Reindexing an arrow along a wire-count equality, lifted to Hom-sets: well-defined by Component.Impl.recast_congr.

def Component.Impl.Hom.recast {Wire : Type} [Nonempty Wire] [Norm Wire] {n n' m m' : Nat}
    (hn : n = n') (hm : m = m') : Component.Impl.Hom Wire n m → Component.Impl.Hom Wire n' m' :=
  Quotient.map
    (fun f =>
      letI := f.nonempty; letI := f.size
      (⟨f.State, inferInstance, inferInstance, Component.Impl.recast hn hm f.component, f.state⟩ :
        Component.Impl.Arrow Wire n' m'))
    (by
      intro f f' hf
      letI := f.nonempty; letI := f.size; letI := f'.nonempty; letI := f'.size
      exact Component.Impl.recast_congr hn hm hf)

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.recast, Component.Impl.recast_congr

Mathlib dependencies: Norm, Quotient.map

Lean core dependencies: Eq, Nat, Nonempty, inferInstance

Used by: Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.recast_eqToHom, Component.Impl.Hom.recast_recast, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.braidedCategory, Component.Impl.monoidalCategory

NoteComponent.Impl.Hom.tensorUnit

The empty (0-wire) arrow, as a Hom-set element.

abbrev Component.Impl.Hom.tensorUnit (Wire : Type) [Nonempty Wire] [Norm Wire] :
    Component.Impl.Hom Wire 0 0 :=
  Quotient.mk _ ⟨Unit, inferInstance, inferInstance, Component.Impl.empty Wire Wire, ()⟩

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.empty, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance

Used by: (none)

NoteComponent.Impl.Hom.symmetry

The symmetry (swap) arrow, as a Hom-set element.

abbrev Component.Impl.Hom.symmetry (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : Nat) :
    Component.Impl.Hom Wire (n + m) (m + n) :=
  Quotient.mk _ ⟨Unit, inferInstance, inferInstance, Component.Impl.symmetry Wire n m, ()⟩

Outer dependencies: Component.Impl.Hom

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.symmetry, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance

Used by: Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor_comm, Component.Impl.braiding, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right

TipComponent.Impl.Hom.id_comp

theorem Component.Impl.Hom.id_comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : Nat}
    (f : Component.Impl.Hom Wire n m) :
    Component.Impl.Hom.comp (Component.Impl.Hom.id Wire n) f = f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.id

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.id, Component.Impl.id_sequential, Component.Impl.sequential, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance

Used by: Component.Impl.Hom.eqToHom_comp, Component.Impl.category

TipComponent.Impl.Hom.comp_id

theorem Component.Impl.Hom.comp_id {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : Nat}
    (f : Component.Impl.Hom Wire n m) :
    Component.Impl.Hom.comp f (Component.Impl.Hom.id Wire m) = f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.id

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.id, Component.Impl.sequential, Component.Impl.sequential_id, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance

Used by: Component.Impl.Hom.comp_eqToHom, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.category

TipComponent.Impl.Hom.comp_assoc

theorem Component.Impl.Hom.comp_assoc {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p q : Nat}
    (f : Component.Impl.Hom Wire n m) (g : Component.Impl.Hom Wire m p) (h : Component.Impl.Hom Wire p q) :
    Component.Impl.Hom.comp (Component.Impl.Hom.comp f g) h =
      Component.Impl.Hom.comp f (Component.Impl.Hom.comp g h) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.sequential, Component.Impl.sequential_assoc, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance

Used by: Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.category

NoteComponent.Impl.category

Component.Impl (bundled with a state, and quotiented by InformationSystem.equivalent) forms a genuine Category, with objects the natural numbers (wire counts): Component.Impl.sequential is composition, Component.Impl.id its identity. Not registered as a global instance since which Wire type to use can’t be inferred from Category Nat alone — bring it into scope locally via letI := Component.Impl.category Wire where needed.

@[reducible] def Component.Impl.category (Wire : Type) [Nonempty Wire] [Norm Wire] :
    CategoryTheory.Category Nat where
  Hom n m := Component.Impl.Hom Wire n m
  id n := Component.Impl.Hom.id Wire n
  comp f g := Component.Impl.Hom.comp f g
  id_comp := Component.Impl.Hom.id_comp
  comp_id := Component.Impl.Hom.comp_id
  assoc := Component.Impl.Hom.comp_assoc

Outer dependencies: (none)

Inner dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_id, Component.Impl.Hom.id, Component.Impl.Hom.id_comp

Mathlib dependencies: CategoryTheory.Category, Norm

Lean core dependencies: Nat, Nonempty

Used by: Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.recast_eqToHom, Component.Impl.braidedCategory, Component.Impl.braiding, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.monoidalCategory, Component.Impl.monoidalCategoryStruct, instCategoryPROP

TipComponent.Impl.interchange

The interchange law: sequencing two parallel placements is the same as placing two sequences in parallel — (f₁ ⊗ g₁) ≫ (f₂ ⊗ g₂) = (f₁ ≫ f₂) ⊗ (g₁ ≫ g₂), up to re-associating the combined state. This is exactly what makes Component.Impl.Hom.tensor a bifunctor (needed for MonoidalCategory.tensorHom_comp_tensorHom).

theorem Component.Impl.interchange {StateA StateB StateC StateD : Type}
    [Nonempty StateA] [Norm StateA] [Nonempty StateB] [Norm StateB]
    [Nonempty StateC] [Norm StateC] [Nonempty StateD] [Norm StateD]
    {n1 m1 n2 m2 p1 p2 : Nat}
    (f1 : Component.Impl StateA Wire Wire n1 m1) (f2 : Component.Impl StateB Wire Wire n2 m2)
    (g1 : Component.Impl StateC Wire Wire m1 p1) (g2 : Component.Impl StateD Wire Wire m2 p2)
    (sa : StateA) (sb : StateB) (sc : StateC) (sd : StateD) :
    InformationSystem.equivalent
      (Component.Impl.sequential (Component.Impl.parallel f1 f2) (Component.Impl.parallel g1 g2))
      (Component.Impl.parallel (Component.Impl.sequential f1 g1) (Component.Impl.sequential f2 g2))
      ((sa, sb), (sc, sd)) ((sa, sc), (sb, sd)) := by

Dependencies: Component.Impl, Component.Impl.parallel, Component.Impl.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right, Norm

Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, congrArg, funext, id, rfl

Used by: Component.Impl.Hom.tensor_comp_tensor

TipComponent.Impl.recast_recast

Composing two reindexings is the same as reindexing once, along the composed proof.

theorem Component.Impl.recast_recast {State : Type} [Nonempty State] [Norm State]
    {n n' n'' m m' m'' : Nat} (h1 : n = n') (h2 : m = m') (h1' : n' = n'') (h2' : m' = m'')
    (c : Component.Impl State Wire Wire n m) :
    Component.Impl.recast h1' h2' (Component.Impl.recast h1 h2 c) =
      Component.Impl.recast (h1.trans h1') (h2.trans h2') c := by

Dependencies: Component.Impl, Component.Impl.recast

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.trans, Nat, Nonempty

Used by: Component.Impl.Hom.recast_recast

TipComponent.Impl.Hom.recast_recast

The Hom-level version of Component.Impl.recast_recast.

theorem Component.Impl.Hom.recast_recast {n n' n'' m m' m'' : Nat} (h1 : n = n') (h2 : m = m')
    (h1' : n' = n'') (h2' : m' = m'') (f : Component.Impl.Hom Wire n m) :
    Component.Impl.Hom.recast h1' h2' (Component.Impl.Hom.recast h1 h2 f) =
      Component.Impl.Hom.recast (h1.trans h1') (h2.trans h2') f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.recast

Proof dependencies: Component.Impl, Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.recast, Component.Impl.recast_recast

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Nat, Nonempty, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.eqToHom_eq_recast_id

In this category, eqToHom h is exactly the identity, reindexed on its output wires.

theorem Component.Impl.Hom.eqToHom_eq_recast_id {n m : Nat} (h : n = m) :
    letI := Component.Impl.category Wire
    (eqToHom h : Component.Impl.Hom Wire n m) =
      Component.Impl.Hom.recast rfl h (Component.Impl.Hom.id Wire n) := by

Dependencies: Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.category

Mathlib dependencies: CategoryTheory.eqToHom, Norm

Lean core dependencies: Eq, Nat, Nonempty, rfl

Used by: Component.Impl.braidedCategory, Component.Impl.monoidalCategory

TipComponent.Impl.Hom.comp_eqToHom

Composing with eqToHom h on the right is the same as reindexing the output wires by h.

theorem Component.Impl.Hom.comp_eqToHom {n m p : Nat} (h : m = p) (f : Component.Impl.Hom Wire n m) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.comp f (eqToHom h) = Component.Impl.Hom.recast rfl h f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.recast, Component.Impl.category

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.Hom.comp_id, Component.Impl.Hom.id

Mathlib dependencies: CategoryTheory.eqToHom, Norm

Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Quotient.ind, Quotient.mk, congrArg, id, rfl

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.eqToHom_comp

Composing with eqToHom h on the left is the same as reindexing the input wires by h.

theorem Component.Impl.Hom.eqToHom_comp {n m p : Nat} (h : n = m) (f : Component.Impl.Hom Wire m p) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.comp (eqToHom h) f = Component.Impl.Hom.recast h.symm rfl f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.recast, Component.Impl.category

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.Hom.id, Component.Impl.Hom.id_comp

Mathlib dependencies: CategoryTheory.eqToHom, Norm

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Nat, Nonempty, Quotient.ind, Quotient.mk, congrArg, id, rfl

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.recast_eqToHom

Reindexing eqToHom h on both sides is again an eqToHom, of the composed equality.

theorem Component.Impl.Hom.recast_eqToHom {a b c d : Nat} (hn : b = a) (h : b = c) (hm : c = d) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.recast hn hm (eqToHom h) = eqToHom (hn.symm.trans (h.trans hm)) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.recast, Component.Impl.category

Mathlib dependencies: CategoryTheory.eqToHom, Norm

Lean core dependencies: Eq, Eq.symm, Eq.trans, Nat, Nonempty

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.recast_parallel_left

Reindexing the first factor of a parallel placement is the same as reindexing the whole placement’s matching wires.

theorem Component.Impl.recast_parallel_left {State1 State2 : Type}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    {n1 n1' m1 m1' n2 m2 : Nat} (hn : n1 = n1') (hm : m1 = m1')
    (c1 : Component.Impl State1 Wire Wire n1 m1) (c2 : Component.Impl State2 Wire Wire n2 m2) :
    Component.Impl.parallel (Component.Impl.recast hn hm c1) c2 =
      Component.Impl.recast (congrArg (· + n2) hn) (congrArg (· + m2) hm)
        (Component.Impl.parallel c1 c2) := by

Dependencies: Component.Impl, Component.Impl.parallel, Component.Impl.recast, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, congrArg

Used by: Component.Impl.Hom.tensor_recast_left

TipComponent.Impl.recast_parallel_right

Reindexing the second factor of a parallel placement is the same as reindexing the whole placement’s matching wires.

theorem Component.Impl.recast_parallel_right {State1 State2 : Type}
    [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2]
    {n1 m1 n2 n2' m2 m2' : Nat} (hn : n2 = n2') (hm : m2 = m2')
    (c1 : Component.Impl State1 Wire Wire n1 m1) (c2 : Component.Impl State2 Wire Wire n2 m2) :
    Component.Impl.parallel c1 (Component.Impl.recast hn hm c2) =
      Component.Impl.recast (congrArg (n1 + ·) hn) (congrArg (m1 + ·) hm)
        (Component.Impl.parallel c1 c2) := by

Dependencies: Component.Impl, Component.Impl.parallel, Component.Impl.recast, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, congrArg

Used by: Component.Impl.Hom.tensor_recast_right

TipComponent.Impl.Hom.tensor_recast_left

The Hom-level version of Component.Impl.recast_parallel_left.

theorem Component.Impl.Hom.tensor_recast_left {n1 n1' m1 m1' n2 m2 : Nat}
    (hn : n1 = n1') (hm : m1 = m1')
    (f1 : Component.Impl.Hom Wire n1 m1) (f2 : Component.Impl.Hom Wire n2 m2) :
    Component.Impl.Hom.tensor (Component.Impl.Hom.recast hn hm f1) f2 =
      Component.Impl.Hom.recast (congrArg (· + n2) hn) (congrArg (· + m2) hm)
        (Component.Impl.Hom.tensor f1 f2) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.recast, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl, Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.parallel, Component.Impl.recast, Component.Impl.recast_parallel_left, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Prod, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.tensor_recast_right

The Hom-level version of Component.Impl.recast_parallel_right.

theorem Component.Impl.Hom.tensor_recast_right {n1 m1 n2 n2' m2 m2' : Nat}
    (hn : n2 = n2') (hm : m2 = m2')
    (f1 : Component.Impl.Hom Wire n1 m1) (f2 : Component.Impl.Hom Wire n2 m2) :
    Component.Impl.Hom.tensor f1 (Component.Impl.Hom.recast hn hm f2) =
      Component.Impl.Hom.recast (congrArg (n1 + ·) hn) (congrArg (m1 + ·) hm)
        (Component.Impl.Hom.tensor f1 f2) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.recast, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl, Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.parallel, Component.Impl.recast, Component.Impl.recast_parallel_right, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Prod, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.tensor_id_id

Tensoring two identities gives the identity on the combined wires.

theorem Component.Impl.Hom.tensor_id_id (n m : Nat) :
    Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire n) (Component.Impl.Hom.id Wire m) =
      Component.Impl.Hom.id Wire (n + m) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.id, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.id, Component.Impl.parallel, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Norm

Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, congr, congrArg, congrFun', id, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.tensor_empty

Tensoring with the empty component (0-wire identity) on the left does nothing, up to reindexing across 0 + n = n.

theorem Component.Impl.Hom.tensor_empty {n m : Nat} (f : Component.Impl.Hom Wire n m) :
    Component.Impl.Hom.recast (Nat.zero_add n) (Nat.zero_add m)
      (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire 0) f) = f := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.empty_parallel, Component.Impl.id, Component.Impl.parallel, Component.Impl.recast, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nat.zero_add, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.tensor_assoc

The Hom-level version of Component.Impl.parallel_assoc.

theorem Component.Impl.Hom.tensor_assoc {n1 m1 n2 m2 n3 m3 : Nat}
    (f1 : Component.Impl.Hom Wire n1 m1) (f2 : Component.Impl.Hom Wire n2 m2)
    (f3 : Component.Impl.Hom Wire n3 m3) :
    Component.Impl.Hom.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
      (Component.Impl.Hom.tensor (Component.Impl.Hom.tensor f1 f2) f3) =
      Component.Impl.Hom.tensor f1 (Component.Impl.Hom.tensor f2 f3) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.recast, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.parallel, Component.Impl.parallel_assoc, Component.Impl.recast, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance

Used by: Component.Impl.monoidalCategory

TipComponent.Impl.Hom.tensor_comp_tensor

The Hom-level version of Component.Impl.interchange: tensorHom_comp_tensorHom, making Component.Impl.Hom.tensor a bifunctor.

theorem Component.Impl.Hom.tensor_comp_tensor {n1 m1 p1 n2 m2 p2 : Nat}
    (f1 : Component.Impl.Hom Wire n1 m1) (f2 : Component.Impl.Hom Wire n2 m2)
    (g1 : Component.Impl.Hom Wire m1 p1) (g2 : Component.Impl.Hom Wire m2 p2) :
    Component.Impl.Hom.comp (Component.Impl.Hom.tensor f1 f2) (Component.Impl.Hom.tensor g1 g2) =
      Component.Impl.Hom.tensor (Component.Impl.Hom.comp f1 g1) (Component.Impl.Hom.comp f2 g2) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.interchange, Component.Impl.parallel, Component.Impl.sequential, instNormProd_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance

Used by: Component.Impl.monoidalCategory

NoteComponent.Impl.monoidalCategoryStruct

The tensor of Component.Impl.category Wire: tensorObj := (+), tensorHom := Component.Impl.Hom.tensor, identity/associator/unitors via eqToIso on the corresponding Nat equalities.

@[reducible] def Component.Impl.monoidalCategoryStruct (Wire : Type) [Nonempty Wire] [Norm Wire] :
    @MonoidalCategoryStruct Nat (Component.Impl.category Wire) :=
  letI := Component.Impl.category Wire
  { tensorObj := fun n m => n + m
    whiskerLeft := fun n {_ _} f => Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire n) f
    whiskerRight := fun {_ _} f m => Component.Impl.Hom.tensor f (Component.Impl.Hom.id Wire m)
    tensorHom := fun f g => Component.Impl.Hom.tensor f g
    tensorUnit := 0
    associator := fun n m p => eqToIso (Nat.add_assoc n m p)
    leftUnitor := fun n => eqToIso (Nat.zero_add n)
    rightUnitor := fun n => eqToIso (Nat.add_zero n) }

Outer dependencies: Component.Impl.category

Inner dependencies: Component.Impl.Hom.id, Component.Impl.Hom.tensor

Mathlib dependencies: CategoryTheory.MonoidalCategoryStruct, CategoryTheory.eqToIso, Norm

Lean core dependencies: Nat, Nat.add_assoc, Nat.add_zero, Nat.zero_add, Nonempty

Used by: Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right, Component.Impl.monoidalCategory

NoteComponent.Impl.monoidalCategory

Component.Impl (bundled with a state, quotiented by InformationSystem.equivalent) forms a genuine MonoidalCategory: Component.Impl.parallel is the tensor, Component.Impl.empty its unit. associator_naturality/pentagon/triangle reduce, via the recast/eqToHom lemmas above, to a statement that two proofs of the same Nat equation give the same eqToHom — true by proof irrelevance, nothing more. leftUnitor_naturality/rightUnitor_naturality need one genuine extra fact beyond that: that Component.Impl.id Wire 0 and Component.Impl.empty Wire Wire are InformationSystem.equivalent (both have no wires, so this is immediate, but it’s still a real induction, not proof irrelevance).

@[reducible] noncomputable def Component.Impl.monoidalCategory
    (Wire : Type) [Nonempty Wire] [Norm Wire] :
    letI := Component.Impl.category Wire
    letI := Component.Impl.monoidalCategoryStruct Wire
    MonoidalCategory Nat :=
  letI := Component.Impl.category Wire
  letI := Component.Impl.monoidalCategoryStruct Wire
  MonoidalCategory.ofTensorHom
    (id_tensorHom_id := fun n m => Component.Impl.Hom.tensor_id_id n m)
    (tensorHom_comp_tensorHom := fun f1 f2 g1 g2 => Component.Impl.Hom.tensor_comp_tensor f1 f2 g1 g2)
    (associator_naturality := by
      intro n1 n2 n3 m1 m2 m3 f1 f2 f3
      change Component.Impl.Hom.comp
          (Component.Impl.Hom.tensor (Component.Impl.Hom.tensor f1 f2) f3)
          (eqToIso (Nat.add_assoc m1 m2 m3)).hom =
        Component.Impl.Hom.comp (eqToIso (Nat.add_assoc n1 n2 n3)).hom
          (Component.Impl.Hom.tensor f1 (Component.Impl.Hom.tensor f2 f3))
      rw [eqToIso.hom, eqToIso.hom, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp,
        ← Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.recast_recast])
    (leftUnitor_naturality := by
      intro n m f
      change Component.Impl.Hom.comp (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire 0) f)
          (eqToIso (Nat.zero_add m)).hom = Component.Impl.Hom.comp (eqToIso (Nat.zero_add n)).hom f
      rw [eqToIso.hom, eqToIso.hom, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp]
      have := congrArg (Component.Impl.Hom.recast (Nat.zero_add n).symm rfl)
        (Component.Impl.Hom.tensor_empty f)
      rwa [Component.Impl.Hom.recast_recast] at this)
    (rightUnitor_naturality := by
      intro n m f
      change Component.Impl.Hom.comp (Component.Impl.Hom.tensor f (Component.Impl.Hom.id Wire 0))
          (eqToIso (Nat.add_zero m)).hom = Component.Impl.Hom.comp (eqToIso (Nat.add_zero n)).hom f
      rw [eqToIso.hom, eqToIso.hom, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp]
      change Component.Impl.Hom.recast rfl (Nat.add_zero m)
          (Component.Impl.Hom.tensor f (Component.Impl.Hom.id Wire 0)) =
        Component.Impl.Hom.recast (Nat.add_zero n) rfl f
      have hidempty : InformationSystem.equivalent
          (Component.Impl.id Wire 0) (Component.Impl.empty Wire Wire) () () := by
        intro is
        induction is with
        | nil => rfl
        | cons i is ih =>
          show ((Component.Impl.id Wire 0).eval () (i :: is)).2 =
            ((Component.Impl.empty Wire Wire).eval () (i :: is)).2
          simp only [InformationSystem.eval, Component.Impl.id, Component.Impl.empty]
          have : i = Fin.elim0 := funext (fun k => k.elim0)
          rw [this]
          exact congrArg (List.cons Fin.elim0) ih
      have htensor : Component.Impl.Hom.tensor f (Component.Impl.Hom.id Wire 0) = f := by
        induction f using Quotient.ind with
        | _ f =>
          letI := f.nonempty; letI := f.size
          refine Quotient.sound (fun is => ?_)
          have hrefl : InformationSystem.equivalent f.component f.component f.state f.state :=
            fun _ => rfl
          have h1 := Component.Impl.parallel_congr (c2 := Component.Impl.id Wire 0)
            (c2' := Component.Impl.empty Wire Wire) hrefl hidempty
          have h2 := Component.Impl.parallel_empty f.component f.state
          exact (h1 is).trans (h2 is)
      rw [htensor])
    (pentagon := by
      intro n1 n2 n3 n4
      change Component.Impl.Hom.comp
          (Component.Impl.Hom.tensor (eqToIso (Nat.add_assoc n1 n2 n3)).hom (Component.Impl.Hom.id Wire n4))
          (Component.Impl.Hom.comp (eqToIso (Nat.add_assoc n1 (n2 + n3) n4)).hom
            (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire n1)
              (eqToIso (Nat.add_assoc n2 n3 n4)).hom)) =
        Component.Impl.Hom.comp (eqToIso (Nat.add_assoc (n1 + n2) n3 n4)).hom
          (eqToIso (Nat.add_assoc n1 n2 (n3 + n4))).hom
      rw [eqToIso.hom, eqToIso.hom, eqToIso.hom, eqToIso.hom, eqToIso.hom]
      rw [Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc n1 n2 n3),
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc n2 n3 n4),
        Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right,
        Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_id_id]
      simp only [← Component.Impl.Hom.eqToHom_eq_recast_id]
      simp only [Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.recast_eqToHom])
    (triangle := by
      intro n m
      change Component.Impl.Hom.comp (eqToIso (Nat.add_assoc n 0 m)).hom
          (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire n) (eqToIso (Nat.zero_add m)).hom) =
        Component.Impl.Hom.tensor (eqToIso (Nat.add_zero n)).hom (Component.Impl.Hom.id Wire m)
      rw [eqToIso.hom, eqToIso.hom, eqToIso.hom]
      rw [Component.Impl.Hom.eqToHom_eq_recast_id (Nat.zero_add m),
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_zero n),
        Component.Impl.Hom.tensor_recast_right, Component.Impl.Hom.tensor_recast_left,
        Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_id_id]
      simp only [← Component.Impl.Hom.eqToHom_eq_recast_id]
      simp only [Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.recast_eqToHom])

Outer dependencies: Component.Impl.category

Inner dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.comp_eqToHom, Component.Impl.Hom.eqToHom_comp, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.Hom.recast_eqToHom, Component.Impl.Hom.recast_recast, Component.Impl.Hom.tensor, Component.Impl.Hom.tensor_assoc, Component.Impl.Hom.tensor_comp_tensor, Component.Impl.Hom.tensor_empty, Component.Impl.Hom.tensor_id_id, Component.Impl.Hom.tensor_recast_left, Component.Impl.Hom.tensor_recast_right, Component.Impl.empty, Component.Impl.id, Component.Impl.monoidalCategoryStruct, Component.Impl.parallel, Component.Impl.parallel_congr, Component.Impl.parallel_empty, InformationSystem.equivalent, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: CategoryTheory.MonoidalCategory, CategoryTheory.MonoidalCategory.ofTensorHom, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.eqToIso.hom, Norm

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.elim0, List, Nat, Nat.add_assoc, Nat.add_zero, Nat.zero_add, Nonempty, Prod, Quotient.ind, Quotient.sound, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, funext, id, inferInstance, of_eq_true, rfl

Used by: Component.Impl.braidedCategory, instMonoidalCategoryPROP

TipComponent.Impl.symmetry_symmetry

Swapping twice (with the block sizes swapped back) undoes itself.

theorem Component.Impl.symmetry_symmetry (n m : Nat) :
    InformationSystem.equivalent
      (Component.Impl.sequential (Component.Impl.symmetry Wire n m) (Component.Impl.symmetry Wire m n))
      (Component.Impl.id Wire (n + m)) ((), ()) () := by

Dependencies: Component.Impl.id, Component.Impl.sequential, Component.Impl.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Fin.append_left, Fin.append_right, Norm

Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, congrFun', funext, id

Used by: Component.Impl.Hom.symmetry_symmetry

TipComponent.Impl.Hom.symmetry_symmetry

The Hom-level version of Component.Impl.symmetry_symmetry.

theorem Component.Impl.Hom.symmetry_symmetry (n m : Nat) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.comp (Component.Impl.Hom.symmetry Wire n m) (Component.Impl.Hom.symmetry Wire m n) =
      Component.Impl.Hom.id Wire (n + m) :=

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.id, Component.Impl.Hom.symmetry

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.id, Component.Impl.sequential, Component.Impl.symmetry, Component.Impl.symmetry_symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance

Used by: Component.Impl.braiding, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right

NoteComponent.Impl.braiding

The braiding: swapping the first n wires and the next m wires is a genuine isomorphism, its own inverse (swapped).

@[reducible] noncomputable def Component.Impl.braiding (Wire : Type) [Nonempty Wire] [Norm Wire]
    (n m : Nat) :
    letI := Component.Impl.category Wire
    letI := Component.Impl.monoidalCategoryStruct Wire
    (n + m : Nat) ≅ (m + n) :=
  letI := Component.Impl.category Wire
  { hom := Component.Impl.Hom.symmetry Wire n m
    inv := Component.Impl.Hom.symmetry Wire m n
    hom_inv_id := Component.Impl.Hom.symmetry_symmetry n m
    inv_hom_id := Component.Impl.Hom.symmetry_symmetry m n }

Outer dependencies: Component.Impl.category

Inner dependencies: Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry

Mathlib dependencies: CategoryTheory.Iso, Norm

Lean core dependencies: Nat, Nonempty

Used by: Component.Impl.braidedCategory, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right

TipComponent.Impl.Hom.tensor_comm

The Hom-level version of Component.Impl.parallel_comm: naturality of the braiding with respect to both morphisms being tensored.

theorem Component.Impl.Hom.tensor_comm {n1 m1 n2 m2 : Nat}
    (f1 : Component.Impl.Hom Wire n1 m1) (f2 : Component.Impl.Hom Wire n2 m2) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.tensor f1 f2 =
      Component.Impl.Hom.comp (Component.Impl.Hom.comp (Component.Impl.Hom.symmetry Wire n1 n2)
        (Component.Impl.Hom.tensor f2 f1)) (Component.Impl.Hom.symmetry Wire m2 m1) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.symmetry, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.parallel, Component.Impl.parallel_comm, Component.Impl.sequential, Component.Impl.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, Unit, Unit.unit, inferInstance

Used by: Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right

TipComponent.Impl.braiding_naturality_right

BraidedCategory.braiding_naturality_right, for Component.Impl.braiding.

theorem Component.Impl.braiding_naturality_right {X Y Z : Nat} (f : Component.Impl.Hom Wire Y Z) :
    letI := Component.Impl.category Wire
    letI := Component.Impl.monoidalCategoryStruct Wire
    (MonoidalCategoryStruct.whiskerLeft X f ≫ (Component.Impl.braiding Wire X Z).hom) =
      (Component.Impl.braiding Wire X Y).hom ≫ MonoidalCategoryStruct.whiskerRight f X := by

Dependencies: Component.Impl.Hom, Component.Impl.braiding, Component.Impl.category, Component.Impl.monoidalCategoryStruct

Proof dependencies: Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_id, Component.Impl.Hom.id, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor, Component.Impl.Hom.tensor_comm

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, congrArg, id

Used by: Component.Impl.braidedCategory

TipComponent.Impl.braiding_naturality_left

BraidedCategory.braiding_naturality_left, for Component.Impl.braiding.

theorem Component.Impl.braiding_naturality_left {X Y Z : Nat} (f : Component.Impl.Hom Wire X Y) :
    letI := Component.Impl.category Wire
    letI := Component.Impl.monoidalCategoryStruct Wire
    (MonoidalCategoryStruct.whiskerRight f Z ≫ (Component.Impl.braiding Wire Y Z).hom) =
      (Component.Impl.braiding Wire X Z).hom ≫ MonoidalCategoryStruct.whiskerLeft Z f := by

Dependencies: Component.Impl.Hom, Component.Impl.braiding, Component.Impl.category, Component.Impl.monoidalCategoryStruct

Proof dependencies: Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.comp_id, Component.Impl.Hom.id, Component.Impl.Hom.symmetry, Component.Impl.Hom.symmetry_symmetry, Component.Impl.Hom.tensor, Component.Impl.Hom.tensor_comm

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, congrArg, id

Used by: Component.Impl.braidedCategory

TipComponent.Impl.equivalent_of_stationary

Two components are equivalent (from given starting states) once we know: each one’s own state never actually moves away from that starting state (stationary1/stationary2 — holds by rfl for any Component.Impl.id/Component.Impl.symmetry/Component.Impl.recast/Component.Impl.sequential/ Component.Impl.parallel composite that never touches a “real” underlying component, since such a composite’s state is only ever Unit or a product of Units; there’s no single lemma proving this in general, each call site below just discharges it directly), and their one-step outputs agree there. Sidesteps the awkwardness of the two states carrying different types (as they do for the hexagons), so there is no single “next (state, output) pair” to rewrite with in one step, unlike e.g. Component.Impl.symmetry_symmetry.

theorem Component.Impl.equivalent_of_stationary {State1 State2 : Type} [Nonempty State1] [Norm State1]
    [Nonempty State2] [Norm State2] {n m : Nat}
    {c1 : Component.Impl State1 Wire Wire n m} {c2 : Component.Impl State2 Wire Wire n m}
    (s1 : State1) (s2 : State2)
    (stationary1 : ∀ i, (c1.step s1 i).1 = s1) (stationary2 : ∀ i, (c2.step s2 i).1 = s2)
    (hout : ∀ i, (c1.step s1 i).2 = (c2.step s2 i).2) :
    InformationSystem.equivalent c1 c2 s1 s2 := by

Dependencies: Component.Impl, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Proof dependencies: InformationSystem.eval

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, List, Nat, Nonempty, Prod, congr, congrArg, congrFun', id

Used by: Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow

TipFin.append_eval

Non-dependent (motive-free) evaluation of Fin.append: unlike Fin.append_left/ Fin.append_right, this doesn’t need the index to be a syntactic castAdd/natAdd — only its underlying Nat value, which is all Fin.cast (e.g. from reindexing along associativity) ever changes anyway. Needed by the two hexagon identities just below: the associator reindexing wraps every index in Fin.casts, which defeats the ordinary castAdd/natAdd-shaped simp lemmas even though the values work out.

theorem Fin.append_eval {a b : Nat} {α : Type} (A : Fin a → α) (B : Fin b → α) (x : Fin (a + b)) :
    Fin.append A B x = if h : (x : Nat) < a then A ⟨x, h⟩ else B ⟨(x : Nat) - a, by omega⟩ := by

Dependencies: (none)

Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, False, Fin, Fin.castAdd, Fin.ext, Fin.natAdd, Fin.val_congr, GE.ge, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_not_lt, Nat.lt_or_ge, Nat.lt_or_gt_of_ne, Not, Or, Or.elim, congrArg, dif_neg, dif_pos, dite, eq_self, id, le_of_le_of_eq, of_decide_eq_true, of_eq_true

Used by: Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Impl.hexagon_forward_arrow, Component.Impl.hexagon_reverse_arrow, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

TipComponent.Impl.hexagon_forward_arrow

The first hexagon identity, at the arrow level: reassociating (X+Y)+Z to X+(Y+Z), swapping X past the whole Y+Z block, then reassociating again to Y+(Z+X) is the same as swapping X past Y and Z one at a time, with a reassociation in between.

theorem Component.Impl.hexagon_forward_arrow (X Y Z : Nat) :
    InformationSystem.equivalent
      (Component.Impl.sequential
        (Component.Impl.sequential
          (Component.Impl.recast rfl (Nat.add_assoc X Y Z) (Component.Impl.id Wire ((X + Y) + Z)))
          (Component.Impl.symmetry Wire X (Y + Z)))
        (Component.Impl.recast rfl (Nat.add_assoc Y Z X) (Component.Impl.id Wire ((Y + Z) + X))))
      (Component.Impl.sequential
        (Component.Impl.sequential
          (Component.Impl.parallel (Component.Impl.symmetry Wire X Y) (Component.Impl.id Wire Z))
          (Component.Impl.recast rfl (Nat.add_assoc Y X Z) (Component.Impl.id Wire ((Y + X) + Z))))
        (Component.Impl.parallel (Component.Impl.id Wire Y) (Component.Impl.symmetry Wire X Z)))
      (((), ()), ()) ((((), ()), ()), ((), ())) := by

Dependencies: Component.Impl.id, Component.Impl.parallel, Component.Impl.recast, Component.Impl.sequential, Component.Impl.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: Component.Impl.equivalent_of_stationary, Fin.append_eval

Mathlib dependencies: Fin.append, Norm, add_tsub_cancel_left

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.mpr_not, Eq.mpr_prop, Eq.symm, Eq.trans, False, False.elim, Fin, Fin.cast, Fin.castAdd, Fin.ext, Fin.natAdd, Function.comp, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.natCast_nonneg, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.ofNat_sub_sub, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.add_assoc, Nat.cast, Nat.le_of_not_lt, Nat.lt_add_right, Nat.lt_or_gt_of_ne, Nonempty, Not, Or.elim, Prod, Unit, Unit.unit, congr, congrArg, congrFun', dif_neg, dif_pos, dite, dite_congr, funext, id, le_of_le_of_eq, of_decide_eq_true, rfl

Used by: Component.Impl.Hom.hexagon_forward

TipComponent.Impl.hexagon_reverse_arrow

The second hexagon identity, at the arrow level: the mirror image of hexagon_forward_arrow, using inverse associators (i.e. re-associating the other way).

theorem Component.Impl.hexagon_reverse_arrow (X Y Z : Nat) :
    InformationSystem.equivalent
      (Component.Impl.sequential
        (Component.Impl.sequential
          (Component.Impl.recast rfl (Nat.add_assoc X Y Z).symm (Component.Impl.id Wire (X + (Y + Z))))
          (Component.Impl.symmetry Wire (X + Y) Z))
        (Component.Impl.recast rfl (Nat.add_assoc Z X Y).symm (Component.Impl.id Wire (Z + (X + Y)))))
      (Component.Impl.sequential
        (Component.Impl.sequential
          (Component.Impl.parallel (Component.Impl.id Wire X) (Component.Impl.symmetry Wire Y Z))
          (Component.Impl.recast rfl (Nat.add_assoc X Z Y).symm (Component.Impl.id Wire (X + (Z + Y)))))
        (Component.Impl.parallel (Component.Impl.symmetry Wire X Z) (Component.Impl.id Wire Y)))
      (((), ()), ()) ((((), ()), ()), ((), ())) := by

Dependencies: Component.Impl.id, Component.Impl.parallel, Component.Impl.recast, Component.Impl.sequential, Component.Impl.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: Component.Impl.equivalent_of_stationary, Fin.append_eval

Mathlib dependencies: Fin.append, Norm, add_tsub_cancel_left

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.mpr_not, Eq.mpr_prop, Eq.symm, Eq.trans, False, False.elim, Fin, Fin.cast, Fin.castAdd, Fin.ext, Fin.natAdd, Function.comp, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.natCast_nonneg, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.ofNat_sub_sub, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.coordinate_eval_6, Lean.Omega.LinearCombo.coordinate_eval_7, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.add_assoc, Nat.add_lt_add_left, Nat.cast, Nat.le_of_not_lt, Nat.lt_or_gt_of_ne, Nonempty, Not, Or.elim, Prod, Unit, Unit.unit, congr, congrArg, congrFun', dif_neg, dif_pos, dite, dite_congr, funext, id, le_of_le_of_eq, of_decide_eq_true, rfl

Used by: Component.Impl.Hom.hexagon_reverse

TipComponent.Impl.Hom.hexagon_forward

The Hom-level version of Component.Impl.hexagon_forward_arrow.

theorem Component.Impl.Hom.hexagon_forward (X Y Z : Nat) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.comp
      (Component.Impl.Hom.comp
        (Component.Impl.Hom.recast rfl (Nat.add_assoc X Y Z) (Component.Impl.Hom.id Wire ((X + Y) + Z)))
        (Component.Impl.Hom.symmetry Wire X (Y + Z)))
      (Component.Impl.Hom.recast rfl (Nat.add_assoc Y Z X) (Component.Impl.Hom.id Wire ((Y + Z) + X))) =
    Component.Impl.Hom.comp
      (Component.Impl.Hom.comp
        (Component.Impl.Hom.tensor (Component.Impl.Hom.symmetry Wire X Y) (Component.Impl.Hom.id Wire Z))
        (Component.Impl.Hom.recast rfl (Nat.add_assoc Y X Z) (Component.Impl.Hom.id Wire ((Y + X) + Z))))
      (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire Y) (Component.Impl.Hom.symmetry Wire X Z)) :=

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.hexagon_forward_arrow, Component.Impl.id, Component.Impl.parallel, Component.Impl.recast, Component.Impl.sequential, Component.Impl.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance, rfl

Used by: Component.Impl.braidedCategory

TipComponent.Impl.Hom.hexagon_reverse

The Hom-level version of Component.Impl.hexagon_reverse_arrow.

theorem Component.Impl.Hom.hexagon_reverse (X Y Z : Nat) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.comp
      (Component.Impl.Hom.comp
        (Component.Impl.Hom.recast rfl (Nat.add_assoc X Y Z).symm
          (Component.Impl.Hom.id Wire (X + (Y + Z))))
        (Component.Impl.Hom.symmetry Wire (X + Y) Z))
      (Component.Impl.Hom.recast rfl (Nat.add_assoc Z X Y).symm
        (Component.Impl.Hom.id Wire (Z + (X + Y)))) =
    Component.Impl.Hom.comp
      (Component.Impl.Hom.comp
        (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire X) (Component.Impl.Hom.symmetry Wire Y Z))
        (Component.Impl.Hom.recast rfl (Nat.add_assoc X Z Y).symm
          (Component.Impl.Hom.id Wire (X + (Z + Y)))))
      (Component.Impl.Hom.tensor (Component.Impl.Hom.symmetry Wire X Z) (Component.Impl.Hom.id Wire Y)) :=

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.Hom.symmetry, Component.Impl.Hom.tensor

Proof dependencies: Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.hexagon_reverse_arrow, Component.Impl.id, Component.Impl.parallel, Component.Impl.recast, Component.Impl.sequential, Component.Impl.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.symm, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance, rfl

Used by: Component.Impl.braidedCategory

NoteComponent.Impl.braidedCategory

Component.Impl, bundled with a state and quotiented by InformationSystem.equivalent, forms a genuine BraidedCategory: Component.Impl.symmetry is the braiding, and every coherence law reduces either to the recast/eqToHom proof-irrelevance argument from MonoidalCategory (naturality) or to the Fin-index computations above (the two hexagons).

@[reducible] noncomputable def Component.Impl.braidedCategory
    (Wire : Type) [Nonempty Wire] [Norm Wire] :
    letI := Component.Impl.category Wire
    letI := Component.Impl.monoidalCategoryStruct Wire
    letI := Component.Impl.monoidalCategory Wire
    CategoryTheory.BraidedCategory Nat :=
  letI := Component.Impl.category Wire
  letI := Component.Impl.monoidalCategoryStruct Wire
  letI := Component.Impl.monoidalCategory Wire
  { braiding := Component.Impl.braiding Wire
    braiding_naturality_right := fun X {_ _} f => Component.Impl.braiding_naturality_right f
    braiding_naturality_left := fun {_ _} f Z => Component.Impl.braiding_naturality_left f
    hexagon_forward := fun X Y Z => by
      change Component.Impl.Hom.comp (eqToIso (Nat.add_assoc X Y Z)).hom
          (Component.Impl.Hom.comp (Component.Impl.braiding Wire X (Y + Z)).hom
            (eqToIso (Nat.add_assoc Y Z X)).hom) =
        Component.Impl.Hom.comp
          (Component.Impl.Hom.tensor (Component.Impl.braiding Wire X Y).hom (Component.Impl.Hom.id Wire Z))
          (Component.Impl.Hom.comp (eqToIso (Nat.add_assoc Y X Z)).hom
            (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire Y) (Component.Impl.braiding Wire X Z).hom))
      rw [eqToIso.hom, eqToIso.hom, eqToIso.hom,
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc X Y Z),
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc Y Z X),
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc Y X Z),
        ← Component.Impl.Hom.comp_assoc, ← Component.Impl.Hom.comp_assoc]
      exact Component.Impl.Hom.hexagon_forward X Y Z
    hexagon_reverse := fun X Y Z => by
      change Component.Impl.Hom.comp (eqToIso (Nat.add_assoc X Y Z)).inv
          (Component.Impl.Hom.comp (Component.Impl.braiding Wire (X + Y) Z).hom
            (eqToIso (Nat.add_assoc Z X Y)).inv) =
        Component.Impl.Hom.comp
          (Component.Impl.Hom.tensor (Component.Impl.Hom.id Wire X) (Component.Impl.braiding Wire Y Z).hom)
          (Component.Impl.Hom.comp (eqToIso (Nat.add_assoc X Z Y)).inv
            (Component.Impl.Hom.tensor (Component.Impl.braiding Wire X Z).hom (Component.Impl.Hom.id Wire Y)))
      rw [eqToIso.inv, eqToIso.inv, eqToIso.inv,
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc X Y Z).symm,
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc Z X Y).symm,
        Component.Impl.Hom.eqToHom_eq_recast_id (Nat.add_assoc X Z Y).symm,
        ← Component.Impl.Hom.comp_assoc, ← Component.Impl.Hom.comp_assoc]
      exact Component.Impl.Hom.hexagon_reverse X Y Z }

Outer dependencies: Component.Impl.category, Component.Impl.monoidalCategory

Inner dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.comp_assoc, Component.Impl.Hom.eqToHom_eq_recast_id, Component.Impl.Hom.hexagon_forward, Component.Impl.Hom.hexagon_reverse, Component.Impl.Hom.id, Component.Impl.Hom.recast, Component.Impl.Hom.tensor, Component.Impl.braiding, Component.Impl.braiding_naturality_left, Component.Impl.braiding_naturality_right

Mathlib dependencies: CategoryTheory.BraidedCategory, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.eqToIso.hom, CategoryTheory.eqToIso.inv, Norm

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Nat, Nat.add_assoc, Nonempty, congrArg, id, rfl

Used by: instBraidedCategoryPROP

As a genuine Mathlib instance

Component.Impl.category/Component.Impl.monoidalCategory/Component.Impl.braidedCategory are defs, not instances: Lean’s typeclass search can’t find [CategoryTheory.Category Nat] on its own, since Nat alone doesn’t remember which Wire type the wires carry — for a different Wire, the same Nat would need a genuinely different Hom/comp. Component.Impl.PROP Wire fixes this the way Mathlib’s Additive/Multiplicative/OrderDual fix the analogous problem: it is definitionally just Nat, existing purely so instance search has a type to unify Wire against. With that, Component.Impl.PROP Wire genuinely is a symmetric-monoidal PROP in Mathlib’s own sense — Y ⊗ Z, f ≫ g, β_ X Y, and every lemma about Category/MonoidalCategory/BraidedCategory in Mathlib now apply to it directly, no unfolding required.

NoteComponent.Impl.PROP

Component.Impl’s wire counts, retagged so a Wire type can be recovered from the type alone — see the section docs above. Definitionally just Nat.

def Component.Impl.PROP (Wire : Type) [Nonempty Wire] [Norm Wire] : Type := Nat

Outer dependencies: (none)

Mathlib dependencies: Norm

Lean core dependencies: Nat, Nonempty

Used by: Component.Impl.toSpecFunctor, instBraidedCategoryPROP, instCategoryPROP, instMonoidalCategoryPROP

ImportantinstCategoryPROP

noncomputable instance : CategoryTheory.Category (Component.Impl.PROP Wire) := Component.Impl.category Wire

Outer dependencies: Component.Impl.PROP

Inner dependencies: Component.Impl.category

Mathlib dependencies: CategoryTheory.Category, Norm

Lean core dependencies: Nonempty

Used by: Component.Impl.toSpecFunctor, instBraidedCategoryPROP, instMonoidalCategoryPROP

ImportantinstMonoidalCategoryPROP

noncomputable instance : CategoryTheory.MonoidalCategory (Component.Impl.PROP Wire) :=
  Component.Impl.monoidalCategory Wire

Outer dependencies: Component.Impl.PROP, instCategoryPROP

Inner dependencies: Component.Impl.monoidalCategory

Mathlib dependencies: CategoryTheory.MonoidalCategory, Norm

Lean core dependencies: Nonempty

Used by: instBraidedCategoryPROP

ImportantinstBraidedCategoryPROP

noncomputable instance : CategoryTheory.BraidedCategory (Component.Impl.PROP Wire) :=
  Component.Impl.braidedCategory Wire

Outer dependencies: Component.Impl.PROP, instCategoryPROP, instMonoidalCategoryPROP

Inner dependencies: Component.Impl.braidedCategory

Mathlib dependencies: CategoryTheory.BraidedCategory, Norm

Lean core dependencies: Nonempty

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend