SpecificationCategory

Difficulty: optional — 11 definitions, 0 abbreviations, 1 lemmas, 24 theorems.

definition lemma theorem
legend

Specifications form a PROP too, the same shape ImplementationCategory already gave Component.Impl: a category whose objects are wire counts, with Component.Spec.sequential as composition and Component.Spec.parallel as the monoidal (side-by-side) tensor.

This one is considerably lighter than Component.Impl’s: a specification carries no state, so Component.Spec.sequential is associative and unital exactly, not merely up to some further equivalence — no quotient, no Hom-as-Setoid, none of ImplementationCategory’s machinery for reconciling nested state products is needed here at all.

This file is marked @[difficulty "optional"], matching its sibling: it consolidates the advanced, formalism-heavy proof that Component.Spec genuinely forms a Category/ MonoidalCategory/BraidedCategory in Mathlib’s own sense. None of the rest of the course depends on reading it.

Component.Spec’s own wire counts, retagged so a Wire type can be recovered from the type alone — the same PROP trick Component.Impl.PROP uses, for the same reason: Nat alone doesn’t remember which Wire type the wires carry. Definitionally just Nat; Wire itself is only ever needed at the type level (for instance search to unify against), never in the body.

def Component.Spec.PROP (Wire : Type) : Type := Nat

Outer dependencies: (none)

Lean core dependencies: Nat

Used by: Component.Impl.toSpecFunctor, instBraidedCategoryPROP_1, instCategoryPROP_1, instMonoidalCategoryPROP_1

Component.Spec genuinely forms a Category: objects are wire counts, morphisms are specifications, composition is Component.Spec.sequential. Unlike Component.Impl.category, every law here is the literal Eq already proved above — nothing to quotient.

@[reducible] def Component.Spec.category (Wire : Type) : CategoryTheory.Category Nat where
  Hom n m := Component.Spec Wire Wire n m
  id n := Component.Spec.id Wire n
  comp f g := Component.Spec.sequential f g
  id_comp := Component.Spec.id_sequential
  comp_id := Component.Spec.sequential_id
  assoc := Component.Spec.sequential_assoc

Outer dependencies: (none)

Inner dependencies: Component.Spec, Component.Spec.id, Component.Spec.id_sequential, Component.Spec.sequential, Component.Spec.sequential_assoc, Component.Spec.sequential_id

Mathlib dependencies: CategoryTheory.Category

Lean core dependencies: Nat

Used by: Component.Spec.braidedCategory, Component.Spec.braiding, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp, Component.Spec.eqToHom_eq_recast_id, Component.Spec.monoidalCategory, Component.Spec.monoidalCategoryStruct, Component.Spec.recast_eqToHom, instCategoryPROP_1

The tensor of Component.Spec.category Wire: tensorObj := (+), tensorHom := Component.Spec.parallel, identity/associator/unitors via eqToIso on the corresponding Nat equalities — the same shape as Component.Impl.monoidalCategoryStruct.

