The model transport

Given the strand identification of the standard model, the iterated identification of the monoidal powers: stdToOmega assembles copies of the strand map left-nested through the structure maps of the fibre functor, stdFromOmega disassembles, and the two are mutually inverse whenever the strand maps are.

noncomputable def RS.stdToOmega {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) : superPow (stdSuperPair k ℓ) m ⟶ P.ω.obj { arity := m }

The model transport: iterated strand identifications assembled left-nested through the structure maps.

Equations

• One or more equations did not get rendered due to their size.
• RS.stdToOmega f P e 0 = CategoryTheory.Functor.LaxMonoidal.ε P.ω

noncomputable def RS.stdFromOmega {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (m : ℕ) : P.ω.obj { arity := m } ⟶ superPow (stdSuperPair k ℓ) m

The reverse model transport.

Equations

• One or more equations did not get rendered due to their size.
• RS.stdFromOmega f P e' 0 = CategoryTheory.Functor.OplaxMonoidal.η P.ω

theorem RS.stdFromOmega_stdToOmega {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (m : ℕ) : CategoryTheory.CategoryStruct.comp (stdFromOmega f P e' m) (stdToOmega f P e m) = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := m })

The transports are inverse on the fibre side.

theorem RS.stdToOmega_stdFromOmega {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (he'e : CategoryTheory.CategoryStruct.comp e e' = CategoryTheory.CategoryStruct.id (stdSuperPair k ℓ)) (m : ℕ) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e m) (stdFromOmega f P e' m) = CategoryTheory.CategoryStruct.id (superPow (stdSuperPair k ℓ) m)

The transports are inverse on the model side.