Instantiation of the Γ-algebra substrate at Ind SmallSuperVect

RS.SuperGamma builds the four-block super-commutative algebra superGammaAlgebra of a commutative monoid object over any braided ℂ-linear ambient with an odd line (o, ho, hβ, hα). This file executes the instantiation plan recorded there: the ambient is Ind SmallSuperVect, the odd line is the embedded odd generator indOf.obj sOdd, and the three hypotheses are proved.

• The transported monoidal, symmetric and preadditive structure on SmallSuperVect is installed from SuperVect across the small-model equivalence (Monoidal.transport); the scalar unit ℂ ≃+* End (𝟙_ SmallSuperVect) follows by full faithfulness of the inclusion.

• The three odd-line facts are proved once, by hand, in SuperVect at the standard odd line ℂ^{0|1} (hβ is the existing stdSuper_braiding_neg; hα is the elementwise computation superOdd_coherence), then moved along functors by a reusable braided comparison calculus: a RS.BraidedComparison F packages a unit comparison, a tensor comparison, and the monoidal-functor axioms for F, and the odd-line data (ho, hβ, hα) transports forwards along any comparison (coherence_map, braiding_neg_map) and reflects backwards along a faithful one (coherence_reflect, braiding_neg_reflect). Reflection along the small-model inclusion lands the facts on sOdd; forward transport along the embedding comparison of indOf (assembled from the IndSchur/SchurTransport lemmas as indOfComparison) lifts them to Ind SmallSuperVect.

• superGammaAlgebraInd assembles the resulting RS.SuperCommAlgebra for any commutative monoid object R of Ind SmallSuperVect, with the ℂ-linear structure installed from the scalar unit as in RS.ScalarLinear.

Braided comparisons and transport of odd-line data

A braided comparison on a functor between braided monoidal categories is monoidal-functor data up to isomorphism: a unit comparison, a tensor comparison, and the naturality, associativity, unitality and braiding axioms. indOf carries exactly this data through the lemmas of RS.IndTensorExact, RS.IndSchur and RS.SchurTransport without a registered Functor.Monoidal instance, which is why the data is packaged explicitly rather than through the Mathlib classes. Right unitality is derived from left unitality through the braiding, so it is not a field.

structure RS.BraidedComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C D) : Type (max u v')

Monoidal-functor data up to isomorphism on F, with the braiding axiom: the odd-line transport interface.

• unitIso : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

  The unit comparison.

• tensorIso (x y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj x) (F.obj y) ≅ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

  The tensor comparison.

• natural_left {x x' : C} (f : x ⟶ x') (y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj y)) (self.tensorIso x' y).hom = CategoryTheory.CategoryStruct.comp (self.tensorIso x y).hom (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y))

  Naturality of the tensor comparison in the left factor.

• natural_right (x : C) {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (F.map g)) (self.tensorIso x y').hom = CategoryTheory.CategoryStruct.comp (self.tensorIso x y).hom (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g))

  Naturality of the tensor comparison in the right factor.

• associativity (x y z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.tensorIso x y).hom (F.obj z)) (CategoryTheory.CategoryStruct.comp (self.tensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z).hom (F.map (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x) (F.obj y) (F.obj z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (self.tensorIso y z).hom) (self.tensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)).hom)

  The associativity axiom.

• left_unitality (x : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj x)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.unitIso.hom (F.obj x)) (CategoryTheory.CategoryStruct.comp (self.tensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) x).hom (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom))

  The left unitality axiom.

• braiding (x y : C) : CategoryTheory.CategoryStruct.comp (β_ (F.obj x) (F.obj y)).hom (self.tensorIso y x).hom = CategoryTheory.CategoryStruct.comp (self.tensorIso x y).hom (F.map (β_ x y).hom)

  The braiding axiom.

def RS.BraidedComparison.ofBraidedFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C D) [F.Braided] : BraidedComparison F

A braided functor carries the canonical braided comparison.

Equations

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

theorem RS.BraidedComparison.right_unitality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (x : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) P.unitIso.hom) (CategoryTheory.CategoryStruct.comp (P.tensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom))

Right unitality is derived: the braiding turns the right unitor of F.obj x into its left unitor, the braiding axiom carries the braiding downstairs, and the braiding identity of the base returns the right unitor.