@[reducible] def Component.Spec.monoidalCategoryStruct (Wire : Type) :
    @MonoidalCategoryStruct Nat (Component.Spec.category Wire) :=
  letI := Component.Spec.category Wire
  { tensorObj := fun n m => n + m
    whiskerLeft := fun n {_ _} f => Component.Spec.parallel (Component.Spec.id Wire n) f
    whiskerRight := fun {_ _} f m => Component.Spec.parallel f (Component.Spec.id Wire m)
    tensorHom := fun f g => Component.Spec.parallel 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.Spec.category

Inner dependencies: Component.Spec.id, Component.Spec.parallel

Mathlib dependencies: CategoryTheory.MonoidalCategoryStruct, CategoryTheory.eqToIso

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

Used by: Component.Spec.monoidalCategory

Placing two identity specifications side by side is again an identity specification: a value on n + m wires is fixed exactly when its first n and last m wires each are.

theorem Component.Spec.parallel_id_id {Wire : Type} (n m : Nat) :
    Component.Spec.parallel (Component.Spec.id Wire n) (Component.Spec.id Wire m) =
      Component.Spec.id Wire (n + m) := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.parallel

Lean core dependencies: And, Eq, Fin, Fin.addCases, Fin.castAdd, Fin.natAdd, Nat, congrFun, funext, id, rfl

Used by: Component.Func.parallel_id_id, Component.Spec.monoidalCategory

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

theorem Component.Spec.parallel_id_zero_left {Wire : Type} {n m : Nat}
    (f : Component.Spec Wire Wire n m) :
    Component.Spec.recast (Nat.zero_add n) (Nat.zero_add m)
      (Component.Spec.parallel (Component.Spec.id Wire 0) f) = f := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.parallel, Component.Spec.recast

Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.cast, Fin.castAdd, Fin.elim0, Fin.ext, Fin.natAdd, Fin.natAdd_zero, Function.comp, Nat, Nat.zero_add, True, congr, congrArg, congrFun, congrFun', eq_self, funext, id, of_eq_true

Used by: Component.Func.parallel_id_zero_left, Component.Spec.monoidalCategory

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

theorem Component.Spec.parallel_id_zero_right {Wire : Type} {n m : Nat}
    (f : Component.Spec Wire Wire n m) :
    Component.Spec.recast (Nat.add_zero n) (Nat.add_zero m)
      (Component.Spec.parallel f (Component.Spec.id Wire 0)) = f := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.parallel, Component.Spec.recast

Lean core dependencies: And, Eq, Eq.mpr, Fin, Fin.cast, Fin.castAdd, Fin.elim0, Fin.ext, Fin.natAdd, Function.comp, Nat, Nat.add_zero, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true

Used by: Component.Func.parallel_id_zero_right, Component.Spec.monoidalCategory

Reindexing twice is the same as reindexing once, by the composed equality.

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

Dependencies: Component.Spec, Component.Spec.recast

Lean core dependencies: Eq, Eq.trans, Nat

Used by: Component.Spec.monoidalCategory

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

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

Dependencies: Component.Spec.category, Component.Spec.id, Component.Spec.recast

Mathlib dependencies: CategoryTheory.eqToHom

Lean core dependencies: Eq, Nat, rfl

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

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

theorem Component.Spec.comp_eqToHom {Wire : Type} {n m p : Nat} (h : m = p)
    (f : Component.Spec Wire Wire n m) :
    letI := Component.Spec.category Wire
    Component.Spec.sequential f (eqToHom h) = Component.Spec.recast rfl h f := by

Dependencies: Component.Spec, Component.Spec.category, Component.Spec.recast, Component.Spec.sequential

Proof dependencies: Component.Spec.id, Component.Spec.sequential_id

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Spec.monoidalCategory

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

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

Dependencies: Component.Spec, Component.Spec.category, Component.Spec.recast, Component.Spec.sequential

Proof dependencies: Component.Spec.id, Component.Spec.id_sequential

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Spec.monoidalCategory

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

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

Dependencies: Component.Spec, Component.Spec.category, Component.Spec.recast

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Spec.monoidalCategory

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

theorem Component.Spec.recast_parallel_left {Wire : Type} {n1 n1' m1 m1' n2 m2 : Nat}
    (hn : n1 = n1') (hm : m1 = m1')
    (f1 : Component.Spec Wire Wire n1 m1) (f2 : Component.Spec Wire Wire n2 m2) :
    Component.Spec.parallel (Component.Spec.recast hn hm f1) f2 =
      Component.Spec.recast (congrArg (· + n2) hn) (congrArg (· + m2) hm)
        (Component.Spec.parallel f1 f2) := by

Dependencies: Component.Spec, Component.Spec.parallel, Component.Spec.recast

Lean core dependencies: Eq, Nat, congrArg

Used by: Component.Spec.monoidalCategory

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

theorem Component.Spec.recast_parallel_right {Wire : Type} {n1 m1 n2 n2' m2 m2' : Nat}
    (hn : n2 = n2') (hm : m2 = m2')
    (f1 : Component.Spec Wire Wire n1 m1) (f2 : Component.Spec Wire Wire n2 m2) :
    Component.Spec.parallel f1 (Component.Spec.recast hn hm f2) =
      Component.Spec.recast (congrArg (n1 + ·) hn) (congrArg (m1 + ·) hm)
        (Component.Spec.parallel f1 f2) := by

Dependencies: Component.Spec, Component.Spec.parallel, Component.Spec.recast

Lean core dependencies: Eq, Nat, congrArg

Used by: Component.Spec.monoidalCategory

@[reducible] noncomputable def Component.Spec.monoidalCategory (Wire : Type) :
    letI := Component.Spec.category Wire
    letI := Component.Spec.monoidalCategoryStruct Wire
    MonoidalCategory Nat :=
  letI := Component.Spec.category Wire
  letI := Component.Spec.monoidalCategoryStruct Wire
  MonoidalCategory.ofTensorHom
    (id_tensorHom_id := Component.Spec.parallel_id_id)
    (id_tensorHom := by intros; rfl)
    (tensorHom_id := by intros; rfl)
    (tensorHom_comp_tensorHom := fun f1 f2 g1 g2 =>
      (Component.Spec.parallel_sequential f1 g1 f2 g2).symm)
    (associator_naturality := by
      intro n1 n2 n3 m1 m2 m3 f1 f2 f3
      change Component.Spec.sequential
          (Component.Spec.parallel (Component.Spec.parallel f1 f2) f3)
          (eqToIso (Nat.add_assoc m1 m2 m3)).hom =
        Component.Spec.sequential (eqToIso (Nat.add_assoc n1 n2 n3)).hom
          (Component.Spec.parallel f1 (Component.Spec.parallel f2 f3))
      rw [eqToIso.hom, eqToIso.hom, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp,
        ← Component.Spec.parallel_assoc, Component.Spec.recast_recast])
    (leftUnitor_naturality := by
      intro n m f
      change Component.Spec.sequential (Component.Spec.parallel (Component.Spec.id Wire 0) f)
          (eqToIso (Nat.zero_add m)).hom = Component.Spec.sequential (eqToIso (Nat.zero_add n)).hom f
      rw [eqToIso.hom, eqToIso.hom, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp]
      have := congrArg (Component.Spec.recast (Nat.zero_add n).symm rfl)
        (Component.Spec.parallel_id_zero_left f)
      rwa [Component.Spec.recast_recast] at this)
    (rightUnitor_naturality := by
      intro n m f
      change Component.Spec.sequential (Component.Spec.parallel f (Component.Spec.id Wire 0))
          (eqToIso (Nat.add_zero m)).hom = Component.Spec.sequential (eqToIso (Nat.add_zero n)).hom f
      rw [eqToIso.hom, eqToIso.hom, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp]
      have := congrArg (Component.Spec.recast (Nat.add_zero n).symm rfl)
        (Component.Spec.parallel_id_zero_right f)
      rwa [Component.Spec.recast_recast] at this)
    (pentagon := by
      intro n1 n2 n3 n4
      change Component.Spec.sequential
          (Component.Spec.parallel (eqToIso (Nat.add_assoc n1 n2 n3)).hom (Component.Spec.id Wire n4))
          (Component.Spec.sequential (eqToIso (Nat.add_assoc n1 (n2 + n3) n4)).hom
            (Component.Spec.parallel (Component.Spec.id Wire n1)
              (eqToIso (Nat.add_assoc n2 n3 n4)).hom)) =
        Component.Spec.sequential (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.Spec.eqToHom_eq_recast_id (Nat.add_assoc n1 n2 n3),
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc n2 n3 n4),
        Component.Spec.recast_parallel_left, Component.Spec.recast_parallel_right,
        Component.Spec.parallel_id_id, Component.Spec.parallel_id_id]
      simp only [← Component.Spec.eqToHom_eq_recast_id]
      simp only [Component.Spec.comp_eqToHom, Component.Spec.recast_eqToHom])
    (triangle := by
      intro n m
      change Component.Spec.sequential (eqToIso (Nat.add_assoc n 0 m)).hom
          (Component.Spec.parallel (Component.Spec.id Wire n) (eqToIso (Nat.zero_add m)).hom) =
        Component.Spec.parallel (eqToIso (Nat.add_zero n)).hom (Component.Spec.id Wire m)
      rw [eqToIso.hom, eqToIso.hom, eqToIso.hom]
      rw [Component.Spec.eqToHom_eq_recast_id (Nat.zero_add m),
        Component.Spec.eqToHom_eq_recast_id (Nat.add_zero n),
        Component.Spec.recast_parallel_right, Component.Spec.recast_parallel_left,
        Component.Spec.parallel_id_id, Component.Spec.parallel_id_id]
      simp only [← Component.Spec.eqToHom_eq_recast_id]
      simp only [Component.Spec.comp_eqToHom, Component.Spec.recast_eqToHom])

