FunctionalityCategory

Difficulty: optional — 6 definitions, 0 abbreviations, 0 lemmas, 19 theorems.

definition theorem

legend

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

Every coherence law below is proved by transport, not by redoing the underlying Fin-index arithmetic a third time: Component.Func.toSpec is injective (Component.Func.toSpec_injective) and commutes with every one of these operations (Component.Func.toSpec_sequential, Component.Spec.parallel_toSpec_eq, id_eq_toSpec, symmetry_eq_toSpec, recast_toSpec_eq), so a Component.Func equation is provable by pushing .toSpec through both sides and citing the already-proven Component.Spec analogue.

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

NoteComponent.Func.PROP

Component.Func’s own wire counts, retagged so a Wire type can be recovered from the type alone — the same PROP trick Component.Impl.PROP/Component.Spec.PROP use. Definitionally just Nat.

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

Outer dependencies: (none)

Lean core dependencies: Nat

Used by: instBraidedCategoryPROP_2, instCategoryPROP_2, instMonoidalCategoryPROP_2

NoteComponent.Func.category

Component.Func genuinely forms a Category: objects are wire counts, morphisms are rules, composition is Component.Func.sequential. Every law here is rfl — a rule is a plain function, so composing rules is plain function composition, associative and unital on the nose.

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

Outer dependencies: (none)

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

Mathlib dependencies: CategoryTheory.Category

Lean core dependencies: Nat

Used by: Component.Func.braidedCategory, Component.Func.braiding, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.eqToHom_eq_recast_id, Component.Func.monoidalCategory, Component.Func.monoidalCategoryStruct, Component.Func.recast_eqToHom, instCategoryPROP_2

NoteComponent.Func.monoidalCategoryStruct

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

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

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

Mathlib dependencies: CategoryTheory.MonoidalCategoryStruct, CategoryTheory.eqToIso

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

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.parallel_id_id

Placing two identity rules side by side is again an identity rule — transported directly from Component.Spec.parallel_id_id via Component.Func.toSpec_injective.

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

Dependencies: Component.Func, Component.Func.id, Component.Func.parallel

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Spec, Component.Spec.id, Component.Spec.id_eq_toSpec, Component.Spec.parallel, Component.Spec.parallel_id_id, Component.Spec.parallel_toSpec_eq

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

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.parallel_id_zero_left

Tensoring with the empty rule (the 0-wire identity) on the left does nothing, up to reindexing across 0 + n = n — transported from Component.Spec.parallel_id_zero_left.

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

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

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Spec, Component.Spec.id, Component.Spec.id_eq_toSpec, Component.Spec.parallel, Component.Spec.parallel_id_zero_left, Component.Spec.parallel_toSpec_eq, Component.Spec.recast, Component.Spec.recast_toSpec_eq

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Nat, Nat.zero_add, congrArg, congrFun', id

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.parallel_id_zero_right

Tensoring with the empty rule (the 0-wire identity) on the right does nothing, up to reindexing across n + 0 = n — transported from Component.Spec.parallel_id_zero_right.

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

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

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Spec, Component.Spec.id, Component.Spec.id_eq_toSpec, Component.Spec.parallel, Component.Spec.parallel_id_zero_right, Component.Spec.parallel_toSpec_eq, Component.Spec.recast, Component.Spec.recast_toSpec_eq

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Nat, Nat.add_zero, congrArg, congrFun', id

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.recast_recast

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

theorem Component.Func.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.Func Wire Wire n m) :
    Component.Func.recast h1' h2' (Component.Func.recast h1 h2 f) =
      Component.Func.recast (h1.trans h1') (h2.trans h2') f := by

Dependencies: Component.Func, Component.Func.recast

Lean core dependencies: Eq, Eq.trans, Nat

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.eqToHom_eq_recast_id

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

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

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

Mathlib dependencies: CategoryTheory.eqToHom

Lean core dependencies: Eq, Nat, rfl

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

ImportantComponent.Func.comp_eqToHom

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

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

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

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

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.eqToHom_comp

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

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

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

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

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.recast_eqToHom

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

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

Dependencies: Component.Func, Component.Func.category, Component.Func.recast

Mathlib dependencies: CategoryTheory.eqToHom

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

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.recast_parallel_left

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

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

Dependencies: Component.Func, Component.Func.parallel, Component.Func.recast

Lean core dependencies: Eq, Nat, congrArg

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.recast_parallel_right

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

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

Dependencies: Component.Func, Component.Func.parallel, Component.Func.recast

Lean core dependencies: Eq, Nat, congrArg

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.parallel_assoc

Placing rules side by side is associative, up to Component.Func.recast lining up the two sides’ wire counts — transported from Component.Spec.parallel_assoc.

theorem Component.Func.parallel_assoc {Wire : Type} {n1 m1 n2 m2 n3 m3 : Nat}
    (f1 : Component.Func Wire Wire n1 m1) (f2 : Component.Func Wire Wire n2 m2)
    (f3 : Component.Func Wire Wire n3 m3) :
    Component.Func.recast (Nat.add_assoc n1 n2 n3) (Nat.add_assoc m1 m2 m3)
        (Component.Func.parallel (Component.Func.parallel f1 f2) f3) =
      Component.Func.parallel f1 (Component.Func.parallel f2 f3) := by

Dependencies: Component.Func, Component.Func.parallel, Component.Func.recast

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Spec, Component.Spec.parallel, Component.Spec.parallel_assoc, Component.Spec.parallel_toSpec_eq, Component.Spec.recast, Component.Spec.recast_toSpec_eq

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Nat, Nat.add_assoc, congr, congrArg, congrFun', id