def RS.BraidedComparison.square {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj o) (F.obj o) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The transported odd-square trivialization: conjugate ho by the tensor and unit comparisons.

Equations

• P.square o ho = P.tensorIso o o ≪≫ F.mapIso ho ≪≫ P.unitIso.symm

theorem RS.BraidedComparison.square_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : (P.square o ho).inv = CategoryTheory.CategoryStruct.comp P.unitIso.hom (CategoryTheory.CategoryStruct.comp (F.map ho.inv) (P.tensorIso o o).inv)

The inverse of the transported odd square, in components.

theorem RS.BraidedComparison.leftUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (x : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj x)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).inv) (CategoryTheory.CategoryStruct.comp (P.tensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) x).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.unitIso.inv (F.obj x)))

Inverse form of left unitality.

theorem RS.BraidedComparison.rightUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (x : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv) (CategoryTheory.CategoryStruct.comp (P.tensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) P.unitIso.inv))

Inverse form of right unitality.

theorem RS.BraidedComparison.natural_left_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) {x x' : C} (f : x ⟶ x') (y : C) : CategoryTheory.CategoryStruct.comp (P.tensorIso x y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj y)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y)) (P.tensorIso x' y).inv

Inverse form of naturality in the left factor.

theorem RS.BraidedComparison.natural_right_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (x : C) {y y' : C} (g : y ⟶ y') : CategoryTheory.CategoryStruct.comp (P.tensorIso x y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (F.map g)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g)) (P.tensorIso x y').inv

Inverse form of naturality in the right factor.

theorem RS.BraidedComparison.associativity_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (x y z : C) : CategoryTheory.CategoryStruct.comp (P.tensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (P.tensorIso x y).inv (F.obj z)) (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x) (F.obj y) (F.obj z)).hom) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) (CategoryTheory.CategoryStruct.comp (P.tensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (P.tensorIso y z).inv))

Inverse form of associativity.

theorem RS.BraidedComparison.conv_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj o)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (P.square o ho).inv (F.obj o)) (CategoryTheory.MonoidalCategoryStruct.associator (F.obj o) (F.obj o) (F.obj o)).hom) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor o).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ho.inv o) (CategoryTheory.MonoidalCategoryStruct.associator o o o).hom))) (CategoryTheory.CategoryStruct.comp (P.tensorIso o (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj o) (P.tensorIso o o).inv))

The left odd-line pattern in components: the transported form of (λ_ o).inv ≫ ho.inv ▷ o ≫ (α_ o o o).hom is the image of the pattern downstairs, followed by the inverse triple-tensor comparison.

theorem RS.BraidedComparison.conv_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj o)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj o) (P.square o ho).inv) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor o).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft o ho.inv))) (CategoryTheory.CategoryStruct.comp (P.tensorIso o (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj o) (P.tensorIso o o).inv))

The right odd-line pattern in components: the transported form of (ρ_ o).inv ≫ o ◁ ho.inv is the image of the pattern downstairs, followed by the same inverse comparison.

theorem RS.BraidedComparison.coherence_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (hα : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor o).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ho.inv o) (CategoryTheory.MonoidalCategoryStruct.associator o o o).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor o).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft o ho.inv)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj o)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (P.square o ho).inv (F.obj o)) (CategoryTheory.MonoidalCategoryStruct.associator (F.obj o) (F.obj o) (F.obj o)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj o)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj o) (P.square o ho).inv)

Forward transport of the odd-cubed coherence: the hypothesis hα of RS.superGammaAlgebra moves along any braided comparison.

theorem RS.BraidedComparison.coherence_reflect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} (P : BraidedComparison F) [F.Faithful] (o : C) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (hα : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj o)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (P.square o ho).inv (F.obj o)) (CategoryTheory.MonoidalCategoryStruct.associator (F.obj o) (F.obj o) (F.obj o)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj o)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj o) (P.square o ho).inv)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor o).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ho.inv o) (CategoryTheory.MonoidalCategoryStruct.associator o o o).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor o).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft o ho.inv)

Reflection of the odd-cubed coherence: along a faithful braided comparison, hα downstairs at the transported square forces hα upstairs.

theorem RS.BraidedComparison.braiding_neg_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (P : BraidedComparison F) {o : C} (hβ : (β_ o o).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)) : (β_ (F.obj o) (F.obj o)).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj o) (F.obj o))