Outer dependencies: Component.Spec.category

Inner dependencies: Component.Spec, Component.Spec.comp_eqToHom, Component.Spec.eqToHom_comp, Component.Spec.eqToHom_eq_recast_id, Component.Spec.id, Component.Spec.monoidalCategoryStruct, Component.Spec.parallel, Component.Spec.parallel_assoc, Component.Spec.parallel_id_id, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_id_zero_right, Component.Spec.parallel_sequential, Component.Spec.recast, Component.Spec.recast_eqToHom, Component.Spec.recast_parallel_left, Component.Spec.recast_parallel_right, Component.Spec.recast_recast, Component.Spec.sequential

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

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Nat, Nat.add_assoc, Nat.add_zero, Nat.zero_add, True, congr, congrArg, congrFun', eq_self, id, of_eq_true, rfl

Used by: Component.Spec.braidedCategory, instMonoidalCategoryPROP_1

Component.Spec.symmetry_symmetry, restated as a literal identity rather than an identity up to a trivial rfl-recast — exactly the shape Iso.hom_inv_id/Iso.inv_hom_id need below.

theorem Component.Spec.symmetry_symmetry' {Wire : Type} (n m : Nat) :
    Component.Spec.sequential
        (Component.Spec.symmetry Wire n m) (Component.Spec.symmetry Wire m n) =
      Component.Spec.id Wire (n + m) := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.sequential, Component.Spec.symmetry

