Documentation

LeanPool.RegtsSevenster.RS.Novel.Skein.MonoidalNat

Naturality of the structural morphisms, fragment level #

The associator and unitor naturality squares of the monoidal skein category, at the fragment level: composing with a cast bundle map on either side is a boundary cast, the tensor associativity and unit laws are relabellings by casts, and all casts collapse through the transport lemmas.

source
noncomputable def RS.assocNatFrag {s₁ t₁ s₂ t₂ s₃ t₃ : ℕ} (F₁ : Fragment (Fin (s₁ + t₁))) (F₂ : Fragment (Fin (s₂ + t₂))) (F₃ : Fragment (Fin (s₃ + t₃))) :
((tensorFragment (tensorFragment F₁ F₂) F₃).compose (bundleMap (finCongr ⋯))).Equiv ((bundleMap (finCongr ⋯)).compose (tensorFragment F₁ (tensorFragment F₂ F₃)))

The associator naturality square, fragment level.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def RS.strandBundleZeroEmpty :
    (strandBundle 0).Equiv emptyClosedFragment

    The zero-strand bundle is the empty closed fragment.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def RS.leftUnitNatFrag {s t : ℕ} (F : Fragment (Fin (s + t))) :
      ((tensorFragment (strandBundle 0) F).compose (bundleMap (finCongr ⋯))).Equiv ((bundleMap (finCongr ⋯)).compose F)

      The left-unitor naturality square, fragment level.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def RS.rightUnitNatFrag {s t : ℕ} (F : Fragment (Fin (s + t))) :
        ((tensorFragment F (strandBundle 0)).compose (bundleMap (finCongr ⋯))).Equiv ((bundleMap (finCongr ⋯)).compose F)

        The right-unitor naturality square, fragment level.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem RS.mem_ker_assocNat {R : ℕ} (f : EdgeRankParameter R) {s₁ t₁ s₂ t₂ s₃ t₃ : ℕ} (x₁ : Fragment (Fin (s₁ + t₁)) →₀ ℂ) (x₂ : Fragment (Fin (s₂ + t₂)) →₀ ℂ) (x₃ : Fragment (Fin (s₃ + t₃)) →₀ ℂ) :
          ((composeFinsupp (s₁ + s₂ + s₃) (t₁ + t₂ + t₃) (t₁ + (t₂ + t₃))) (((tensorFinsupp (s₁ + s₂) (t₁ + t₂) s₃ t₃) (((tensorFinsupp s₁ t₁ s₂ t₂) x₁) x₂)) x₃)) (Finsupp.single (bundleMap (finCongr ⋯)) 1) - ((composeFinsupp (s₁ + s₂ + s₃) (s₁ + (s₂ + s₃)) (t₁ + (t₂ + t₃))) (Finsupp.single (bundleMap (finCongr ⋯)) 1)) (((tensorFinsupp s₁ t₁ (s₂ + s₃) (t₂ + t₃)) x₁) (((tensorFinsupp s₂ t₂ s₃ t₃) x₂) x₃)) ∈ (connectionMap f.val (s₁ + s₂ + s₃ + (t₁ + (t₂ + t₃)))).ker

          The associator-naturality difference lies in the kernel.

          source
          theorem RS.mem_ker_leftUnitNat {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (x : Fragment (Fin (s + t)) →₀ ℂ) :
          ((composeFinsupp (0 + s) (0 + t) t) (((tensorFinsupp 0 0 s t) (Finsupp.single (strandBundle 0) 1)) x)) (Finsupp.single (bundleMap (finCongr ⋯)) 1) - ((composeFinsupp (0 + s) s t) (Finsupp.single (bundleMap (finCongr ⋯)) 1)) x ∈ (connectionMap f.val (0 + s + t)).ker

          The left-unitor-naturality difference lies in the kernel.

          source
          theorem RS.mem_ker_rightUnitNat {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (x : Fragment (Fin (s + t)) →₀ ℂ) :
          ((composeFinsupp (s + 0) (t + 0) t) (((tensorFinsupp s t 0 0) x) (Finsupp.single (strandBundle 0) 1))) (Finsupp.single (bundleMap (finCongr ⋯)) 1) - ((composeFinsupp (s + 0) s t) (Finsupp.single (bundleMap (finCongr ⋯)) 1)) x ∈ (connectionMap f.val (s + 0 + t)).ker

          The right-unitor-naturality difference lies in the kernel.

          source
          theorem RS.assocNat_class {R : ℕ} (f : EdgeRankParameter R) {s₁ t₁ s₂ t₂ s₃ t₃ : ℕ} (p₁ : HomSpace f.val (s₁ + t₁)) (p₂ : HomSpace f.val (s₂ + t₂)) (p₃ : HomSpace f.val (s₃ + t₃)) :
          ((HomSpace.comp f (s₁ + s₂ + s₃) (t₁ + t₂ + t₃) (t₁ + (t₂ + t₃))) (((HomSpace.tensor f (s₁ + s₂) (t₁ + t₂) s₃ t₃) (((HomSpace.tensor f s₁ t₁ s₂ t₂) p₁) p₂)) p₃)) (bundleMapClass f (finCongr ⋯)) = ((HomSpace.comp f (s₁ + s₂ + s₃) (s₁ + (s₂ + s₃)) (t₁ + (t₂ + t₃))) (bundleMapClass f (finCongr ⋯))) (((HomSpace.tensor f s₁ t₁ (s₂ + s₃) (t₂ + t₃)) p₁) (((HomSpace.tensor f s₂ t₂ s₃ t₃) p₂) p₃))

          Associator naturality on Hom classes.

          source
          theorem RS.leftUnitNat_class {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (p : HomSpace f.val (s + t)) :
          ((HomSpace.comp f (0 + s) (0 + t) t) (((HomSpace.tensor f 0 0 s t) (HomSpace.ofFragment f.val (strandBundle 0))) p)) (bundleMapClass f (finCongr ⋯)) = ((HomSpace.comp f (0 + s) s t) (bundleMapClass f (finCongr ⋯))) p

          Left-unitor naturality on Hom classes.

          source
          theorem RS.rightUnitNat_class {R : ℕ} (f : EdgeRankParameter R) {s t : ℕ} (p : HomSpace f.val (s + t)) :
          ((HomSpace.comp f (s + 0) (t + 0) t) (((HomSpace.tensor f s t 0 0) p) (HomSpace.ofFragment f.val (strandBundle 0)))) (bundleMapClass f (finCongr ⋯)) = ((HomSpace.comp f (s + 0) s t) (bundleMapClass f (finCongr ⋯))) p

          Right-unitor naturality on Hom classes.