The statement surface, defined

Every definition the theorems of record are phrased in, in one self-contained module: the flag model of multigraph fragments with its gluing, fragment isomorphism, composition, the connection pairing and the edge-rank hypothesis, Eulerian edge subsets, the mixed partition function (Regts–Sevenster's Definition 5), the three named statements, the symmetric monoidal category of super vector spaces, the vocabulary of Deligne's hypotheses, and Deligne's theorem, which RS/Classical/Deligne/ proves.

This module imports only the Mathlib funnel (RS/Common/MathlibDeps.lean, an import list with no content), so its meaning is determined by this file against Mathlib alone. It is the trusted surface of the comparator certification: Challenge.lean carries a copy of the sections below, against Mathlib alone, and states the theorems of record with sorry; Solution.lean proves each by the theorem of record of the same name, against the definitions here. Comparator confirms at the kernel-export level that the two sides prove identical statements about identical definitions — the definitions below. The rest of the tree imports them from here rather than restating them, so this file is the single source of what the theorems mean.

How to read it. Each section names the theory it carries; the rest of the repository builds on these declarations by import, so what is written here is, verbatim, what the theorems of record are about. The order is: the sorting sign; fragments and gluing; fragment isomorphism; composition; connection pairings and the edge-rank hypothesis; Eulerian edge subsets; the mixed partition function; the named statements; super vector spaces; the vocabulary of Deligne's hypotheses; and Deligne's theorem.

1. Inversions and the sorting sign

The sorting sign supplies the antisymmetry of the odd-colour evaluation in Definition 5: reordering the odd colours multiplies the vertex value by the sign of the permutation, realized as (−1) to the inversion count.

def RS.inversions {α : Type} [LinearOrder α] : List α → ℕ

The number of inversions of a list over a linear order.

Equations

• RS.inversions [] = 0
• RS.inversions (a :: l) = (List.filter (fun (b : α) => decide (b < a)) l).length + RS.inversions l

def RS.sortSign {α : Type} [LinearOrder α] (l : List α) : ℤ

The sorting sign of a list: (−1) to the number of inversions.

Equations

• RS.sortSign l = (-1) ^ RS.inversions l

2. The flag model of multigraph fragments

A fragment is a finite multigraph in half-edge (flag) form: flags attach to internal vertices or to boundary labels, a fixed-point-free involution pairs flags into edges, each boundary label carries exactly one flag, and free circles are counted separately. Gluing two boundary labels either closes an edge into a free circle (when the two flags bound a common edge) or rewires the two edges end to end. These are the graphs the main theorems quantify over; ClosedFragment below is the case of no boundary labels.

structure RS.Fragment (α : Type) : Type 1

A fragment over the boundary-label type α: a finite multigraph in half-edge (flag) form whose dangling flags are labelled bijectively by α, together with a count of free circles.

• Flag : Type

  The type of flags (half-edges).

• Vertex : Type

  The type of internal vertices.

• flagFintype : Fintype self.Flag

  Flags form a finite type with decidable equality.

• flagDecEq : DecidableEq self.Flag
• vertexFintype : Fintype self.Vertex

  Vertices form a finite type.

• attach : self.Flag → self.Vertex ⊕ α

  Each flag is attached to an internal vertex or to a boundary label.

• pairing : self.Flag → self.Flag

  The edge involution: every flag has a partner.

• pairing_invol (f : self.Flag) : self.pairing (self.pairing f) = f

  The pairing is an involution.

• pairing_ne (f : self.Flag) : self.pairing f ≠ f

  The pairing has no fixed points.

• boundaryFlag : α → self.Flag

  The flag at each boundary label.

• attach_boundaryFlag (ℓ : α) : self.attach (self.boundaryFlag ℓ) = Sum.inr ℓ

  The boundary flag of ℓ is attached to ℓ.

• eq_boundaryFlag (ℓ : α) (f : self.Flag) : self.attach f = Sum.inr ℓ → f = self.boundaryFlag ℓ

  Any flag attached to ℓ is the boundary flag of ℓ.

• circles : ℕ

  Free circles, counted separately.

theorem RS.Fragment.boundaryFlag_injective {α : Type} (W : Fragment α) : Function.Injective W.boundaryFlag

Boundary flags of distinct labels are distinct.

theorem RS.Fragment.pairing_boundaryFlag_comm {α : Type} (W : Fragment α) {i j : α} (h : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) : W.pairing (W.boundaryFlag j) = W.boundaryFlag i

Bounding a common edge is symmetric in the two labels: if the flag at i pairs to the flag at j, then the flag at j pairs back to the flag at i.

def RS.Fragment.circlesOnly (c : ℕ) : Fragment Empty

The closed fragment with no flags, no vertices, and a given number of free circles.

Equations

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

def RS.Fragment.relabel {α β : Type} (W : Fragment α) (e : α ≃ β) : Fragment β

Transport a fragment along an equivalence of label types.

Equations

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

def RS.Fragment.disjUnion {α β : Type} (W₁ : Fragment α) (W₂ : Fragment β) : Fragment (α ⊕ β)

Disjoint union of fragments, over the sum of the label types.

Equations

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

Single-pair gluing

@[reducible, inline]

abbrev RS.Fragment.SurvivingLabel (α : Type) (i j : α) : Type

The labels surviving a glue at {i, j}.

Equations

• RS.Fragment.SurvivingLabel α i j = { x : α // x ≠ i ∧ x ≠ j }

@[reducible, inline]

abbrev RS.Fragment.SurvivingFlag {α : Type} (W : Fragment α) (i j : α) : Type

The flags surviving a glue at {i, j}: all but the two glued boundary flags.

Equations

• W.SurvivingFlag i j = { f : W.Flag // f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j }

theorem RS.Fragment.survivingFlag_attach_ne {α : Type} {W : Fragment α} {i j : α} (f : W.SurvivingFlag i j) : W.attach ↑f ≠ Sum.inr i ∧ W.attach ↑f ≠ Sum.inr j

A surviving flag is never attached to a glued label.

def RS.Fragment.glueAttachOn {α : Type} (W : Fragment α) (i j : α) (f : W.SurvivingFlag i j) (s : W.Vertex ⊕ α) : W.attach ↑f = s → W.Vertex ⊕ SurvivingLabel α i j

The attachment map computed at a given value of W.attach, which is supplied together with the equation identifying it. Taking the value as a parameter is what lets every proof below reason by cases on it, so glueAttach itself is never unfolded.

Equations

• W.glueAttachOn i j f (Sum.inl v) x_2 = Sum.inl v
• W.glueAttachOn i j f (Sum.inr ℓ) ha = Sum.inr ⟨ℓ, ⋯⟩

def RS.Fragment.glueAttach {α : Type} (W : Fragment α) (i j : α) (f : W.SurvivingFlag i j) : W.Vertex ⊕ SurvivingLabel α i j

The attachment map after gluing at {i, j}: unchanged, with the label type restricted to the surviving labels.

Equations

• W.glueAttach i j f = W.glueAttachOn i j f (W.attach ↑f) ⋯

theorem RS.Fragment.glueAttachOn_spec {α : Type} (W : Fragment α) (i j : α) (f : W.SurvivingFlag i j) (s : W.Vertex ⊕ α) (h : W.attach ↑f = s) : Sum.map id Subtype.val (W.glueAttachOn i j f s h) = s

glueAttachOn returns, under the label inclusion, exactly the value of attach it was handed.

theorem RS.Fragment.glueAttach_spec {α : Type} (W : Fragment α) (i j : α) (f : W.SurvivingFlag i j) : Sum.map id Subtype.val (W.glueAttach i j f) = W.attach ↑f

glueAttach agrees with attach under the label inclusion.

def RS.Fragment.rewire {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) : W.SurvivingFlag i j

The rewired pairing for an open glue (the two glued flags do not bound a common edge): the far ends of the two glued edges become partners; all other flags keep their partners.

Equations

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

theorem RS.Fragment.rewire_invol {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) : rewire hopen (rewire hopen f) = f

Rewiring across an open glue is an involution: it is the glued fragment's edge pairing.

theorem RS.Fragment.rewire_ne {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) : rewire hopen f ≠ f

And fixed-point-free, so the glued fragment is again a fragment.

The glued fragment

def RS.Fragment.glueBoundaryFlag {α : Type} (W : Fragment α) (i j : α) (ℓ : SurvivingLabel α i j) : W.SurvivingFlag i j

The boundary flag of a surviving label survives the glue.

Equations

• W.glueBoundaryFlag i j ℓ = ⟨W.boundaryFlag ↑ℓ, ⋯⟩

theorem RS.Fragment.glueAttach_inr_iff {α : Type} {W : Fragment α} {i j : α} (f : W.SurvivingFlag i j) (ℓ : SurvivingLabel α i j) : W.glueAttach i j f = Sum.inr ℓ ↔ W.attach ↑f = Sum.inr ↑ℓ

The glued attachment lands on a surviving label exactly when the original attachment lands on its underlying label.

theorem RS.Fragment.glueAttach_inl_iff {α : Type} {W : Fragment α} {i j : α} (f : W.SurvivingFlag i j) (v : W.Vertex) : W.glueAttach i j f = Sum.inl v ↔ W.attach ↑f = Sum.inl v

The glued attachment lands on a vertex exactly when the original attachment does. With glueAttach_inr_iff this characterises glueAttach, so no proof needs to unfold it.

theorem RS.Fragment.exists_glueAttach_inr {α : Type} {W : Fragment α} {i j : α} (f : W.SurvivingFlag i j) {ℓ : α} (ha : W.attach ↑f = Sum.inr ℓ) : ∃ (p : SurvivingLabel α i j), W.glueAttach i j f = Sum.inr p ∧ ↑p = ℓ

The surviving label a flag glues onto, with its equation.

theorem RS.Fragment.glueAttach_cases {α : Type} {W : Fragment α} {i j : α} {motive : W.Vertex ⊕ SurvivingLabel α i j → Prop} (f : W.SurvivingFlag i j) (hinl : ∀ (v : W.Vertex), W.attach ↑f = Sum.inl v → motive (Sum.inl v)) (hinr : ∀ (p : SurvivingLabel α i j), W.attach ↑f = Sum.inr ↑p → motive (Sum.inr p)) : motive (W.glueAttach i j f)

Case analysis on glueAttach, phrased on the value of attach. This is the eliminator every proof below uses: it replaces unfolding the definition, so glueAttach is never unfolded anywhere.

theorem RS.Fragment.glue_attach_boundaryFlag {α : Type} (W : Fragment α) (i j : α) (ℓ : SurvivingLabel α i j) : W.glueAttach i j (W.glueBoundaryFlag i j ℓ) = Sum.inr ℓ

The glued attachment of a surviving label's flag is that label.

theorem RS.Fragment.glue_eq_boundaryFlag {α : Type} (W : Fragment α) (i j : α) (ℓ : SurvivingLabel α i j) (f : W.SurvivingFlag i j) (h : W.glueAttach i j f = Sum.inr ℓ) : f = W.glueBoundaryFlag i j ℓ

A surviving flag attached to a surviving label is that label's boundary flag.

def RS.Fragment.glueWith {α : Type} (W : Fragment α) (i j : α) (p : W.SurvivingFlag i j → W.SurvivingFlag i j) (hinvol : ∀ (f : W.SurvivingFlag i j), p (p f) = f) (hne : ∀ (f : W.SurvivingFlag i j), p f ≠ f) (c : ℕ) : Fragment (SurvivingLabel α i j)

A glue at {i, j} with a prescribed pairing and circle count.

Flags, vertices, attachment and boundary flags of a single-pair glue are determined by W alone; only the pairing and the circle count tell the closed and open glues apart. Naming that common part gives the two glues a single shape, so any fact about a glue that does not mention its pairing is proved once.

Equations

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

def RS.Fragment.gluePairClosed {α : Type} (W : Fragment α) (i j : α) (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) : Fragment (SurvivingLabel α i j)

Gluing the boundary labels i ≠ j when their flags bound a common edge: the edge closes into a free circle.

Equations

• W.gluePairClosed i j hclosed = W.glueWith i j (fun (f : W.SurvivingFlag i j) => ⟨W.pairing ↑f, ⋯⟩) ⋯ ⋯ (W.circles + 1)

def RS.Fragment.gluePairOpen {α : Type} (W : Fragment α) (i j : α) (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : Fragment (SurvivingLabel α i j)

Gluing the boundary labels i ≠ j when their flags bound distinct edges: the two edges are unified by rewiring.

Equations

• W.gluePairOpen i j hij hopen = W.glueWith i j (RS.Fragment.rewire hopen) ⋯ ⋯ W.circles

def RS.Fragment.gluePair {α : Type} (W : Fragment α) (i j : α) (hij : i ≠ j) : Fragment (SurvivingLabel α i j)

Gluing a pair of distinct boundary labels: the two half-edges at i and j are joined. If they bound a common edge it closes into a free circle; otherwise their edges are unified end to end.

Equations

• W.gluePair i j hij = if hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j then W.gluePairClosed i j hclosed else W.gluePairOpen i j hij hclosed

3. Isomorphism of fragments

The hypothesis class asks parameters to be isomorphism-invariant; this is the notion of isomorphism. (RS/Novel/Skein/FragmentEquiv.lean proves the equivalences form a groupoid and are congruences for the fragment operations.)

structure RS.Fragment.Equiv {α : Type} (W₁ W₂ : Fragment α) : Type

An equivalence of fragments: a pair of type equivalences on flags and vertices commuting with attachment, pairing, and boundary-flag data, preserving the circle count.

• flagEquiv : W₁.Flag ≃ W₂.Flag

  The equivalence of flag types.

• vertexEquiv : W₁.Vertex ≃ W₂.Vertex

  The equivalence of vertex types.

• attach_comm (f : W₁.Flag) : W₂.attach (self.flagEquiv f) = Sum.map (⇑self.vertexEquiv) id (W₁.attach f)

  The flag equivalence commutes with attachment.

• pairing_comm (f : W₁.Flag) : self.flagEquiv (W₁.pairing f) = W₂.pairing (self.flagEquiv f)

  The flag equivalence commutes with pairing.

• circles_eq : W₁.circles = W₂.circles

  The circle counts agree.

4. Composition of fragments

An (s + t)-fragment and a (t + u)-fragment compose by gluing the last t labels of the first to the first t of the second, top pair first, through the single-pair gluing above; the label bookkeeping is by one-point removals of Fin indices. Composition is what the connection pairing evaluates.

Removing a point

noncomputable def RS.finRemoveEquiv {n : ℕ} (a : Fin (n + 1)) : { x : Fin (n + 1) // x ≠ a } ≃ Fin n

Removing one point from Fin (n + 1) leaves Fin n.

Equations

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

def RS.sumRemoveSplitEquiv {A B : Type} (a : A) (b : B) : { x : A ⊕ B // x ≠ Sum.inl a ∧ x ≠ Sum.inr b } ≃ { x : A // x ≠ a } ⊕ { y : B // y ≠ b }

Removing inl a and inr b from a sum splits into the two one-point removals.

Equations

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

noncomputable def RS.rightRemoveEquiv (t u : ℕ) : { x : Fin (t + 1 + u) // x ≠ ⟨t, ⋯⟩ } ≃ Fin (t + u)

Removing label t from Fin (t + 1 + u) leaves Fin (t + u).

Equations

• RS.rightRemoveEquiv t u = ((finCongr ⋯).subtypeEquiv ⋯).trans (RS.finRemoveEquiv ⟨t, ⋯⟩)

noncomputable def RS.interfaceStepEquiv (s t u : ℕ) : { x : Fin (s + t + 1) ⊕ Fin (t + 1 + u) // x ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ x ≠ Sum.inr ⟨t, ⋯⟩ } ≃ Fin (s + t) ⊕ Fin (t + u)

The label re-indexing after gluing the top interface pair: removing the last label on the left and label t on the right.

Equations

• RS.interfaceStepEquiv s t u = (RS.sumRemoveSplitEquiv ⟨s + t, ⋯⟩ ⟨t, ⋯⟩).trans ((RS.finRemoveEquiv ⟨s + t, ⋯⟩).sumCongr (RS.rightRemoveEquiv t u))

Gluing an interface

noncomputable def RS.glueInterface (s t u : ℕ) : Fragment (Fin (s + t) ⊕ Fin (t + u)) → Fragment (Fin s ⊕ Fin u)

Glue the t interface labels of a fragment over Fin (s + t) ⊕ Fin (t + u): the pairs (inl (s + k), inr k) for k < t, glued top pair first.

Equations

• RS.glueInterface s 0 x✝¹ x✝ = x✝.relabel ((finCongr ⋯).sumCongr (finCongr ⋯))
• RS.glueInterface s t.succ x✝¹ x✝ = RS.glueInterface s t x✝¹ ((x✝.gluePair (Sum.inl ⟨s + t, ⋯⟩) (Sum.inr ⟨t, ⋯⟩) ⋯).relabel (RS.interfaceStepEquiv s t x✝¹))

noncomputable def RS.Fragment.compose {s t u : ℕ} (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : Fragment (Fin (s + u))

Composition of fragments: glue the last t labels of F to the first t labels of G, in order.

Equations

• F.compose G = (RS.glueInterface s t u (F.disjUnion G)).relabel finSumFinEquiv

5. Connection pairings and the edge-rank hypothesis

The connection pairing of a parameter at arity t closes two t-fragments against each other; the edge-rank hypothesis bounds, for every t, the rank of that pairing by R ^ t, phrased as the Module.rank of the range of the curried pairing (RS/Novel/Skein/ConnectionRank.lean proves this equivalent to the finite-submatrix reading of the literature; that equivalence is a theorem about the hypothesis and is not needed to state it). EdgeRankParameter packages the hypothesis class of the forward direction: normalized at the empty graph, isomorphism-invariant, rank-bounded.

@[reducible, inline]

abbrev RS.ClosedFragment : Type 1

A closed fragment: no boundary labels.

Equations

• RS.ClosedFragment = RS.Fragment (Fin 0)

noncomputable def RS.pairClose {t : ℕ} (F G : Fragment (Fin t)) : ClosedFragment

The full closure of two t-fragments: compose them as a (0 + t)- and a (t + 0)-fragment.

Equations

• RS.pairClose F G = (F.relabel (finCongr ⋯)).compose (G.relabel (finCongr ⋯))

noncomputable def RS.connectionPairing (f : ClosedFragment → ℂ) (t : ℕ) (F G : Fragment (Fin t)) : ℂ

The connection pairing of a parameter at arity t.

Equations

• RS.connectionPairing f t F G = f (RS.pairClose F G)

noncomputable def RS.connectionMap (f : ClosedFragment → ℂ) (t : ℕ) : (Fragment (Fin t) →₀ ℂ) →ₗ[ℂ] Fragment (Fin t) → ℂ

The curried connection pairing as a linear map from the free module on t-fragments to the function space.

Equations

• RS.connectionMap f t = (Finsupp.lift (RS.Fragment (Fin t) → ℂ) ℂ (RS.Fragment (Fin t))) fun (F G : RS.Fragment (Fin t)) => RS.connectionPairing f t F G

def RS.EdgeRankBounded (f : ClosedFragment → ℂ) (R : ℕ) : Prop

The edge-rank hypothesis H2: the connection pairing at every arity has rank at most R ^ t.

Equations

• RS.EdgeRankBounded f R = ∀ (t : ℕ), Module.rank ℂ ↥(RS.connectionMap f t).range ≤ ↑R ^ t

noncomputable def RS.emptyClosedFragment : ClosedFragment

The empty closed fragment.

Equations

• RS.emptyClosedFragment = (RS.Fragment.circlesOnly 0).relabel (Equiv.equivOfIsEmpty Empty (Fin 0))

structure RS.EdgeRankParameter (R : ℕ) : Type 1

The hypothesis class of the main theorem: a parameter on closed fragments, normalized on the empty graph, with exponentially bounded connection rank.

• val : ClosedFragment → ℂ

  The parameter, on concrete closed fragments.

• val_empty : self.val emptyClosedFragment = 1

  The parameter takes the value 1 on the empty graph.

• iso_invariant (W₁ W₂ : ClosedFragment) : ∀ (a : Fragment.Equiv W₁ W₂), self.val W₁ = self.val W₂

  The parameter is invariant under fragment isomorphism.

• rank_bounded : EdgeRankBounded self.val R

  The rank bound.

6. Eulerian edge subsets and circuit data

Definition 5 sums over pairing-closed flag subsets in which every vertex has even degree. A transition system is the local pairing κ of Definition 5: a second fixed-point-free involution matching participating flags at common vertices. Following an edge and then the matching generates the circuit walks; each geometric circuit of n edges appears as two walk-cycles (its two directions) when n ≥ 2 and as two walk fixed points when n = 1, so the circuit count is half the number of orbits.

structure RS.EdgeSubset {α : Type} (W : Fragment α) : Type

An edge subset of a fragment: a flag set closed under the edge pairing.

• flags : Finset W.Flag

  The participating flags.

• pairing_mem (f : W.Flag) : f ∈ self.flags → W.pairing f ∈ self.flags

  The set is closed under the edge pairing.

noncomputable def RS.EdgeSubset.deg {α : Type} {W : Fragment α} (F : EdgeSubset W) (v : W.Vertex) : ℕ

The degree of a vertex within an edge subset: the number of participating flags attached to it.

Equations

• F.deg v = {f ∈ F.flags | W.attach f = Sum.inl v}.card

def RS.EdgeSubset.Eulerian {α : Type} {W : Fragment α} (F : EdgeSubset W) : Prop

An edge subset is Eulerian when every vertex has even degree within it.

Equations

• F.Eulerian = ∀ (v : W.Vertex), Even (F.deg v)

structure RS.EdgeSubset.TransitionSystem {α : Type} {W : Fragment α} (F : EdgeSubset W) : Type

A transition system on an edge subset: a fixed-point-free involution of its flags matching flags at a common internal vertex. This is the local pairing data κ of Definition 5.

• match_ : W.Flag → W.Flag

  The matching.

• match_invol (f : W.Flag) : f ∈ F.flags → self.match_ (self.match_ f) = f

  The matching is an involution on the participating flags.

• match_ne (f : W.Flag) : f ∈ F.flags → self.match_ f ≠ f

  The matching has no fixed points on the participating flags.

• match_mem (f : W.Flag) : f ∈ F.flags → self.match_ f ∈ F.flags

  The matching stays within the participating flags.

• match_vertex (f : W.Flag) : f ∈ F.flags → ∀ (v : W.Vertex), W.attach f = Sum.inl v → W.attach (self.match_ f) = Sum.inl v

  Matched flags share an internal vertex.

• attach_internal (f : W.Flag) : f ∈ F.flags → ∃ (v : W.Vertex), W.attach f = Sum.inl v

  Only internally attached flags participate.

def RS.EdgeSubset.TransitionSystem.walk {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (f : W.Flag) : W.Flag

The walk map of a transition system: follow the edge to the partner flag, then the matching at its vertex.

Equations

• κ.walk f = κ.match_ (W.pairing f)

theorem RS.EdgeSubset.TransitionSystem.walk_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : κ.walk f ∈ F.flags

The walk map preserves the participating flags.

theorem RS.EdgeSubset.TransitionSystem.walk_injOn {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f g : W.Flag} (hf : f ∈ F.flags) (hg : g ∈ F.flags) (h : κ.walk f = κ.walk g) : f = g

The walk map is injective on the participating flags.

noncomputable def RS.EdgeSubset.TransitionSystem.walkPerm {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : Equiv.Perm ↥F.flags

The walk permutation of a transition system: the walk map as a permutation of the participating flags.

Equations

• κ.walkPerm = Equiv.ofBijective (fun (f : ↥F.flags) => ⟨κ.walk ↑f, ⋯⟩) ⋯

noncomputable def RS.EdgeSubset.TransitionSystem.circuitCount {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : ℕ

The circuit count of a transition system: each geometric circuit of n edges carries two walk-cycles of length n when n ≥ 2 and two walk fixed points when n = 1, so the count is half the total number of orbits.

Equations

• κ.circuitCount = (κ.walkPerm.cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑κ.walkPerm)) / 2

7. The mixed partition function (Definition 5)

A (k, 2ℓ) mixed vertex functional assigns a value to a multiset of even colours and a set of odd colours; the alternating evaluation on an ordered odd list is recovered through the sorting sign, so antisymmetry is a theorem of the evaluator rather than a condition on the data. The summand of an Eulerian subset is its circuit sign times the colouring sum of vertex values, odd colours contributing through the symplectic pairing (oddPartner, oddPartnerSign); the value of the subset is choice-free because the tree proves it independent of the transition data, and mixedPartition is the free-circle factor (k − 2ℓ)^circles times the sum over Eulerian subsets.

def RS.MixedFunctional (k ℓ : ℕ) : Type

The data of a (k, 2ℓ) mixed vertex functional: a value for each multiset of even colours and set of odd colours.

Equations

• RS.MixedFunctional k ℓ = (Multiset (Fin k) → Finset (Fin (2 * ℓ)) → ℂ)

def RS.MixedFunctional.evalOdd {k ℓ : ℕ} (h : MixedFunctional k ℓ) (μ : Multiset (Fin k)) (w : List (Fin (2 * ℓ))) : ℂ

The alternating evaluation of a mixed functional on an ordered list of odd colours: zero on repetitions, otherwise the sorting sign times the value on the underlying set.

Equations

• h.evalOdd μ w = if w.Nodup then ↑(RS.sortSign w) * h μ w.toFinset else 0

def RS.oddPartner (ℓ : ℕ) (c : Fin (2 * ℓ)) : Fin (2 * ℓ)

The odd-colour index pairing of the standard symplectic basis: the partner of colour c is c + ℓ when c < ℓ and c − ℓ otherwise.

Equations

• RS.oddPartner ℓ c = if h : ↑c < ℓ then ⟨↑c + ℓ, ⋯⟩ else ⟨↑c - ℓ, ⋯⟩

def RS.oddPartnerSign (ℓ : ℕ) (c : Fin (2 * ℓ)) : ℤ

The sign of the odd-colour pairing: g_c = −f_{c+ℓ} for c < ℓ and g_c = f_{c−ℓ} otherwise.

Equations

• RS.oddPartnerSign ℓ c = if ↑c < ℓ then -1 else 1

structure RS.EdgeSubset.TransitionSystem.Orientation {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : Type

An orientation compatible with a transition system: an in/out designation of the participating flags, flipped both by the vertex matching and by the edge pairing (so circuits are traversed consistently).

• isOut : W.Flag → Bool

  Whether a flag is an outgoing end.

• match_flip (f : W.Flag) : f ∈ F.flags → self.isOut (κ.match_ f) = !self.isOut f

  The vertex matching pairs incoming with outgoing flags.

• pairing_flip (f : W.Flag) : f ∈ F.flags → self.isOut (W.pairing f) = !self.isOut f

  Each edge has one outgoing and one incoming end.

@[instance_reducible]

noncomputable def RS.Fragment.flagOrder {α : Type} (W : Fragment α) : LinearOrder W.Flag

An arbitrary but fixed linear order on the flags of a fragment, transported from an enumeration. Used only to enumerate vertex pairings; the evaluated summands are independent of the choice because pair blocks move by even permutations.

Equations

• W.flagOrder = LinearOrder.lift' ⇑(Fintype.equivFin W.Flag) ⋯

noncomputable def RS.EdgeSubset.inFlagsAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (v : W.Vertex) : List W.Flag

The incoming participating flags at a vertex, in the fixed flag order.

Equations

• F.inFlagsAt o v = {f ∈ F.flags | W.attach f = Sum.inl v ∧ o.isOut f = false}.sort fun (x1 x2 : W.Flag) => x1 ≤ x2

theorem RS.EdgeSubset.pairing_not_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∉ F.flags) : W.pairing f ∉ F.flags

The complement of an edge subset is closed under the pairing.

def RS.EdgeSubset.EvenColouring {α : Type} {W : Fragment α} (F : EdgeSubset W) (k : ℕ) : Type

Even colourings of the non-participating edges: pairing-constant colours on the flags outside the subset.

Equations

• F.EvenColouring k = { ψ : { f : W.Flag // f ∉ F.flags } → Fin k // ∀ (f : { f : W.Flag // f ∉ F.flags }), ψ ⟨W.pairing ↑f, ⋯⟩ = ψ f }

def RS.EdgeSubset.OddColouring {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Type

Odd colourings of the participating edges: pairing-constant colours on the flags of the subset.

Equations

• F.OddColouring ℓ = { φ : ↥F.flags → Fin (2 * ℓ) // ∀ (f : ↥F.flags), φ ⟨W.pairing ↑f, ⋯⟩ = φ f }

@[instance_reducible]

noncomputable instance RS.EdgeSubset.EvenColouring.instFintype {α : Type} {W : Fragment α} (F : EdgeSubset W) (k : ℕ) : Fintype (F.EvenColouring k)

Even colourings are finite in number.

Equations

• RS.EdgeSubset.EvenColouring.instFintype F k = id inferInstance

@[instance_reducible]

noncomputable instance RS.EdgeSubset.OddColouring.instFintype {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Fintype (F.OddColouring ℓ)

And so are odd ones, so Definition 5's sum is finite.

Equations

• RS.EdgeSubset.OddColouring.instFintype F ℓ = id inferInstance

noncomputable def RS.EdgeSubset.evenColoursAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {k : ℕ} (ψ : F.EvenColouring k) (v : W.Vertex) : Multiset (Fin k)

The even-colour multiset at a vertex: the colours of the non-participating flags attached to it.

Equations

• F.evenColoursAt ψ v = Multiset.map ↑ψ {f : { f : W.Flag // f ∉ F.flags } | W.attach ↑f = Sum.inl v}.val

theorem RS.EdgeSubset.mem_of_mem_inFlagsAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} {o : κ.Orientation} {v : W.Vertex} {f : W.Flag} (hf : f ∈ F.inFlagsAt o v) : f ∈ F.flags

Every in-flag at a vertex participates in the edge subset.

noncomputable def RS.EdgeSubset.oddPairFn {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.TransitionSystem) (φ : F.OddColouring ℓ) (f : ↥F.flags) : List (Fin (2 * ℓ))

The odd pair contributed by an incoming participating flag: its edge colour followed by the partner index of its matched outgoing flag's edge colour.

Equations

• F.oddPairFn κ φ f = [↑φ f, RS.oddPartner ℓ (↑φ ⟨κ.match_ ↑f, ⋯⟩)]

noncomputable def RS.EdgeSubset.oddSignFn {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.TransitionSystem) (φ : F.OddColouring ℓ) (f : ↥F.flags) : ℤ

The odd-pairing sign contributed by an incoming participating flag: the partner sign of its matched outgoing flag's colour.

Equations

• F.oddSignFn κ φ f = RS.oddPartnerSign ℓ (↑φ ⟨κ.match_ ↑f, ⋯⟩)

noncomputable def RS.EdgeSubset.oddListAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : List (Fin (2 * ℓ))

The odd-colour list at a vertex: the odd pairs of the incoming flags in the fixed order.

Equations

• F.oddListAt o φ v = List.flatMap (F.oddPairFn κ φ) ((F.inFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.flags) ⋯)

noncomputable def RS.EdgeSubset.oddSignAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : ℤ

The odd-pairing sign at a vertex: the product of the partner signs of the outgoing colours.

Equations

• F.oddSignAt o φ v = (List.map (F.oddSignFn κ φ) ((F.inFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.flags) ⋯)).prod

noncomputable def RS.EdgeSubset.mixedSummand {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) {κ : F.TransitionSystem} (o : κ.Orientation) : ℂ

The Definition 5 summand of an Eulerian edge subset with chosen transition system and orientation: the circuit sign times the colouring sum of the vertex values.

Equations

• F.mixedSummand h o = (-1) ^ κ.circuitCount * ∑ ψ : F.EvenColouring k, ∑ φ : F.OddColouring ℓ, ∏ v : W.Vertex, ↑(F.oddSignAt o φ v) * h.evalOdd (F.evenColoursAt ψ v) (F.oddListAt o φ v)

noncomputable def RS.EdgeSubset.mixedValue {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) : ℂ

The Definition 5 value of an edge subset: the summand for a choice of transition system and orientation, zero when none exists. (Every Eulerian subset admits one; the value is independent of the choice by the Eulerian-independence input.)

Equations

• F.mixedValue h = if hne : Nonempty ((κ : F.TransitionSystem) × κ.Orientation) then F.mixedSummand h (Classical.choice hne).snd else 0

noncomputable def RS.mixedPartition {α : Type} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : Fragment α) : ℂ

The mixed partition function (Regts–Sevenster Definition 5) of a fragment: the free-circle factor times the sum over Eulerian edge subsets of their circuit-signed colouring sums.

Equations

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

def RS.IsMixedPartitionFunction (f : ClosedFragment → ℂ) : Prop

A parameter on closed fragments is a mixed partition function when it is the Definition 5 value of some mixed functional.

Equations

• RS.IsMixedPartitionFunction f = ∃ (k : ℕ) (ℓ : ℕ) (h : RS.MixedFunctional k ℓ), ∀ (W : RS.ClosedFragment), f W = RS.mixedPartition h W

8. The named statements

The forward direction, the separate parity bound ⌊2eR⌋, the sharp total colour bound R, and the converse with its explicit base.

def RS.RegtsSevensterStatement : Prop

THE REGTS–SEVENSTER CONJECTURE. Every graph parameter with exponentially bounded edge-connection rank is a mixed partition function.

Equations

• RS.RegtsSevensterStatement = ∀ (R : ℕ) (f : RS.EdgeRankParameter R), RS.IsMixedPartitionFunction f.val

def RS.IsMixedPartitionFunctionBounded (f : ClosedFragment → ℂ) (B : ℕ) : Prop

A mixed partition function with explicit dimension bounds: the functional's even dimension k and odd dimension 2ℓ are both at most B.

Equations

• RS.IsMixedPartitionFunctionBounded f B = ∃ (k : ℕ) (ℓ : ℕ) (h : RS.MixedFunctional k ℓ), k ≤ B ∧ 2 * ℓ ≤ B ∧ ∀ (W : RS.ClosedFragment), f W = RS.mixedPartition h W

def RS.RegtsSevensterStatementQuant : Prop

THE QUANTITATIVE REGTS–SEVENSTER STATEMENT: every graph parameter with edge-connection rank at most R ^ t is a mixed partition function of a (k, 2ℓ)-functional with k, 2ℓ ≤ ⌊2eR⌋.

Equations

• RS.RegtsSevensterStatementQuant = ∀ (R : ℕ) (f : RS.EdgeRankParameter R), RS.IsMixedPartitionFunctionBounded f.val ⌊2 * Real.exp 1 * ↑R⌋₊

structure RS.TotalBoundedMixedModel (f : ClosedFragment → ℂ) (B : ℕ) : Type

A mixed model with a bound on the sum of its even and odd dimensions. The named fields retain the functional and its agreement with the graph parameter as part of the witness.

• k : ℕ

  The number of even colours.

• ℓ : ℕ

  Half the number of odd colours.

• functional : MixedFunctional self.k self.ℓ

  The vertex functional of the model.

• dimension_le : self.k + 2 * self.ℓ ≤ B

  The total number of colours is bounded by B.

• partition_eq (W : ClosedFragment) : f W = mixedPartition self.functional W

  The model evaluates to the given parameter on every fragment.

def RS.IsMixedPartitionFunctionTotalBounded (f : ClosedFragment → ℂ) (B : ℕ) : Prop

A parameter admits a mixed model with at most B colours in total, counting both the even and odd components.

Equations

• RS.IsMixedPartitionFunctionTotalBounded f B = Nonempty (RS.TotalBoundedMixedModel f B)

def RS.RegtsSevensterStatementTotal : Prop

The total-dimension Regts–Sevenster statement: an edge-rank base R bounds the total number of colours of a representing mixed model.

Equations

• RS.RegtsSevensterStatementTotal = ∀ (R : ℕ) (f : RS.EdgeRankParameter R), RS.IsMixedPartitionFunctionTotalBounded f.val R

def RS.RegtsSevensterConverseStatement : Prop

THE CONVERSE STATEMENT: every mixed partition function is an edge-rank-bounded parameter with base max 1 (k + 2ℓ) (Regts–Sevenster, arXiv:1807.04494, Theorem 6).

Equations

• RS.RegtsSevensterConverseStatement = ∀ (k ℓ : ℕ) (h : RS.MixedFunctional k ℓ), ∃ (g : RS.EdgeRankParameter (max 1 (k + 2 * ℓ))), ∀ (W : RS.ClosedFragment), g.val W = RS.mixedPartition h W

9. The symmetric monoidal category of super vector spaces

The codomain of the fibre functor in Deligne's conclusion: finite-dimensional ℤ/2-graded complex vector spaces with grading-preserving maps, the graded tensor product, and the braiding that carries the Koszul sign — the odd⊗odd block acquires a factor of −1 under the swap (koszulEvenAux, second component). This is the longest section; its content is one structure, its category structure, and the monoidal, braided, symmetric, additive and ℂ-linear instances, together with the computation lemmas their coherence proofs run on. An auditor checking what Deligne's theorem says should read the objects, tensorObj, tensorUnit and the two Koszul blocks; the rest is coherence.

structure RS.SuperVect : Type 1

A super vector space over ℂ: a pair of finite-dimensional complex vector spaces, called the even and odd components.

• even : Type

  The even-graded component.

• odd : Type

  The odd-graded component.

• evenAddCommGroup : AddCommGroup self.even
• evenModule : Module ℂ self.even
• oddAddCommGroup : AddCommGroup self.odd
• oddModule : Module ℂ self.odd
• evenFinite : FiniteDimensional ℂ self.even
• oddFinite : FiniteDimensional ℂ self.odd

structure RS.SuperVect.Hom (V W : SuperVect) : Type

A morphism of super vector spaces: a pair of ℂ-linear maps preserving the grading.

• evenMap : V.even →ₗ[ℂ] W.even

  The even component of the morphism.

• oddMap : V.odd →ₗ[ℂ] W.odd

  The odd component of the morphism.

theorem RS.SuperVect.Hom.ext {V W : SuperVect} {x y : V.Hom W} (evenMap : x.evenMap = y.evenMap) (oddMap : x.oddMap = y.oddMap) : x = y

theorem RS.SuperVect.Hom.ext_iff {V W : SuperVect} {x y : V.Hom W} : x = y ↔ x.evenMap = y.evenMap ∧ x.oddMap = y.oddMap

def RS.SuperVect.Hom.id (V : SuperVect) : V.Hom V

The identity morphism on a super vector space.

Equations

• RS.SuperVect.Hom.id V = { evenMap := LinearMap.id, oddMap := LinearMap.id }

def RS.SuperVect.Hom.comp {V W X : SuperVect} (g : W.Hom X) (f : V.Hom W) : V.Hom X

Composition of super-vector-space morphisms.

Equations

• g.comp f = { evenMap := g.evenMap ∘ₗ f.evenMap, oddMap := g.oddMap ∘ₗ f.oddMap }

@[instance_reducible]

instance RS.SuperVect.instCategoryStruct : CategoryTheory.CategoryStruct.{0, 1} SuperVect

Super vector spaces and grading-preserving maps form a category.

Equations

• RS.SuperVect.instCategoryStruct = { Hom := RS.SuperVect.Hom, id := RS.SuperVect.Hom.id, comp := fun {X Y Z : RS.SuperVect} (f : X.Hom Y) (g : Y.Hom Z) => g.comp f }

theorem RS.SuperVect.hom_ext {V W : SuperVect} {f g : V ⟶ W} (he : f.evenMap = g.evenMap) (ho : f.oddMap = g.oddMap) : f = g

Two morphisms agreeing in both components are equal.

theorem RS.SuperVect.hom_ext_iff {V W : SuperVect} {f g : V ⟶ W} : f = g ↔ f.evenMap = g.evenMap ∧ f.oddMap = g.oddMap

@[instance_reducible]

instance RS.SuperVect.instCategory : CategoryTheory.Category.{0, 1} SuperVect

SuperVect forms a category with grading-preserving linear maps.

Equations

• RS.SuperVect.instCategory = { toCategoryStruct := RS.SuperVect.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

Tensor product

def RS.SuperVect.tensorObj (V W : SuperVect) : SuperVect

The graded tensor product of two super vector spaces. The even component is (V.even ⊗ W.even) × (V.odd ⊗ W.odd) and the odd component is (V.even ⊗ W.odd) × (V.odd ⊗ W.even).

Equations

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

def RS.SuperVect.tensorHom {V₁ V₂ W₁ W₂ : SuperVect} (f : V₁.Hom V₂) (g : W₁.Hom W₂) : (V₁.tensorObj W₁).Hom (V₂.tensorObj W₂)

The tensor product of two grading-preserving maps acts component-wise on each tensor block.

Equations

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

@[reducible]

def RS.SuperVect.tensorUnit : SuperVect

The monoidal unit: ℂ in even degree, the zero module in odd degree. Marked reducible so that tensorUnit.odd reduces to PUnit during type-class synthesis.

Equations

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

The Koszul braiding

def RS.SuperVect.koszulEvenAux (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] : TensorProduct ℂ A B × TensorProduct ℂ C D →ₗ[ℂ] TensorProduct ℂ B A × TensorProduct ℂ D C

Module-level even Koszul block: TensorProduct.comm on the first factor and minus TensorProduct.comm on the second. Stated over bare modules so that instances of it at compound objects have syntactically reduced types.

Equations

• RS.SuperVect.koszulEvenAux A B C D = (↑(TensorProduct.comm ℂ A B)).prodMap (-↑(TensorProduct.comm ℂ C D))

def RS.SuperVect.koszulOddAux (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] : TensorProduct ℂ A B × TensorProduct ℂ C D →ₗ[ℂ] TensorProduct ℂ D C × TensorProduct ℂ B A

Module-level odd Koszul block: swaps the two summands and applies TensorProduct.comm on each (no sign).

Equations

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

def RS.SuperVect.koszulBraidingEven (V W : SuperVect) : TensorProduct ℂ V.even W.even × TensorProduct ℂ V.odd W.odd →ₗ[ℂ] TensorProduct ℂ W.even V.even × TensorProduct ℂ W.odd V.odd

The even component of the Koszul braiding: applies TensorProduct.comm on the even⊗even block and minus TensorProduct.comm on the odd⊗odd block.

Equations

• V.koszulBraidingEven W = RS.SuperVect.koszulEvenAux V.even W.even V.odd W.odd

def RS.SuperVect.koszulBraidingOdd (V W : SuperVect) : TensorProduct ℂ V.even W.odd × TensorProduct ℂ V.odd W.even →ₗ[ℂ] TensorProduct ℂ W.even V.odd × TensorProduct ℂ W.odd V.even

The odd component of the Koszul braiding: swaps the two blocks and applies TensorProduct.comm on each (no sign, since even⊗odd and odd⊗even contribute (−1)^(0·1) = 1).

Equations

• V.koszulBraidingOdd W = RS.SuperVect.koszulOddAux V.even W.odd V.odd W.even

def RS.SuperVect.koszulBraiding (V W : SuperVect) : (V.tensorObj W).Hom (W.tensorObj V)

The Koszul braiding morphism V ⊗ W → W ⊗ V in SuperVect, carrying the sign (−1)^(p·q) on the swap of homogeneous elements of parity p and q.

Equations

• V.koszulBraiding W = { evenMap := id (V.koszulBraidingEven W), oddMap := id (V.koszulBraidingOdd W) }

theorem RS.SuperVect.koszulBraiding_self_inverse (V W : SuperVect) : (W.koszulBraiding V).comp (V.koszulBraiding W) = Hom.id (V.tensorObj W)

The Koszul braiding is a self-inverse: the two applications of the sign on the odd⊗odd block cancel, and the component swaps on the odd part compose to the identity.

@[simp]

theorem RS.SuperVect.koszulBraidingOdd_pair (V W : SuperVect) (x : TensorProduct ℂ V.even W.odd) (y : TensorProduct ℂ V.odd W.even) : (V.koszulBraidingOdd W) (x, y) = ((TensorProduct.comm ℂ V.odd W.even) y, (TensorProduct.comm ℂ V.even W.odd) x)

Application of the Koszul odd braiding to a pair of elements.

Koszul braiding as a categorical isomorphism

def RS.SuperVect.koszulBraidingIso (V W : SuperVect) : V.tensorObj W ≅ W.tensorObj V

The Koszul braiding as an isomorphism in SuperVect.

Equations

• V.koszulBraidingIso W = { hom := V.koszulBraiding W, inv := W.koszulBraiding V, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Left and right unitors

def RS.SuperVect.leftUnitor (V : SuperVect) : tensorUnit.tensorObj V ≅ V

The left unitor isomorphism 𝟙_ ⊗ V ≅ V.

Equations

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

def RS.SuperVect.rightUnitor (V : SuperVect) : V.tensorObj tensorUnit ≅ V

The right unitor isomorphism V ⊗ 𝟙_ ≅ V.

Equations

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

Associator

def RS.SuperVect.prod4Perm (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] : ((A × B) × C × D) ≃ₗ[ℂ] (A × C) × D × B

Permutation of product components used in the associator: ((A × B) × (C × D)) ≃ₗ ((A × C) × (D × B)). The mapping is (a, b, c, d) ↦ (a, c, d, b). All field proofs hold by rfl because the permutation is a definitional reshuffling of product components.

Equations

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

def RS.SuperVect.assocAux (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] : (TensorProduct ℂ (TensorProduct ℂ A₁ B₁ × TensorProduct ℂ A₂ B₂) C₁ × TensorProduct ℂ (TensorProduct ℂ A₁ B₂ × TensorProduct ℂ A₂ B₁) C₂) ≃ₗ[ℂ] TensorProduct ℂ A₁ (TensorProduct ℂ B₁ C₁ × TensorProduct ℂ B₂ C₂) × TensorProduct ℂ A₂ (TensorProduct ℂ B₁ C₂ × TensorProduct ℂ B₂ C₁)

Module-level associator block. The construction distributes the tensor over products (via prodLeft and prodRight), reassociates each tensor block (via TensorProduct.assoc), and permutes the four summands via prod4Perm. Stated over bare modules so that instances of it at compound objects have syntactically reduced types; the even and odd components of the SuperVect associator are its instantiations with the two C-slots in the two orders.

Equations

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

def RS.SuperVect.assocEvenEquiv (V W X : SuperVect) : (TensorProduct ℂ (TensorProduct ℂ V.even W.even × TensorProduct ℂ V.odd W.odd) X.even × TensorProduct ℂ (TensorProduct ℂ V.even W.odd × TensorProduct ℂ V.odd W.even) X.odd) ≃ₗ[ℂ] TensorProduct ℂ V.even (TensorProduct ℂ W.even X.even × TensorProduct ℂ W.odd X.odd) × TensorProduct ℂ V.odd (TensorProduct ℂ W.even X.odd × TensorProduct ℂ W.odd X.even)

The even component of the associator equivalence.

Equations

• V.assocEvenEquiv W X = RS.SuperVect.assocAux V.even V.odd W.even W.odd X.even X.odd

def RS.SuperVect.assocOddEquiv (V W X : SuperVect) : (TensorProduct ℂ (TensorProduct ℂ V.even W.even × TensorProduct ℂ V.odd W.odd) X.odd × TensorProduct ℂ (TensorProduct ℂ V.even W.odd × TensorProduct ℂ V.odd W.even) X.even) ≃ₗ[ℂ] TensorProduct ℂ V.even (TensorProduct ℂ W.even X.odd × TensorProduct ℂ W.odd X.even) × TensorProduct ℂ V.odd (TensorProduct ℂ W.even X.even × TensorProduct ℂ W.odd X.odd)

The odd component of the associator equivalence: assocAux with the roles of the two X-slots swapped.

Equations

• V.assocOddEquiv W X = RS.SuperVect.assocAux V.even V.odd W.even W.odd X.odd X.even

def RS.SuperVect.associator (V W X : SuperVect) : (V.tensorObj W).tensorObj X ≅ V.tensorObj (W.tensorObj X)

The associator isomorphism (V ⊗ W) ⊗ X ≅ V ⊗ (W ⊗ X) in SuperVect. Distributes tensor over products, reassociates each block, and permutes the summands back into the canonical grading order.

Equations

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

Associator computation lemmas

@[simp]

theorem RS.SuperVect.prod_fst_zero {A : Type u_1} {B : Type u_2} [Zero A] [Zero B] : 0.1 = 0

The first component of the zero pair.

@[simp]

theorem RS.SuperVect.prod_snd_zero {A : Type u_1} {B : Type u_2} [Zero A] [Zero B] : 0.2 = 0

The second component of the zero pair.

@[simp]

theorem RS.SuperVect.prod_mk_zero {A : Type u_1} {B : Type u_2} [Zero A] [Zero B] : (0, 0) = 0

The pair of zeros is the zero pair.

@[simp]

theorem RS.SuperVect.prod4Perm_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (x : (A × B) × C × D) : (prod4Perm A B C D) x = ((x.1.1, x.2.1), x.2.2, x.1.2)

prod4Perm, applied.

theorem RS.SuperVect.prodRight_symm_tmul_fst {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} [AddCommGroup M₁] [Module ℂ M₁] [AddCommGroup M₂] [Module ℂ M₂] [AddCommGroup M₃] [Module ℂ M₃] (m₁ : M₁) (m₂ : M₂) : (TensorProduct.prodRight ℂ ℂ M₁ M₂ M₃).symm (m₁ ⊗ₜ[ℂ] m₂, 0) = m₁ ⊗ₜ[ℂ] (m₂, 0)

The inverse product-distribution on a first-summand pure tensor.

theorem RS.SuperVect.prodRight_symm_tmul_snd {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} [AddCommGroup M₁] [Module ℂ M₁] [AddCommGroup M₂] [Module ℂ M₂] [AddCommGroup M₃] [Module ℂ M₃] (m₁ : M₁) (m₃ : M₃) : (TensorProduct.prodRight ℂ ℂ M₁ M₂ M₃).symm (0, m₁ ⊗ₜ[ℂ] m₃) = m₁ ⊗ₜ[ℂ] (0, m₃)

The inverse product-distribution on a second-summand pure tensor.

@[simp]

theorem RS.SuperVect.assocAux_ee {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (a : A₁) (b : B₁) (c : C₁) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂) ((a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c, 0) = (a ⊗ₜ[ℂ] (b ⊗ₜ[ℂ] c, 0), 0)

The associator block on a pure tensor of the A₁ ⊗ B₁ summand with C₁.

@[simp]

theorem RS.SuperVect.assocAux_oo {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (p : A₂) (q : B₂) (c : C₁) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂) ((0, p ⊗ₜ[ℂ] q) ⊗ₜ[ℂ] c, 0) = (0, p ⊗ₜ[ℂ] (0, q ⊗ₜ[ℂ] c))

The associator block on a pure tensor of the A₂ ⊗ B₂ summand with C₁.

@[simp]

theorem RS.SuperVect.assocAux_eo {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (a : A₁) (b : B₂) (c : C₂) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂) (0, (a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c) = (a ⊗ₜ[ℂ] (0, b ⊗ₜ[ℂ] c), 0)

The associator block on a pure tensor of the A₁ ⊗ B₂ summand with C₂.

@[simp]

theorem RS.SuperVect.assocAux_oe {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (p : A₂) (q : B₁) (c : C₂) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂) (0, (0, p ⊗ₜ[ℂ] q) ⊗ₜ[ℂ] c) = (0, p ⊗ₜ[ℂ] (q ⊗ₜ[ℂ] c, 0))

The associator block on a pure tensor of the A₂ ⊗ B₁ summand with C₂.

@[simp]

theorem RS.SuperVect.assocAux_symm_ee {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (a : A₁) (b : B₁) (c : C₁) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂).symm (a ⊗ₜ[ℂ] (b ⊗ₜ[ℂ] c, 0), 0) = ((a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c, 0)

The inverse associator block on a pure tensor of A₁ with the B₁ ⊗ C₁ summand.

@[simp]

theorem RS.SuperVect.assocAux_symm_oo {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (p : A₂) (q : B₂) (c : C₁) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂).symm (0, p ⊗ₜ[ℂ] (0, q ⊗ₜ[ℂ] c)) = ((0, p ⊗ₜ[ℂ] q) ⊗ₜ[ℂ] c, 0)

The inverse associator block on a pure tensor of A₂ with the B₂ ⊗ C₁ summand.

@[simp]

theorem RS.SuperVect.assocAux_symm_eo {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (a : A₁) (b : B₂) (c : C₂) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂).symm (a ⊗ₜ[ℂ] (0, b ⊗ₜ[ℂ] c), 0) = (0, (a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c)

The inverse associator block on a pure tensor of A₁ with the B₂ ⊗ C₂ summand.

@[simp]

theorem RS.SuperVect.assocAux_symm_oe {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (p : A₂) (q : B₁) (c : C₂) : (assocAux A₁ A₂ B₁ B₂ C₁ C₂).symm (0, p ⊗ₜ[ℂ] (q ⊗ₜ[ℂ] c, 0)) = (0, (0, p ⊗ₜ[ℂ] q) ⊗ₜ[ℂ] c)

The inverse associator block on a pure tensor of A₂ with the B₁ ⊗ C₂ summand.

@[simp]

theorem RS.SuperVect.koszulEvenAux_fst {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (a : A) (b : B) : (koszulEvenAux A B C D) (a ⊗ₜ[ℂ] b, 0) = (b ⊗ₜ[ℂ] a, 0)

The even Koszul block on the first summand: plain commutation, no sign.

@[simp]

theorem RS.SuperVect.koszulEvenAux_snd {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (c : C) (d : D) : (koszulEvenAux A B C D) (0, c ⊗ₜ[ℂ] d) = -(0, d ⊗ₜ[ℂ] c)

The Koszul sign: on the second summand — the odd⊗odd block — the even block commutes and negates.

@[simp]

theorem RS.SuperVect.koszulOddAux_fst {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (a : A) (b : B) : (koszulOddAux A B C D) (a ⊗ₜ[ℂ] b, 0) = (0, b ⊗ₜ[ℂ] a)

The odd Koszul block on the first summand: commutation into the other summand, no sign.

@[simp]

theorem RS.SuperVect.koszulOddAux_snd {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (c : C) (d : D) : (koszulOddAux A B C D) (0, c ⊗ₜ[ℂ] d) = (d ⊗ₜ[ℂ] c, 0)

The odd Koszul block on the second summand: likewise unsigned — only the odd⊗odd block carries the sign.

theorem RS.SuperVect.prod_mk_neg_left {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (u : A) : (-u, 0) = -(u, 0)

A left-negated pair is a negated pair.

theorem RS.SuperVect.prod_mk_neg_right {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (v : B) : (0, -v) = -(0, v)

A right-negated pair is a negated pair.

theorem RS.SuperVect.assocAux_triangle (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] : (TensorProduct.map LinearMap.id (↑(TensorProduct.lid ℂ B₁) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ ℂ B₁) (TensorProduct ℂ PUnit.{u_5 + 1} B₂))).prodMap (TensorProduct.map LinearMap.id (↑(TensorProduct.lid ℂ B₂) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ ℂ B₂) (TensorProduct ℂ PUnit.{u_5 + 1} B₁))) ∘ₗ ↑(assocAux A₁ A₂ ℂ PUnit.{u_5 + 1} B₁ B₂) = (TensorProduct.map (↑(TensorProduct.rid ℂ A₁) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ A₁ ℂ) (TensorProduct ℂ A₂ PUnit.{u_5 + 1})) LinearMap.id).prodMap (TensorProduct.map (↑(TensorProduct.rid ℂ A₂) ∘ₗ LinearMap.snd ℂ (TensorProduct ℂ A₁ PUnit.{u_5 + 1}) (TensorProduct ℂ A₂ ℂ)) LinearMap.id)

The triangle coherence of the module-level associator block against the unit slots ℂ (even) and PUnit (odd). Both graded components of the SuperVect triangle are instantiations.

theorem RS.SuperVect.koszulAux_hexagon_fwd_even (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] : (↑(assocAux B₁ B₂ C₁ C₂ A₁ A₂) ∘ₗ koszulEvenAux A₁ (TensorProduct ℂ B₁ C₁ × TensorProduct ℂ B₂ C₂) A₂ (TensorProduct ℂ B₁ C₂ × TensorProduct ℂ B₂ C₁)) ∘ₗ ↑(assocAux A₁ A₂ B₁ B₂ C₁ C₂) = ((TensorProduct.map LinearMap.id (koszulEvenAux A₁ C₁ A₂ C₂)).prodMap (TensorProduct.map LinearMap.id (koszulOddAux A₁ C₂ A₂ C₁)) ∘ₗ ↑(assocAux B₁ B₂ A₁ A₂ C₁ C₂)) ∘ₗ (TensorProduct.map (koszulEvenAux A₁ B₁ A₂ B₂) LinearMap.id).prodMap (TensorProduct.map (koszulOddAux A₁ B₂ A₂ B₁) LinearMap.id)

The forward hexagon for the even graded component, at the module level: braiding past a tensor product in two steps agrees with braiding past its factors.

theorem RS.SuperVect.koszulAux_hexagon_fwd_odd (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] : (↑(assocAux B₁ B₂ C₁ C₂ A₂ A₁) ∘ₗ koszulOddAux A₁ (TensorProduct ℂ B₁ C₂ × TensorProduct ℂ B₂ C₁) A₂ (TensorProduct ℂ B₁ C₁ × TensorProduct ℂ B₂ C₂)) ∘ₗ ↑(assocAux A₁ A₂ B₁ B₂ C₂ C₁) = ((TensorProduct.map LinearMap.id (koszulOddAux A₁ C₂ A₂ C₁)).prodMap (TensorProduct.map LinearMap.id (koszulEvenAux A₁ C₁ A₂ C₂)) ∘ₗ ↑(assocAux B₁ B₂ A₁ A₂ C₂ C₁)) ∘ₗ (TensorProduct.map (koszulEvenAux A₁ B₁ A₂ B₂) LinearMap.id).prodMap (TensorProduct.map (koszulOddAux A₁ B₂ A₂ B₁) LinearMap.id)

The forward hexagon for the odd graded component.

theorem RS.SuperVect.koszulAux_hexagon_rev_even (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] : (↑(assocAux C₁ C₂ A₁ A₂ B₁ B₂).symm ∘ₗ koszulEvenAux (TensorProduct ℂ A₁ B₁ × TensorProduct ℂ A₂ B₂) C₁ (TensorProduct ℂ A₁ B₂ × TensorProduct ℂ A₂ B₁) C₂) ∘ₗ ↑(assocAux A₁ A₂ B₁ B₂ C₁ C₂).symm = ((TensorProduct.map (koszulEvenAux A₁ C₁ A₂ C₂) LinearMap.id).prodMap (TensorProduct.map (koszulOddAux A₁ C₂ A₂ C₁) LinearMap.id) ∘ₗ ↑(assocAux A₁ A₂ C₁ C₂ B₁ B₂).symm) ∘ₗ (TensorProduct.map LinearMap.id (koszulEvenAux B₁ C₁ B₂ C₂)).prodMap (TensorProduct.map LinearMap.id (koszulOddAux B₁ C₂ B₂ C₁))

The reverse hexagon for the even graded component, phrased through the inverse associator blocks.

theorem RS.SuperVect.koszulAux_hexagon_rev_odd (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] : (↑(assocAux C₁ C₂ A₁ A₂ B₂ B₁).symm ∘ₗ koszulOddAux (TensorProduct ℂ A₁ B₁ × TensorProduct ℂ A₂ B₂) C₂ (TensorProduct ℂ A₁ B₂ × TensorProduct ℂ A₂ B₁) C₁) ∘ₗ ↑(assocAux A₁ A₂ B₁ B₂ C₂ C₁).symm = ((TensorProduct.map (koszulEvenAux A₁ C₁ A₂ C₂) LinearMap.id).prodMap (TensorProduct.map (koszulOddAux A₁ C₂ A₂ C₁) LinearMap.id) ∘ₗ ↑(assocAux A₁ A₂ C₁ C₂ B₂ B₁).symm) ∘ₗ (TensorProduct.map LinearMap.id (koszulOddAux B₁ C₂ B₂ C₁)).prodMap (TensorProduct.map LinearMap.id (koszulEvenAux B₁ C₁ B₂ C₂))

The reverse hexagon for the odd graded component.

theorem RS.SuperVect.assocAux_pentagon (A₁ : Type u_1) (A₂ : Type u_2) (B₁ : Type u_3) (B₂ : Type u_4) (C₁ : Type u_5) (C₂ : Type u_6) (D₁ : Type u_7) (D₂ : Type u_8) [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] [AddCommGroup D₁] [Module ℂ D₁] [AddCommGroup D₂] [Module ℂ D₂] : ((TensorProduct.map LinearMap.id ↑(assocAux B₁ B₂ C₁ C₂ D₁ D₂)).prodMap (TensorProduct.map LinearMap.id ↑(assocAux B₁ B₂ C₁ C₂ D₂ D₁)) ∘ₗ ↑(assocAux A₁ A₂ (TensorProduct ℂ B₁ C₁ × TensorProduct ℂ B₂ C₂) (TensorProduct ℂ B₁ C₂ × TensorProduct ℂ B₂ C₁) D₁ D₂)) ∘ₗ (TensorProduct.map (↑(assocAux A₁ A₂ B₁ B₂ C₁ C₂)) LinearMap.id).prodMap (TensorProduct.map (↑(assocAux A₁ A₂ B₁ B₂ C₂ C₁)) LinearMap.id) = ↑(assocAux A₁ A₂ B₁ B₂ (TensorProduct ℂ C₁ D₁ × TensorProduct ℂ C₂ D₂) (TensorProduct ℂ C₁ D₂ × TensorProduct ℂ C₂ D₁)) ∘ₗ ↑(assocAux (TensorProduct ℂ A₁ B₁ × TensorProduct ℂ A₂ B₂) (TensorProduct ℂ A₁ B₂ × TensorProduct ℂ A₂ B₁) C₁ C₂ D₁ D₂)

The pentagon coherence of the module-level associator block: both routes from a four-fold graded product to its right-nested form agree. Both graded components of the SuperVect pentagon are instantiations.

Component projection lemmas

@[simp]

theorem RS.SuperVect.cat_comp_evenMap {V W X : SuperVect} (f : V ⟶ W) (g : W ⟶ X) : (CategoryTheory.CategoryStruct.comp f g).evenMap = g.evenMap ∘ₗ f.evenMap

The even component of a categorical composite.

@[simp]

theorem RS.SuperVect.cat_comp_oddMap {V W X : SuperVect} (f : V ⟶ W) (g : W ⟶ X) : (CategoryTheory.CategoryStruct.comp f g).oddMap = g.oddMap ∘ₗ f.oddMap

The odd component of a categorical composite.

@[simp]

theorem RS.SuperVect.cat_id_evenMap (V : SuperVect) : (CategoryTheory.CategoryStruct.id V).evenMap = LinearMap.id

The even component of a categorical identity.

@[simp]

theorem RS.SuperVect.cat_id_oddMap (V : SuperVect) : (CategoryTheory.CategoryStruct.id V).oddMap = LinearMap.id

The odd component of a categorical identity.

@[simp]

theorem RS.SuperVect.tensorHom_evenMap {V₁ V₂ W₁ W₂ : SuperVect} (f : V₁.Hom V₂) (g : W₁.Hom W₂) : (tensorHom f g).evenMap = (TensorProduct.map f.evenMap g.evenMap).prodMap (TensorProduct.map f.oddMap g.oddMap)

The even component of a tensor of morphisms: even⊗even and odd⊗odd in parallel.

@[simp]

theorem RS.SuperVect.tensorHom_oddMap {V₁ V₂ W₁ W₂ : SuperVect} (f : V₁.Hom V₂) (g : W₁.Hom W₂) : (tensorHom f g).oddMap = (TensorProduct.map f.evenMap g.oddMap).prodMap (TensorProduct.map f.oddMap g.evenMap)

The odd component of a tensor of morphisms: even⊗odd and odd⊗even in parallel.

@[simp]

theorem RS.SuperVect.associator_hom_evenMap (V W X : SuperVect) : (V.associator W X).hom.evenMap = ↑(V.assocEvenEquiv W X)

The associator's even component is the even associator equivalence.

@[simp]

theorem RS.SuperVect.associator_hom_oddMap (V W X : SuperVect) : (V.associator W X).hom.oddMap = ↑(V.assocOddEquiv W X)

The associator's odd component is the odd associator equivalence.

@[simp]

theorem RS.SuperVect.associator_inv_evenMap (V W X : SuperVect) : (V.associator W X).inv.evenMap = ↑(V.assocEvenEquiv W X).symm

The inverse associator's even component.

@[simp]

theorem RS.SuperVect.associator_inv_oddMap (V W X : SuperVect) : (V.associator W X).inv.oddMap = ↑(V.assocOddEquiv W X).symm

The inverse associator's odd component.

@[simp]

theorem RS.SuperVect.leftUnitor_hom_evenMap (V : SuperVect) : V.leftUnitor.hom.evenMap = ↑(TensorProduct.lid ℂ V.even) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ ℂ V.even) (TensorProduct ℂ tensorUnit.odd V.odd)

The left unitor's even component: the unit's odd part is zero, so only the first summand survives.

@[simp]

theorem RS.SuperVect.leftUnitor_hom_oddMap (V : SuperVect) : V.leftUnitor.hom.oddMap = ↑(TensorProduct.lid ℂ V.odd) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ ℂ V.odd) (TensorProduct ℂ tensorUnit.odd V.even)

The left unitor's odd component.

@[simp]

theorem RS.SuperVect.rightUnitor_hom_evenMap (V : SuperVect) : V.rightUnitor.hom.evenMap = ↑(TensorProduct.rid ℂ V.even) ∘ₗ LinearMap.fst ℂ (TensorProduct ℂ V.even ℂ) (TensorProduct ℂ V.odd tensorUnit.odd)

The right unitor's even component.

@[simp]

theorem RS.SuperVect.rightUnitor_hom_oddMap (V : SuperVect) : V.rightUnitor.hom.oddMap = ↑(TensorProduct.rid ℂ V.odd) ∘ₗ LinearMap.snd ℂ (TensorProduct ℂ V.even tensorUnit.odd) (TensorProduct ℂ V.odd ℂ)

The right unitor's odd component: here it is the second summand that survives, the unit sitting on the right.

@[simp]

theorem RS.SuperVect.koszulBraiding_evenMap (V W : SuperVect) : (V.koszulBraiding W).evenMap = V.koszulBraidingEven W

The braiding's even component.

@[simp]

theorem RS.SuperVect.koszulBraiding_oddMap (V W : SuperVect) : (V.koszulBraiding W).oddMap = V.koszulBraidingOdd W

The braiding's odd component.

Monoidal structure

@[instance_reducible]

instance RS.SuperVect.instMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct SuperVect

The monoidal category structure on SuperVect: graded tensor product, ℂ unit, standard associator/unitors.

Equations

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

MonoidalCategory axioms

theorem RS.SuperVect.tensorHom_id_id (X₁ X₂ : SuperVect) : tensorHom (Hom.id X₁) (Hom.id X₂) = Hom.id (X₁.tensorObj X₂)

tensorHom id id = id: the tensor of identity morphisms is the identity on the tensor product.

theorem RS.SuperVect.tensorHom_comp (X₁ Y₁ Z₁ X₂ Y₂ Z₂ : SuperVect) (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂) (g₁ : Y₁.Hom Z₁) (g₂ : Y₂.Hom Z₂) : (tensorHom g₁ g₂).comp (tensorHom f₁ f₂) = tensorHom (g₁.comp f₁) (g₂.comp f₂)

Composition distributes over tensor product of morphisms.

@[instance_reducible]

instance RS.SuperVect.instMonoidalCategory : CategoryTheory.MonoidalCategory SuperVect

The full monoidal category structure on SuperVect, constructed via ofTensorHom.

Equations

• RS.SuperVect.instMonoidalCategory = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ RS.SuperVect.instMonoidalCategory._proof_3 @RS.SuperVect.instMonoidalCategory._proof_4 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Braided and symmetric structure

@[instance_reducible]

instance RS.SuperVect.instBraidedCategory : CategoryTheory.BraidedCategory SuperVect

SuperVect is a braided monoidal category with the Koszul braiding: swapping odd ⊗ odd elements picks up a factor of −1.

Equations

• RS.SuperVect.instBraidedCategory = { braiding := RS.SuperVect.koszulBraidingIso, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

@[instance_reducible]

instance RS.SuperVect.instSymmetricCategory : CategoryTheory.SymmetricCategory SuperVect

SuperVect is a symmetric monoidal category: applying the Koszul braiding twice recovers the identity.

Equations

• RS.SuperVect.instSymmetricCategory = { toBraidedCategory := RS.SuperVect.instBraidedCategory, symmetry := ⋯ }

Additive and linear structure

@[instance_reducible]

instance RS.SuperVect.instZeroHom {V W : SuperVect} : Zero (V ⟶ W)

The zero morphism: zero in both components.

Equations

• RS.SuperVect.instZeroHom = { zero := { evenMap := 0, oddMap := 0 } }

@[instance_reducible]

instance RS.SuperVect.instAddHom {V W : SuperVect} : Add (V ⟶ W)

Componentwise addition of morphisms.

Equations

• RS.SuperVect.instAddHom = { add := fun (f g : V ⟶ W) => { evenMap := f.evenMap + g.evenMap, oddMap := f.oddMap + g.oddMap } }

@[instance_reducible]

instance RS.SuperVect.instNegHom {V W : SuperVect} : Neg (V ⟶ W)

Componentwise negation.

Equations

• RS.SuperVect.instNegHom = { neg := fun (f : V ⟶ W) => { evenMap := -f.evenMap, oddMap := -f.oddMap } }

@[instance_reducible]

instance RS.SuperVect.instSubHom {V W : SuperVect} : Sub (V ⟶ W)

Componentwise subtraction.

Equations

• RS.SuperVect.instSubHom = { sub := fun (f g : V ⟶ W) => { evenMap := f.evenMap - g.evenMap, oddMap := f.oddMap - g.oddMap } }

@[instance_reducible]

instance RS.SuperVect.instSMulComplexHom {V W : SuperVect} : SMul ℂ (V ⟶ W)

Componentwise scaling by a complex number.

Equations

• RS.SuperVect.instSMulComplexHom = { smul := fun (c : ℂ) (f : V ⟶ W) => { evenMap := c • f.evenMap, oddMap := c • f.oddMap } }

@[instance_reducible]

instance RS.SuperVect.instSMulNatHom {V W : SuperVect} : SMul ℕ (V ⟶ W)

Componentwise natural scaling, given definitionally so that the AddCommGroup structure below has no transported nsmul field.

Equations

• RS.SuperVect.instSMulNatHom = { smul := fun (n : ℕ) (f : V ⟶ W) => { evenMap := n • f.evenMap, oddMap := n • f.oddMap } }

@[instance_reducible]

instance RS.SuperVect.instSMulIntHom {V W : SuperVect} : SMul ℤ (V ⟶ W)

Componentwise integer scaling, likewise definitional.

Equations

• RS.SuperVect.instSMulIntHom = { smul := fun (n : ℤ) (f : V ⟶ W) => { evenMap := n • f.evenMap, oddMap := n • f.oddMap } }

def RS.SuperVect.homComponents {V W : SuperVect} (f : V ⟶ W) : (V.even →ₗ[ℂ] W.even) × (V.odd →ₗ[ℂ] W.odd)

The components of a morphism determine it; the additive and module structures are pulled back componentwise.

Equations

• RS.SuperVect.homComponents f = (f.evenMap, f.oddMap)

theorem RS.SuperVect.homComponents_injective {V W : SuperVect} : Function.Injective homComponents

Componentwise equality of morphisms.

@[instance_reducible]

instance RS.SuperVect.instAddCommGroupHom {V W : SuperVect} : AddCommGroup (V ⟶ W)

Morphisms form an abelian group, pulled back along the injection into the pair of component maps.

Equations

• RS.SuperVect.instAddCommGroupHom = Function.Injective.addCommGroup RS.SuperVect.homComponents ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance RS.SuperVect.instModuleComplexHom {V W : SuperVect} : Module ℂ (V ⟶ W)

Morphisms form a ℂ-module, pulled back the same way: SuperVect is ℂ-linear.

Equations

• RS.SuperVect.instModuleComplexHom = Function.Injective.module ℂ { toFun := RS.SuperVect.homComponents, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem RS.SuperVect.add_evenMap {V W : SuperVect} (f g : V ⟶ W) : (f + g).evenMap = f.evenMap + g.evenMap

Addition of morphisms is componentwise on the even part.

@[simp]

theorem RS.SuperVect.add_oddMap {V W : SuperVect} (f g : V ⟶ W) : (f + g).oddMap = f.oddMap + g.oddMap

Addition of morphisms is componentwise on the odd part.

@[simp]

theorem RS.SuperVect.zero_evenMap {V W : SuperVect} : Hom.evenMap 0 = 0

The zero morphism's even component is zero.

@[simp]

theorem RS.SuperVect.zero_oddMap {V W : SuperVect} : Hom.oddMap 0 = 0

The zero morphism's odd component is zero.

@[simp]

theorem RS.SuperVect.smul_evenMap {V W : SuperVect} (c : ℂ) (f : V ⟶ W) : (c • f).evenMap = c • f.evenMap

Scalar multiplication is componentwise on the even part.

@[simp]

theorem RS.SuperVect.smul_oddMap {V W : SuperVect} (c : ℂ) (f : V ⟶ W) : (c • f).oddMap = c • f.oddMap

Scalar multiplication is componentwise on the odd part.

@[instance_reducible]

instance RS.SuperVect.instPreadditive : CategoryTheory.Preadditive SuperVect

SuperVect is preadditive: composition is bilinear componentwise.

Equations

• RS.SuperVect.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

@[instance_reducible]

instance RS.SuperVect.instLinear : CategoryTheory.Linear ℂ SuperVect

SuperVect is ℂ-linear: composition is ℂ-bilinear componentwise.

Equations

• RS.SuperVect.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

10. The vocabulary of Deligne's hypotheses

Subquotients and bounded composition length, scalar unit endomorphisms, iterated and mixed tensor powers, finite ⊗-generation, and moderate growth: exactly the predicates in which the hypothesis list of Théorème 0.6 is phrased. (Their theory continues in RS/Classical/CatTheory/.)

def RS.IsSubquotientOf {C : Type u} [CategoryTheory.Category.{v, u} C] (Y Z : C) : Prop

Y is a subquotient of Z: a quotient of a subobject of Z. This is the relation Deligne's tensor-generation hypothesis is stated with.

Equations

• RS.IsSubquotientOf Y Z = ∃ (S : C) (i : S ⟶ Z) (p : S ⟶ Y), CategoryTheory.Mono i ∧ CategoryTheory.Epi p

theorem RS.isSubquotientOf_of_retract {C : Type u} [CategoryTheory.Category.{v, u} C] {Y Z : C} (i : Y ⟶ Z) (r : Z ⟶ Y) (h : CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Y) : IsSubquotientOf Y Z

A retract is in particular a subquotient: a splitting makes the inclusion a mono, and the object is a quotient of itself.

def RS.LengthLE {C : Type u} [CategoryTheory.Category.{v, u} C] (Y : C) (k : ℕ) : Prop

LengthLE Y k states that the subobject order of Y contains no strictly increasing chain of k + 2 subobjects; equivalently, every chain 0 = Y₀ < ⋯ < Y_ℓ = Y has ℓ ≤ k, so the composition length of Y is at most k.

Equations

• RS.LengthLE Y k = ∀ (f : Fin (k + 2) → CategoryTheory.Subobject Y), ¬StrictMono f

def RS.HasScalarUnit (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] : Prop

The unit's endomorphisms are the scalars.

Equations

• RS.HasScalarUnit A = Function.Bijective fun (c : ℂ) => c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

def RS.tensorPow (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) : ℕ → A

Iterated tensor power of an object.

Equations

• RS.tensorPow A X 0 = CategoryTheory.MonoidalCategoryStruct.tensorUnit A
• RS.tensorPow A X n.succ = CategoryTheory.MonoidalCategoryStruct.tensorObj (RS.tensorPow A X n) X

def RS.mixedPow (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) (a b : ℕ) : A

A mixed tensor power of X: X ^ ⊗ a ⊗ (Xᘁ) ^ ⊗ b.

Equations

• RS.mixedPow A X a b = CategoryTheory.MonoidalCategoryStruct.tensorObj (RS.tensorPow A X a) (RS.tensorPow A Xᘁ b)

def RS.TensorGeneratedBy (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteBiproducts A] [CategoryTheory.RigidCategory A] (X : A) : Prop

Finite tensor generation, in the sense of Deligne's hypothesis: every object is a subquotient of a finite biproduct of mixed tensor powers of X — a quotient of a subobject of such a biproduct.

Equations

• RS.TensorGeneratedBy A X = ∀ (Y : A), ∃ (k : ℕ) (ab : Fin k → ℕ × ℕ), RS.IsSubquotientOf Y (⨁ fun (t : Fin k) => RS.mixedPow A X (ab t).1 (ab t).2)

def RS.ModerateLengthGrowth (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] : Prop

Every object has moderate tensor-power growth, measured by composition length.

Equations

• RS.ModerateLengthGrowth A = ∀ (Y : A), ∃ (C : ℕ) (c : ℕ), ∀ (N : ℕ), RS.LengthLE (RS.tensorPow A Y N) (C * c ^ N)

11. Deligne's theorem

The correspondence with the published hypotheses, item by item: essentially small — [EssentiallySmall.{v} A]; abelian ℂ-linear with ℂ-bilinear tensor — [Abelian A], [Linear ℂ A], [MonoidalPreadditive A], [MonoidalLinear ℂ A]; rigid symmetric monoidal — [MonoidalCategory A], [SymmetricCategory A], [RigidCategory A]; End 𝟙 = ℂ — HasScalarUnit A; finitely ⊗-generated — ∃ X, TensorGeneratedBy A X; moderate growth — ModerateLengthGrowth A. Exactness of the tensor product needs no separate hypothesis (rigidity makes X ⊗ − a two-sided adjoint), and [HasFiniteBiproducts A] is implied by [Abelian A], named only so the generation predicate can be stated. The conclusion is taken in fibre-functor form — weaker than Deligne's ⊗-equivalence with the representations of an affine supergroup scheme, which yields the functor by composing with the forgetful functor.

Reference: Pierre Deligne, Catégories tensorielles, Moscow Math. J. 2 (2002), 227–248, Théorème 0.6 (with §0.1 for the definitions); see also Victor Ostrik, Tensor categories (after P. Deligne), arXiv:math/0401347, Thm 2.3.

structure RS.DeligneFibreFunctor (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] : Type (max (max 1 u_1) u_2)

The conclusion of Deligne's theorem for a candidate tensor category: an exact faithful ℂ-linear symmetric monoidal functor into super vector spaces. This extends the consumed interface (DelignePackage) by the conclusions the development does not use: faithfulness, and exactness in the form of preservation of finite limits and finite colimits.

• ω : CategoryTheory.Functor A SuperVect

  The fibre functor.

• braided : self.ω.Braided

  The fibre functor is symmetric monoidal.

• additive : self.ω.Additive

  The fibre functor is additive.

• linear : CategoryTheory.Functor.Linear ℂ self.ω

  The fibre functor is ℂ-linear.

• faithful : self.ω.Faithful

  The fibre functor is faithful.

• preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits self.ω

  The fibre functor preserves finite limits: the left half of exactness.

• preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits self.ω

  The fibre functor preserves finite colimits: the right half of exactness.

def RS.DeligneTheoremStatement : Prop

Deligne's theorem (Catégories tensorielles, Théorème 0.6): every essentially small abelian ℂ-linear rigid symmetric monoidal category with ℂ-bilinear tensor product, scalar unit endomorphisms, a finite tensor generator and moderate growth of the lengths of its tensor powers admits an exact faithful ℂ-linear symmetric monoidal fibre functor to finite-dimensional super vector spaces.

Equations

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