Proof dependencies: Component.Spec.recast, Component.Spec.symmetry_symmetry

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

Used by: Component.Spec.braidedCategory, Component.Spec.braiding

The braiding: swapping the first n wires and the next m wires is a genuine isomorphism, its own inverse (swapped) — the same shape Component.Impl.braiding has for Component.Impl.

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

Outer dependencies: Component.Spec.category

Inner dependencies: Component.Spec.symmetry, Component.Spec.symmetry_symmetry'

Mathlib dependencies: CategoryTheory.Iso

Lean core dependencies: Nat

Used by: Component.Spec.braidedCategory

The hexagons

Every specification appearing in the hexagon identities below (recast of an id, symmetry, and their parallel placements) happens to be deterministic: the graph of one plain rule, via Component.Func.toSpec. Once every piece is rewritten into that form, Component.Spec.sequential collapses into plain function composition (Component.Func.toSpec_sequential) and Component.Spec.parallel into plain function pairing — turning each hexagon from a statement about existentially-quantified specifications into a statement about two plain Fin-index functions, provable the same direct way Component.Impl.hexagon_forward_arrow computes its Component.Impl counterpart.

Component.Func.toSpec only remembers a rule’s own graph, nothing more: two rules with the same graph are the same rule.

theorem Component.Func.toSpec_injective {Input Output : Type} {n m : Nat}
    {f g : Component.Func Input Output n m} (h : f.toSpec = g.toSpec) : f = g := by

Dependencies: Component.Func, Component.Func.toSpec, Component.Spec

Lean core dependencies: Eq, Fin, Nat, congrFun, funext, rfl

Used by: Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.symmetry_symmetry

Reindexing the graph of a rule is again the graph of the rule’s own reindexing (Component.Func.recast).

theorem Component.Spec.recast_toSpec_eq {Wire : Type} {n n' m m' : Nat} (hn : n = n') (hm : m = m')
    (f : Component.Func Wire Wire n m) :
    Component.Spec.recast hn hm (Component.Func.toSpec f) =
      Component.Func.toSpec (Component.Func.recast hn hm f) := by

Dependencies: Component.Func, Component.Func.recast, Component.Func.toSpec, Component.Spec, Component.Spec.recast

Lean core dependencies: Eq, Nat

Used by: Component.Func.parallel_assoc, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.symmetry_symmetry, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

Placing two rules’ graphs side by side is again the graph of the rules’ own parallel placement (Component.Func.parallel).

theorem Component.Spec.parallel_toSpec_eq {Wire : Type} {n1 m1 n2 m2 : Nat}
    (f1 : Component.Func Wire Wire n1 m1) (f2 : Component.Func Wire Wire n2 m2) :
    Component.Spec.parallel (Component.Func.toSpec f1) (Component.Func.toSpec f2) =
      Component.Func.toSpec (Component.Func.parallel f1 f2) := by

Dependencies: Component.Func, Component.Func.parallel, Component.Func.toSpec, Component.Spec, Component.Spec.parallel

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

Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.addCases, Fin.castAdd, Fin.natAdd, Nat, True, congrArg, congrFun', eq_self, funext, id, of_eq_true

Used by: Component.Func.parallel_assoc, Component.Func.parallel_comm, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse

Component.Spec.id is already the graph of Component.Func.id.

theorem Component.Spec.id_eq_toSpec {Wire : Type} (n : Nat) :
    Component.Spec.id Wire n = Component.Func.toSpec (Component.Func.id Wire n) := rfl

Dependencies: Component.Func.id, Component.Func.toSpec, Component.Spec, Component.Spec.id

Lean core dependencies: Eq, Nat, rfl

Used by: Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.symmetry_symmetry