Forward transport of the odd braiding sign along an additive braided comparison.

theorem RS.BraidedComparison.braiding_neg_reflect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.Functor C D} [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] [F.Faithful] (P : BraidedComparison F) {o : C} (hβ : (β_ (F.obj o) (F.obj o)).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj o) (F.obj o))) : (β_ o o).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)

Reflection of the odd braiding sign along a faithful additive braided comparison.

The odd line of SuperVect, trivialized

The standard odd line ℂ^{0|1} of SuperVect carries the trivialization superOddSquare : ℂ^{0|1} ⊗ ℂ^{0|1} ≅ 𝟙, pairing the two odd generators; its braiding sign is RS.stdSuper_braiding_neg, and the odd-cubed coherence hα is the elementwise computation superOdd_coherence: both insertions of the trivialized square send the odd generator e to e ⊗ e ⊗ e.

def RS.prodZeroEquiv (A M : Type) [AddCommGroup A] [Module ℂ A] [AddCommGroup M] [Module ℂ M] [Subsingleton A] : (A × M) ≃ₗ[ℂ] M

A product with a subsingleton first factor is its second factor.

Equations

• RS.prodZeroEquiv A M = { toFun := fun (p : A × M) => p.2, map_add' := ⋯, map_smul' := ⋯, invFun := fun (m : M) => (0, m), left_inv := ⋯, right_inv := ⋯ }

def RS.lineTensorEquiv : TensorProduct ℂ (Fin 1 → ℂ) (Fin 1 → ℂ) ≃ₗ[ℂ] ℂ

The square of the scalar line, trivialized.

Equations

• RS.lineTensorEquiv = TensorProduct.congr (LinearEquiv.funUnique (Fin 1) ℂ ℂ) (LinearEquiv.funUnique (Fin 1) ℂ ℂ) ≪≫ₗ TensorProduct.lid ℂ ℂ

def RS.superOddSquare : CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSuper 0 1) (stdSuper 0 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect

The trivialization of the odd square in SuperVect: the even component pairs the two odd lines through lineTensorEquiv, and the odd component is trivial.

Equations

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

theorem RS.superOdd_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (stdSuper 0 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight superOddSquare.inv (stdSuper 0 1)) (CategoryTheory.MonoidalCategoryStruct.associator (stdSuper 0 1) (stdSuper 0 1) (stdSuper 0 1)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (stdSuper 0 1)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSuper 0 1) superOddSquare.inv)

The odd-cubed coherence holds in SuperVect at the standard odd line: both insertions of the trivialized square send the odd generator to the triple tensor of generators.

The transported structure on the small model

SmallSuperVect receives the monoidal and symmetric structure of SuperVect across the small-model equivalence, by Monoidal.transport; the inclusion is then monoidal, braided, faithful and additive, so preadditivity of the tensor and the scalar unit follow by reflection.

@[instance_reducible]

noncomputable instance RS.instMonoidalCategorySmallSuperVect : CategoryTheory.MonoidalCategory SmallSuperVect

The monoidal structure of the small model, transported from SuperVect across the small-model equivalence.

Equations

• RS.instMonoidalCategorySmallSuperVect = CategoryTheory.Monoidal.transport RS.smallSuperEquiv.symm

@[instance_reducible]

noncomputable instance RS.instSymmetricCategorySmallSuperVect : CategoryTheory.SymmetricCategory SmallSuperVect

The symmetry of the small model.

Equations

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

@[instance_reducible]

noncomputable instance RS.instMonoidalSmallSuperVectSuperVectSmallSuperInclusion : smallSuperInclusion.Monoidal

The inclusion is monoidal for the transported structure.

Equations

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

@[instance_reducible]

noncomputable instance RS.instBraidedSmallSuperVectSuperVectSmallSuperInclusion : smallSuperInclusion.Braided

The inclusion is braided for the transported structure.

Equations

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

instance RS.instMonoidalPreadditiveSmallSuperVect : CategoryTheory.MonoidalPreadditive SmallSuperVect

The small model is monoidal preadditive, by reflection along the faithful additive monoidal inclusion.

def RS.unitEvenMap (f : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect)) : ℂ →ₗ[ℂ] ℂ

The even component of a unit endomorphism, at the scalar type.

Equations

• RS.unitEvenMap f = f.evenMap

def RS.superVectScalarUnit : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect)