Used by: Component.Func.monoidalCategory

ImportantComponent.Func.symmetry_symmetry

Composing the symmetry rule with itself, both ways round, undoes the swap — transported from Component.Spec.symmetry_symmetry.

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

Dependencies: Component.Func, Component.Func.id, Component.Func.recast, Component.Func.sequential, Component.Func.symmetry

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Func.toSpec_sequential, Component.Spec, Component.Spec.id, Component.Spec.id_eq_toSpec, Component.Spec.recast, Component.Spec.recast_toSpec_eq, Component.Spec.sequential, Component.Spec.symmetry, Component.Spec.symmetry_eq_toSpec, Component.Spec.symmetry_symmetry

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

Used by: Component.Func.symmetry_symmetry'

ImportantComponent.Func.parallel_comm

Swapping two rules placed in parallel is the same as placing the swapped pair in the other order, up to rewiring both ends with Component.Func.symmetry — transported from Component.Spec.parallel_comm.

theorem Component.Func.parallel_comm {Wire : Type} {n1 m1 n2 m2 : Nat}
    (f1 : Component.Func Wire Wire n1 m1) (f2 : Component.Func Wire Wire n2 m2) :
    Component.Func.parallel f1 f2 =
      Component.Func.sequential
        (Component.Func.sequential (Component.Func.symmetry Wire n1 n2)
          (Component.Func.parallel f2 f1))
        (Component.Func.symmetry Wire m2 m1) := by

Dependencies: Component.Func, Component.Func.parallel, Component.Func.sequential, Component.Func.symmetry

Proof dependencies: Component.Func.toSpec, Component.Func.toSpec_injective, Component.Func.toSpec_sequential, Component.Spec, Component.Spec.parallel, Component.Spec.parallel_comm, Component.Spec.parallel_toSpec_eq, Component.Spec.sequential, Component.Spec.symmetry, Component.Spec.symmetry_eq_toSpec

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Eq.trans, Nat, congr, congrArg, congrFun', id

Used by: Component.Func.braidedCategory

NoteComponent.Func.monoidalCategory

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

Outer dependencies: Component.Func.category

Inner dependencies: Component.Func, Component.Func.comp_eqToHom, Component.Func.eqToHom_comp, Component.Func.eqToHom_eq_recast_id, Component.Func.id, Component.Func.monoidalCategoryStruct, Component.Func.parallel, Component.Func.parallel_assoc, Component.Func.parallel_id_id, Component.Func.parallel_id_zero_left, Component.Func.parallel_id_zero_right, Component.Func.parallel_sequential, Component.Func.recast, Component.Func.recast_eqToHom, Component.Func.recast_parallel_left, Component.Func.recast_parallel_right, Component.Func.recast_recast, Component.Func.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.Func.braidedCategory, instMonoidalCategoryPROP_2

ImportantComponent.Func.symmetry_symmetry'

Component.Func.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.Func.symmetry_symmetry' {Wire : Type} (n m : Nat) :
    Component.Func.sequential
        (Component.Func.symmetry Wire n m) (Component.Func.symmetry Wire m n) =
      Component.Func.id Wire (n + m) := by

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

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

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

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

NoteComponent.Func.braiding

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

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

Outer dependencies: Component.Func.category

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

Mathlib dependencies: CategoryTheory.Iso

Lean core dependencies: Nat

Used by: Component.Func.braidedCategory

The hexagons

Unlike Component.Spec’s, Component.Func’s hexagons don’t need any collapsing step first: a rule already is the plain Fin-index function Component.Spec.hexagon_forward/hexagon_reverse had to work to reduce down to via Component.Func.toSpec. So the exact same closing tactic applies directly, one layer earlier.

ImportantComponent.Func.hexagon_forward

The first hexagon identity for Component.Func.

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

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

Proof dependencies: 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.Func.braidedCategory

ImportantComponent.Func.hexagon_reverse

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

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

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

Proof dependencies: 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.Func.braidedCategory

NoteComponent.Func.braidedCategory

Component.Func genuinely forms a BraidedCategory, with Component.Func.braiding as the braiding. Every coherence law is fully proved: both naturality laws via Component.Func.parallel_comm, and both hexagons via Component.Func.hexagon_forward/ hexagon_reverse above.

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

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

Inner dependencies: Component.Func, Component.Func.braiding, Component.Func.eqToHom_eq_recast_id, Component.Func.hexagon_forward, Component.Func.hexagon_reverse, Component.Func.id, Component.Func.parallel, Component.Func.parallel_comm, Component.Func.recast, Component.Func.sequential, Component.Func.sequential_assoc, Component.Func.sequential_id, Component.Func.symmetry, Component.Func.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_2

As a genuine Mathlib instance

ImportantinstCategoryPROP_2

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

Outer dependencies: Component.Func.PROP

Inner dependencies: Component.Func.category

Mathlib dependencies: CategoryTheory.Category

Used by: instBraidedCategoryPROP_2, instMonoidalCategoryPROP_2

ImportantinstMonoidalCategoryPROP_2

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

Outer dependencies: Component.Func.PROP, instCategoryPROP_2

Inner dependencies: Component.Func.monoidalCategory

Mathlib dependencies: CategoryTheory.MonoidalCategory

Used by: instBraidedCategoryPROP_2

ImportantinstBraidedCategoryPROP_2

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

Outer dependencies: Component.Func.PROP, instCategoryPROP_2, instMonoidalCategoryPROP_2

Inner dependencies: Component.Func.braidedCategory

Mathlib dependencies: CategoryTheory.BraidedCategory

Used by: (none)

Dependency diagram

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

definitiontheoremdeclared elsewheredependencyproof dependency

legend