Component.Spec.symmetry is already the graph of Component.Func.symmetry.

theorem Component.Spec.symmetry_eq_toSpec {Wire : Type} (n m : Nat) :
    Component.Spec.symmetry Wire n m = Component.Func.toSpec (Component.Func.symmetry Wire n m) :=

Dependencies: Component.Func.symmetry, Component.Func.toSpec, Component.Spec, Component.Spec.symmetry

Lean core dependencies: Eq, Nat, rfl

Used by: Component.Func.parallel_comm, Component.Func.symmetry_symmetry

The first hexagon identity for Component.Spec: 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. Every piece collapses to the graph of a rule (Component.Spec.recast_toSpec_eq/parallel_spec_eq/id_eq_spec/symmetry_eq_spec), so Component.Func.toSpec_injective reduces the whole identity to one equation between plain Fin permutations, closed by the same direct index computation Fin.append_eval/Fin.ext/omega give Component.Impl.hexagon_forward_arrow.

theorem Component.Spec.hexagon_forward {Wire : Type} (X Y Z : Nat) :
    Component.Spec.sequential
      (Component.Spec.sequential
        (Component.Spec.recast rfl (Nat.add_assoc X Y Z) (Component.Spec.id Wire ((X + Y) + Z)))
        (Component.Spec.symmetry Wire X (Y + Z)))
      (Component.Spec.recast rfl (Nat.add_assoc Y Z X) (Component.Spec.id Wire ((Y + Z) + X))) =
    Component.Spec.sequential
      (Component.Spec.sequential
        (Component.Spec.parallel (Component.Spec.symmetry Wire X Y) (Component.Spec.id Wire Z))
        (Component.Spec.recast rfl (Nat.add_assoc Y X Z) (Component.Spec.id Wire ((Y + X) + Z))))
      (Component.Spec.parallel (Component.Spec.id Wire Y) (Component.Spec.symmetry Wire X Z)) := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.parallel, Component.Spec.recast, Component.Spec.sequential, Component.Spec.symmetry

Proof dependencies: Component.Func, Component.Func.id, Component.Func.parallel, Component.Func.recast, Component.Func.sequential, Component.Func.symmetry, Component.Func.toSpec, Component.Func.toSpec_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.recast_toSpec_eq, Fin.append_eval

Mathlib dependencies: Fin.append, 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, Not, Or.elim, 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.Spec.braidedCategory

The second hexagon identity for Component.Spec: the mirror image of Component.Spec.hexagon_forward, using inverse associators (i.e. re-associating the other way).

theorem Component.Spec.hexagon_reverse {Wire : Type} (X Y Z : Nat) :
    Component.Spec.sequential
      (Component.Spec.sequential
        (Component.Spec.recast rfl (Nat.add_assoc X Y Z).symm (Component.Spec.id Wire (X + (Y + Z))))
        (Component.Spec.symmetry Wire (X + Y) Z))
      (Component.Spec.recast rfl (Nat.add_assoc Z X Y).symm (Component.Spec.id Wire (Z + (X + Y)))) =
    Component.Spec.sequential
      (Component.Spec.sequential
        (Component.Spec.parallel (Component.Spec.id Wire X) (Component.Spec.symmetry Wire Y Z))
        (Component.Spec.recast rfl (Nat.add_assoc X Z Y).symm (Component.Spec.id Wire (X + (Z + Y)))))
      (Component.Spec.parallel (Component.Spec.symmetry Wire X Z) (Component.Spec.id Wire Y)) := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.parallel, Component.Spec.recast, Component.Spec.sequential, Component.Spec.symmetry

Proof dependencies: Component.Func, Component.Func.id, Component.Func.parallel, Component.Func.recast, Component.Func.sequential, Component.Func.symmetry, Component.Func.toSpec, Component.Func.toSpec_sequential, Component.Spec.parallel_toSpec_eq, Component.Spec.recast_toSpec_eq, Fin.append_eval

Mathlib dependencies: Fin.append, 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, Not, Or.elim, 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.Spec.braidedCategory

Component.Spec genuinely forms a BraidedCategory, with Component.Spec.braiding as the braiding. Every coherence law is fully proved: both naturality laws via Component.Spec.parallel_comm (the Component.Spec counterpart of Component.Impl.Hom.tensor_comm), and both hexagons via Component.Spec.hexagon_forward/hexagon_reverse above.