The scalar unit of SuperVect: endomorphisms of the monoidal unit are the scalars.

Equations

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

def RS.smallEndRingEquiv (x : SmallSuperVect) : CategoryTheory.End x ≃+* CategoryTheory.End (smallSuperInclusion.obj x)

Full faithfulness of the inclusion on endomorphisms, as a ring isomorphism; End-multiplication is reversed composition on both sides, and the inclusion is functorial on the nose.

Equations

• RS.smallEndRingEquiv x = { toEquiv := CategoryTheory.InducedCategory.homAddEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

noncomputable def RS.smallScalarUnit : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit SmallSuperVect)

The scalar unit of the small model: transport the scalar unit of SuperVect along the unit comparison of the inclusion and pull back by full faithfulness.

Equations

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

noncomputable def RS.smallComparison : BraidedComparison smallSuperInclusion

The canonical braided comparison on the inclusion.

Equations

• RS.smallComparison = RS.BraidedComparison.ofBraidedFunctor RS.smallSuperInclusion

noncomputable def RS.smallOddSquare : CategoryTheory.MonoidalCategoryStruct.tensorObj sOdd sOdd ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit SmallSuperVect

The trivialized odd square of the small model: the SuperVect trivialization of the embedded odd generator, pulled back through the fully faithful inclusion.

Equations

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

theorem RS.smallComparison_square : smallComparison.square sOdd smallOddSquare = superOddSquare

The comparison square of smallOddSquare is the SuperVect trivialization it was pulled back from.

theorem RS.smallOdd_braiding : (β_ sOdd sOdd).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj sOdd sOdd)

The braiding sign at the small odd generator, by reflection along the inclusion from RS.stdSuper_braiding_neg.

theorem RS.smallOdd_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor sOdd).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight smallOddSquare.inv sOdd) (CategoryTheory.MonoidalCategoryStruct.associator sOdd sOdd sOdd).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor sOdd).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft sOdd smallOddSquare.inv)

The odd-cubed coherence at the small odd generator, by reflection along the inclusion from RS.superOdd_coherence.

The embedding comparison of indOf

noncomputable def RS.indOfComparison {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : BraidedComparison indOf

The braided comparison of the ind-embedding: the unit and tensor comparisons of RS.IndSchur and RS.SchurTransport assemble into a braided comparison on indOf, over any braided small base.

Equations

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

The odd line of Ind SmallSuperVect and the Γ-algebra

noncomputable def RS.indOddLine : CategoryTheory.Ind SmallSuperVect

The odd line of the instantiated ambient: the embedded odd generator of the small model.

Equations

• RS.indOddLine = RS.indOf.obj RS.sOdd

noncomputable def RS.indOddSquare : CategoryTheory.MonoidalCategoryStruct.tensorObj indOddLine indOddLine ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind SmallSuperVect)

The trivialized odd square of the ambient: the transported small-model trivialization.

Equations

• RS.indOddSquare = RS.indOfComparison.square RS.sOdd RS.smallOddSquare

theorem RS.indOdd_braiding : (β_ indOddLine indOddLine).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj indOddLine indOddLine)

The braiding sign at the odd line of the ambient: the hypothesis hβ of RS.superGammaAlgebra.

theorem RS.indOdd_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor indOddLine).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight indOddSquare.inv indOddLine) (CategoryTheory.MonoidalCategoryStruct.associator indOddLine indOddLine indOddLine).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor indOddLine).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft indOddLine indOddSquare.inv)

The odd-cubed coherence at the odd line of the ambient: the hypothesis hα of RS.superGammaAlgebra.

noncomputable def RS.superGammaAlgebraInd (R : CategoryTheory.Ind SmallSuperVect) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : SuperCommAlgebra

The Γ-algebra of the instantiated ambient: for any commutative monoid object R of Ind SmallSuperVect, the morphisms out of the unit and out of the embedded odd generator form a super-commutative ℂ-algebra under prefixed convolution — RS.superGammaAlgebra at the odd line indOddLine, with the ℂ-linear structure installed from the scalar unit of the small model as in RS.ScalarLinear.

Equations

• RS.superGammaAlgebraInd R = RS.superGammaAlgebra R RS.indOddLine RS.indOddSquare RS.indOdd_braiding RS.indOdd_coherence

Acceptance