@[reducible] noncomputable def Component.Spec.braidedCategory (Wire : Type) :
    letI := Component.Spec.category Wire
    letI := Component.Spec.monoidalCategory Wire
    CategoryTheory.BraidedCategory Nat :=
  letI := Component.Spec.category Wire
  letI := Component.Spec.monoidalCategory Wire
  { braiding := Component.Spec.braiding Wire
    braiding_naturality_right := by
      intro X Y Z f
      change Component.Spec.sequential
          (Component.Spec.parallel (Component.Spec.id Wire X) f)
          (Component.Spec.symmetry Wire X Z) =
        Component.Spec.sequential (Component.Spec.symmetry Wire X Y)
          (Component.Spec.parallel f (Component.Spec.id Wire X))
      rw [Component.Spec.parallel_comm (Component.Spec.id Wire X) f]
      rw [Component.Spec.sequential_assoc, Component.Spec.symmetry_symmetry',
        Component.Spec.sequential_id]
    braiding_naturality_left := by
      intro X Y f Z
      change Component.Spec.sequential
          (Component.Spec.parallel f (Component.Spec.id Wire Z))
          (Component.Spec.symmetry Wire Y Z) =
        Component.Spec.sequential (Component.Spec.symmetry Wire X Z)
          (Component.Spec.parallel (Component.Spec.id Wire Z) f)
      rw [Component.Spec.parallel_comm f (Component.Spec.id Wire Z)]
      rw [Component.Spec.sequential_assoc, Component.Spec.symmetry_symmetry',
        Component.Spec.sequential_id]
    hexagon_forward := by
      intro X Y Z
      change Component.Spec.sequential (eqToIso (Nat.add_assoc X Y Z)).hom
          (Component.Spec.sequential (Component.Spec.braiding Wire X (Y + Z)).hom
            (eqToIso (Nat.add_assoc Y Z X)).hom) =
        Component.Spec.sequential
          (Component.Spec.parallel (Component.Spec.braiding Wire X Y).hom (Component.Spec.id Wire Z))
          (Component.Spec.sequential (eqToIso (Nat.add_assoc Y X Z)).hom
            (Component.Spec.parallel (Component.Spec.id Wire Y) (Component.Spec.braiding Wire X Z).hom))
      rw [eqToIso.hom, eqToIso.hom, eqToIso.hom,
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc X Y Z),
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc Y Z X),
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc Y X Z),
        ← Component.Spec.sequential_assoc, ← Component.Spec.sequential_assoc]
      exact Component.Spec.hexagon_forward X Y Z
    hexagon_reverse := by
      intro X Y Z
      change Component.Spec.sequential (eqToIso (Nat.add_assoc X Y Z)).inv
          (Component.Spec.sequential (Component.Spec.braiding Wire (X + Y) Z).hom
            (eqToIso (Nat.add_assoc Z X Y)).inv) =
        Component.Spec.sequential
          (Component.Spec.parallel (Component.Spec.id Wire X) (Component.Spec.braiding Wire Y Z).hom)
          (Component.Spec.sequential (eqToIso (Nat.add_assoc X Z Y)).inv
            (Component.Spec.parallel (Component.Spec.braiding Wire X Z).hom (Component.Spec.id Wire Y)))
      rw [eqToIso.inv, eqToIso.inv, eqToIso.inv,
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc X Y Z).symm,
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc Z X Y).symm,
        Component.Spec.eqToHom_eq_recast_id (Nat.add_assoc X Z Y).symm,
        ← Component.Spec.sequential_assoc, ← Component.Spec.sequential_assoc]
      exact Component.Spec.hexagon_reverse X Y Z }

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

Inner dependencies: Component.Spec, Component.Spec.braiding, Component.Spec.eqToHom_eq_recast_id, Component.Spec.hexagon_forward, Component.Spec.hexagon_reverse, Component.Spec.id, Component.Spec.parallel, Component.Spec.parallel_comm, Component.Spec.recast, Component.Spec.sequential, Component.Spec.sequential_assoc, Component.Spec.sequential_id, Component.Spec.symmetry, Component.Spec.symmetry_symmetry'

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

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

Used by: instBraidedCategoryPROP_1

As a genuine Mathlib instance

Same trick as Component.Impl.PROP: Component.Spec.PROP Wire exists purely so instance search has a type to unify Wire against, since Nat alone can’t remember which Wire type the wires carry.

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

Outer dependencies: Component.Spec.PROP

Inner dependencies: Component.Spec.category

Mathlib dependencies: CategoryTheory.Category

Used by: Component.Impl.toSpecFunctor, instBraidedCategoryPROP_1, instMonoidalCategoryPROP_1

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

Outer dependencies: Component.Spec.PROP, instCategoryPROP_1

Inner dependencies: Component.Spec.monoidalCategory

Mathlib dependencies: CategoryTheory.MonoidalCategory

Used by: instBraidedCategoryPROP_1

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

Outer dependencies: Component.Spec.PROP, instCategoryPROP_1, instMonoidalCategoryPROP_1

Inner dependencies: Component.Spec.braidedCategory

Mathlib dependencies: CategoryTheory.BraidedCategory

Used by: (none)

Comparison: implementation to specification

Every implementation induces the specification it happens to satisfy (fix its current state, read its rule off via Component.Impl.toFunc, take that rule’s own graph via Component.Func.toSpec) — and this induced specification only depends on the implementation’s observable behaviour (InformationSystem.equivalent), never on which particular state type realizes it. That is exactly what makes it well-defined on Component.Impl.Hom (an implementation already quotiented down to its observable behaviour), and a genuine Functor between the two PROPs: composing then abstracting gives the same specification as abstracting then composing.

Read a bundled, quotiented implementation’s own specification off: the graph of the rule it follows at its current state. Well-defined since InformationSystem.equivalent arrows agree on their very next output for every input (InformationSystem.equivalent_output), which is all this depends on.

noncomputable def Component.Impl.Hom.toSpec {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : Nat}
    (f : Component.Impl.Hom Wire n m) : Component.Spec Wire Wire n m :=
  f.liftOn
    (fun a => letI := a.nonempty; letI := a.size; (a.component.toFunc a.state).toSpec)
    (fun a b hab => by
      letI := a.nonempty; letI := a.size; letI := b.nonempty; letI := b.size
      funext i o
      show (o = (a.component.step a.state i).2) = (o = (b.component.step b.state i).2)
      rw [InformationSystem.equivalent_output hab i])

Outer dependencies: Component.Impl.Hom, Component.Spec

Inner dependencies: Component.Func.toSpec, Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.toFunc, InformationSystem.equivalent_output, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks

Mathlib dependencies: Norm

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, Nonempty, Quotient.liftOn, congrArg, funext, id

Used by: Component.Impl.Hom.toSpec_comp, Component.Impl.Hom.toSpec_id, Component.Impl.toSpecFunctor

Component.Impl.Hom.toSpec sends the identity arrow to the identity specification: doing nothing, read off as a rule, is exactly the rule “hand the input straight back”.

theorem Component.Impl.Hom.toSpec_id {Wire : Type} [Nonempty Wire] [Norm Wire] (n : Nat) :
    Component.Impl.Hom.toSpec (Component.Impl.Hom.id Wire n) = Component.Spec.id Wire n := by

Dependencies: Component.Impl.Hom.id, Component.Impl.Hom.toSpec, Component.Spec, Component.Spec.id

Mathlib dependencies: Norm

Lean core dependencies: Eq, Fin, Nat, Nonempty, funext

Used by: Component.Impl.toSpecFunctor

Component.Impl.Hom.toSpec respects composition: reading off the specification of two implementations run in sequence is the same as reading off each one’s own specification first, then running those two specifications in sequence — Component.Func.toSpec_sequential, lifted from rules to bundled, quotiented implementations.

theorem Component.Impl.Hom.toSpec_comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p : Nat}
    (f : Component.Impl.Hom Wire n m) (g : Component.Impl.Hom Wire m p) :
    letI := Component.Impl.category Wire
    Component.Impl.Hom.toSpec (Component.Impl.Hom.comp f g) =
      Component.Spec.sequential (Component.Impl.Hom.toSpec f) (Component.Impl.Hom.toSpec g) := by

Dependencies: Component.Impl.Hom, Component.Impl.Hom.comp, Component.Impl.Hom.toSpec, Component.Spec, Component.Spec.sequential

Proof dependencies: Component.Func, Component.Func.sequential, Component.Func.toSpec, Component.Func.toSpec_sequential, Component.Impl.Arrow, Component.Impl.Arrow.setoid, Component.Impl.sequential, Component.Impl.toFunc, instNormProd_computerNetworks

Mathlib dependencies: Norm

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

Used by: Component.Impl.toSpecFunctor

Implementations, bundled/quotiented down to their observable behaviour, form a Functor into specifications: objects (wire counts) go straight across, and every arrow goes to the specification it satisfies. Component.Impl.Hom.toSpec_id/toSpec_comp are exactly the two laws a Functor needs.

@[reducible] noncomputable def Component.Impl.toSpecFunctor (Wire : Type) [Nonempty Wire]
    [Norm Wire] :
    letI := Component.Impl.category Wire
    letI := Component.Spec.category Wire
    Component.Impl.PROP Wire ⥤ Component.Spec.PROP Wire :=
  letI := Component.Impl.category Wire
  letI := Component.Spec.category Wire
  { obj := fun n => n
    map := fun f => Component.Impl.Hom.toSpec f
    map_id := Component.Impl.Hom.toSpec_id
    map_comp := Component.Impl.Hom.toSpec_comp }

Outer dependencies: Component.Impl.PROP, Component.Spec.PROP, instCategoryPROP, instCategoryPROP_1

Inner dependencies: Component.Impl.Hom.toSpec, Component.Impl.Hom.toSpec_comp, Component.Impl.Hom.toSpec_id

Mathlib dependencies: CategoryTheory.Functor, Norm

Lean core dependencies: Nonempty

Used by: (none)

Component.Spec.parallel is not a categorical product

Placing n wires and m wires side by side, wire-for-wire, looks at first like it should make n + m the categorical product of n and m: read off the first n wires and the last m wires separately, and every pair of maps into n and into m ought to combine into one map into n + m. That expectation holds for Component.Func, where every rule always produces some output. It fails here, because a specification is allowed to accept nothing at all.

The specification nothing ever satisfies, for any input or output whatsoever. A legitimate Component.Spec all the same — nothing requires a specification to be satisfiable.

def Component.Spec.impossible (Wire : Type) (n m : Nat) : Component.Spec Wire Wire n m :=
  fun _ _ => False

Outer dependencies: Component.Spec

Lean core dependencies: False, Fin, Nat

Used by: Component.Spec.impossible_univalent, Component.Spec.not_cartesian

The specification nothing satisfies is still univalent: with no outputs allowed at all, the requirement that any two allowed outputs agree holds with nothing to check. What breaks the product below is being unsatisfiable, not being multi-valued.

theorem Component.Spec.impossible_univalent (Wire : Type) (n m : Nat) :
    (Component.Spec.impossible Wire n m).Univalent :=

Dependencies: Component.Spec.Univalent, Component.Spec.impossible

Lean core dependencies: Eq, False.elim, Fin, Nat

Used by: (none)

Read the first n wires off an n + m-wire bundle, discarding the rest.

def Component.Spec.proj1 (Wire : Type) (n m : Nat) : Component.Spec Wire Wire (n + m) n :=
  fun iv o => o = fun k => iv (Fin.castAdd m k)

Outer dependencies: Component.Spec

Lean core dependencies: Eq, Fin, Fin.castAdd, Nat

Used by: Component.Spec.not_cartesian

Read the last m wires off an n + m-wire bundle, discarding the rest.

def Component.Spec.proj2 (Wire : Type) (n m : Nat) : Component.Spec Wire Wire (n + m) m :=
  fun iv o => o = fun k => iv (Fin.natAdd n k)

Outer dependencies: Component.Spec

Lean core dependencies: Eq, Fin, Fin.natAdd, Nat

Used by: Component.Spec.not_cartesian

n + m, together with these two projections, is not the categorical product of n and m: a genuine product needs some way to pair up any map into n with any map into m, however those two behave. Pairing the identity on n (certainly satisfiable) against the specification nothing satisfies at all has no witness whatsoever. Being satisfiable is not required of a specification, so this single unsatisfiable choice already breaks the universal property a product would need — and, since Component.Spec.impossible_univalent shows this same choice never allows more than one output either, allowing nothing at all is already enough on its own; nothing here needed a specification to allow several conflicting outputs.

theorem Component.Spec.not_cartesian (Wire : Type) [Nonempty Wire] (n m : Nat) :
    ¬ ∃ h : Component.Spec Wire Wire n (n + m),
      Component.Spec.sequential h (Component.Spec.proj1 Wire n m) = Component.Spec.id Wire n ∧
      Component.Spec.sequential h (Component.Spec.proj2 Wire n m) =
        Component.Spec.impossible Wire n m := by

Dependencies: Component.Spec, Component.Spec.id, Component.Spec.impossible, Component.Spec.proj1, Component.Spec.proj2, Component.Spec.sequential

Proof dependencies: instNonemptyForallFin_computerNetworks

Mathlib dependencies: Classical.arbitrary

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Exists, False, Fin, Fin.natAdd, Nat, Nonempty, Not, congrArg, id, rfl

Used by: (none)

Dependency diagram

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

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend