Coherence and invertibility of the comparison

The comparison of Comparison.lean satisfies the three laws of a lax monoidal structure and intertwines the braidings: each is transported from the corresponding law over the algebra, proved in Residue.lean, through the coordinates, using the generator calculus of Calculus.lean. It is moreover invertible for every pair of modules — the inverse built alongside it undoes it on generators — as is the unit comparison; this is the usual strength of base change along an algebra map, in super form.

Contents

• RS.superVectMu_associativity, RS.superVectMu_left_unitality, RS.superVectMu_right_unitality, RS.superVectMu_braiding: the coherence of the comparison in RS.SuperVect.
• RS.superVectMu_naturality_left, RS.superVectMu_naturality_right, RS.superVectMuEvenRaw_naturality and its odd companion: naturality in either variable, before and after the coordinates.
• RS.superVectMuEvenRaw_baseNuEven, RS.baseNuEven_superVectMuEvenRaw and their odd companions: the two composites of the comparison with its inverse.
• RS.SuperVect.isoOfBijective: a morphism of super vector spaces with bijective components is an isomorphism.
• RS.superVectEps: the unit of the fibre functor.
• RS.superVectMuIso, RS.isIso_superVectMu, RS.superVectEpsIso, RS.isIso_superVectEps: both comparisons are invertible.

Associativity of the comparison

theorem RS.superVectMu_associativity {S : SuperCommAlgebra} (P : SuperPoint S) (M N Q : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((N.tensor Q).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((N.tensor Q).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (((M.tensor N).tensor Q).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (((M.tensor N).tensor Q).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor (N.tensor Q)).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor (N.tensor Q)).tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (superVectMu P M N) (toSuperVect P Q)) (CategoryTheory.CategoryStruct.comp (superVectMu P (M.tensor N) Q) (superVectHom P (CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (toSuperVect P M) (toSuperVect P N) (toSuperVect P Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toSuperVect P M) (superVectMu P N Q)) (superVectMu P M (N.tensor Q)))

Associativity of the monoidal comparison.

theorem RS.superVectMu_associativity_assoc {S : SuperCommAlgebra} (P : SuperPoint S) (M N Q : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (Q.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((N.tensor Q).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((N.tensor Q).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (((M.tensor N).tensor Q).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (((M.tensor N).tensor Q).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor (N.tensor Q)).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor (N.tensor Q)).tensor (SuperCommAlgebra.pointMod P)).odd] {Z : SuperVect} (h : toSuperVect P (CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorObj N Q)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (superVectMu P M N) (toSuperVect P Q)) (CategoryTheory.CategoryStruct.comp (superVectMu P (M.tensor N) Q) (CategoryTheory.CategoryStruct.comp (superVectHom P (CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (toSuperVect P M) (toSuperVect P N) (toSuperVect P Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toSuperVect P M) (superVectMu P N Q)) (CategoryTheory.CategoryStruct.comp (superVectMu P M (N.tensor Q)) h))

Associativity of the monoidal comparison.

Naturality of the comparison in super vector spaces

theorem RS.superVectMu_naturality_left {S : SuperCommAlgebra} (P : SuperPoint S) {M M' N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (M'.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M'.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M'.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M'.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] (f : M ⟶ M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (superVectHom P f) (toSuperVect P N)) (superVectMu P M' N) = CategoryTheory.CategoryStruct.comp (superVectMu P M N) (superVectHom P (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N))

The comparison is natural in the left variable.

theorem RS.superVectMu_naturality_right {S : SuperCommAlgebra} (P : SuperPoint S) {M N N' : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N'.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N'.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N').tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N').tensor (SuperCommAlgebra.pointMod P)).odd] (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toSuperVect P M) (superVectHom P g)) (superVectMu P M N') = CategoryTheory.CategoryStruct.comp (superVectMu P M N) (superVectHom P (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g))

The comparison is natural in the right variable.

The comparison is invertible

theorem RS.pointEven_eq_smul_one {S : SuperCommAlgebra} (P : SuperPoint S) (a : (SuperCommAlgebra.pointMod P).even) : a = a.down • pointOne P

A residue class is its own coordinate times the unit.

theorem RS.pointOne_mul_self {S : SuperCommAlgebra} (P : SuperPoint S) : { down := (pointOne P).down * (pointOne P).down } = pointOne P

The unit of the residue module is idempotent.

theorem RS.tmulEE_point_eq_smul {S : SuperCommAlgebra} (P : SuperPoint S) {M : S.Mod} (m : M.even) (a : (SuperCommAlgebra.pointMod P).even) : ((M.tmulEE (SuperCommAlgebra.pointMod P)) m) a = a.down • ((M.tmulEE (SuperCommAlgebra.pointMod P)) m) (pointOne P)

An even product with a residue class is a multiple of the product with the unit.

theorem RS.tmulOE_point_eq_smul {S : SuperCommAlgebra} (P : SuperPoint S) {M : S.Mod} (m : M.odd) (a : (SuperCommAlgebra.pointMod P).even) : ((M.tmulOE (SuperCommAlgebra.pointMod P)) m) a = a.down • ((M.tmulOE (SuperCommAlgebra.pointMod P)) m) (pointOne P)

An odd product with a residue class is a multiple of the product with the unit.

theorem RS.superVectMuEvenRaw_baseNuEven {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (w : ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even) : (superVectMuEvenRaw P M N) ((baseNuEven P M N) w) = w

The comparison undoes the inverse, in even degree.

theorem RS.superVectMuOddRaw_baseNuOdd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (w : ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd) : (superVectMuOddRaw P M N) ((baseNuOdd P M N) w) = w

The comparison undoes the inverse, in odd degree.

theorem RS.smulPairInl {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z] (c d : ℂ) (x : X) (y : Y) : (c * d) • (x ⊗ₜ[ℂ] y, 0) = ((c • x) ⊗ₜ[ℂ] (d • y), 0)

A scaled pure tensor in the first summand of a pair.

theorem RS.smulPairInr {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y] [AddCommGroup Z] [Module ℂ Z] (c d : ℂ) (x : X) (y : Y) : (c * d) • (0, x ⊗ₜ[ℂ] y) = (0, (c • x) ⊗ₜ[ℂ] (d • y))

A scaled pure tensor in the second summand of a pair.

The inverse undoes the comparison

theorem RS.baseNuEven_muRaw_inl {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even).compr₂ (LinearMap.inl ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd))).compr₂ (baseNuEven P M N ∘ₗ superVectMuEvenRaw P M N) = (TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even).compr₂ (LinearMap.inl ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd))

The even-even half of the inverse identity.

theorem RS.baseNuEven_muRaw_inr {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd).compr₂ (LinearMap.inr ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd))).compr₂ (baseNuEven P M N ∘ₗ superVectMuEvenRaw P M N) = (TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd).compr₂ (LinearMap.inr ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).even) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).odd))

The odd-odd half of the inverse identity in even degree.

theorem RS.baseNuOdd_muRaw_inl {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd).compr₂ (LinearMap.inl ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even))).compr₂ (baseNuOdd P M N ∘ₗ superVectMuOddRaw P M N) = (TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd).compr₂ (LinearMap.inl ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even))

The even-odd half of the inverse identity in odd degree.

theorem RS.baseNuOdd_muRaw_inr {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even).compr₂ (LinearMap.inr ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even))).compr₂ (baseNuOdd P M N ∘ₗ superVectMuOddRaw P M N) = (TensorProduct.mk ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even).compr₂ (LinearMap.inr ℂ (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even (N.tensor (SuperCommAlgebra.pointMod P)).odd) (TensorProduct ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd (N.tensor (SuperCommAlgebra.pointMod P)).even))

The odd-even half of the inverse identity in odd degree.

theorem RS.baseNuEven_superVectMuEvenRaw {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (z : basePairEven P M N) : (baseNuEven P M N) ((superVectMuEvenRaw P M N) z) = z

The inverse undoes the comparison, in even degree.

theorem RS.baseNuOdd_superVectMuOddRaw {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (z : basePairOdd P M N) : (baseNuOdd P M N) ((superVectMuOddRaw P M N) z) = z

The inverse undoes the comparison, in odd degree.

The comparison is an isomorphism

noncomputable def RS.SuperVect.isoOfBijective {V W : SuperVect} (f : V ⟶ W) (he : Function.Bijective ⇑f.evenMap) (ho : Function.Bijective ⇑f.oddMap) : V ≅ W

A morphism of super vector spaces with bijective components is an isomorphism.

Equations

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

theorem RS.superVectMuEvenRaw_bijective {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : Function.Bijective ⇑(superVectMuEvenRaw P M N)

The raw comparison is bijective in even degree.

theorem RS.superVectMuOddRaw_bijective {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : Function.Bijective ⇑(superVectMuOddRaw P M N)

The raw comparison is bijective in odd degree.

theorem RS.superVectMu_evenMap_bijective {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] : Function.Bijective ⇑(superVectMu P M N).evenMap

The even component of the comparison is bijective.

theorem RS.superVectMu_oddMap_bijective {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] : Function.Bijective ⇑(superVectMu P M N).oddMap

The odd component of the comparison is bijective.

noncomputable def RS.superVectMuIso {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.MonoidalCategoryStruct.tensorObj (toSuperVect P M) (toSuperVect P N) ≅ toSuperVect P (M.tensor N)

The monoidal comparison is an isomorphism of super vector spaces: base change at a complex point is strong, not merely lax.

Equations

• RS.superVectMuIso P M N = RS.SuperVect.isoOfBijective (RS.superVectMu P M N) ⋯ ⋯

instance RS.isIso_superVectMu {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.IsIso (superVectMu P M N)

The monoidal comparison is invertible.

noncomputable def RS.superVectEpsRaw {S : SuperCommAlgebra} (P : SuperPoint S) : ℂ →ₗ[ℂ] (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even

The unit comparison of the fibre functor, before the coordinates are installed: a complex number is scaled into the algebra and pushed into the base change.

Equations

• RS.superVectEpsRaw P = (RS.pointBaseEps P).evenMap ∘ₗ LinearMap.toSpanSingleton ℂ S.even S.one

noncomputable def RS.superVectEps {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] : CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect ⟶ toSuperVect P S.unitMod

The unit comparison of the fibre functor: the unit super vector space maps to the base change of the unit module.

Equations

• RS.superVectEps P = { evenMap := ↑(RS.toSuperVectEvenEquiv P S.unitMod) ∘ₗ RS.superVectEpsRaw P, oddMap := 0 }

theorem RS.superVectEpsRaw_apply {S : SuperCommAlgebra} (P : SuperPoint S) (r : ℂ) : (superVectEpsRaw P) r = (pointBaseEps P).evenMap ((LinearMap.toSpanSingleton ℂ S.even S.one) r)

The raw unit comparison, evaluated.

theorem RS.superVectEps_evenMap_apply {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] (r : ℂ) : (superVectEps P).evenMap r = (toSuperVectEvenEquiv P S.unitMod) ((superVectEpsRaw P) r)

The unit comparison, evaluated.

The unit comparison is an isomorphism

theorem RS.unitTensorPoint_superVectEpsRaw {S : SuperCommAlgebra} (P : SuperPoint S) (c : ℂ) : (unitTensorPoint P).hom.evenMap ((superVectEpsRaw P) c) = { down := c }

The unit comparison, read through the left unitor, is the canonical copy of a complex number in the residue module.

theorem RS.superVectEpsRaw_bijective {S : SuperCommAlgebra} (P : SuperPoint S) : Function.Bijective ⇑(superVectEpsRaw P)

The raw unit comparison is bijective.

instance RS.subsingleton_unitMod_tensor_point_odd {S : SuperCommAlgebra} (P : SuperPoint S) : Subsingleton (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd

The odd part of the base change of the unit module vanishes.

instance RS.subsingleton_toSuperVect_unitMod_odd {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : Subsingleton (toSuperVect P S.unitMod).odd

The odd part of the fibre of the unit module vanishes.

theorem RS.superVectEps_evenMap_bijective {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] : Function.Bijective ⇑(superVectEps P).evenMap

The even component of the unit comparison is bijective.

theorem RS.superVectEps_oddMap_bijective {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : Function.Bijective ⇑(superVectEps P).oddMap

The odd component of the unit comparison is bijective: both sides vanish.

noncomputable def RS.superVectEpsIso {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect ≅ toSuperVect P S.unitMod

The unit comparison is an isomorphism of super vector spaces.

Equations

• RS.superVectEpsIso P = RS.SuperVect.isoOfBijective (RS.superVectEps P) ⋯ ⋯

instance RS.isIso_superVectEps {S : SuperCommAlgebra} (P : SuperPoint S) [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.IsIso (superVectEps P)

The unit comparison is invertible.

Unitality of the comparison

theorem RS.superVectMu_left_unitality {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((S.unitMod.tensor M).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((S.unitMod.tensor M).tensor (SuperCommAlgebra.pointMod P)).odd] : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (toSuperVect P M)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (superVectEps P) (toSuperVect P M)) (CategoryTheory.CategoryStruct.comp (superVectMu P S.unitMod M) (superVectHom P (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom))

Left unitality of the monoidal comparison.

theorem RS.superVectMu_right_unitality {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor S.unitMod).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor S.unitMod).tensor (SuperCommAlgebra.pointMod P)).odd] : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (toSuperVect P M)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toSuperVect P M) (superVectEps P)) (CategoryTheory.CategoryStruct.comp (superVectMu P M S.unitMod) (superVectHom P (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom))

Right unitality of the monoidal comparison.

Naturality of the comparison

theorem RS.superVectMuEvenRaw_naturality {S : SuperCommAlgebra} (P : SuperPoint S) {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') : (SuperCommAlgebra.Mod.tensorHom (SuperCommAlgebra.Mod.tensorHom f g) (CategoryTheory.CategoryStruct.id (SuperCommAlgebra.pointMod P))).evenMap ∘ₗ superVectMuEvenRaw P M N = superVectMuEvenRaw P M' N' ∘ₗ (TensorProduct.map (SuperCommAlgebra.Mod.tensorHom f (CategoryTheory.CategoryStruct.id (SuperCommAlgebra.pointMod P))).evenMap (SuperCommAlgebra.Mod.tensorHom g (CategoryTheory.CategoryStruct.id (SuperCommAlgebra.pointMod P))).evenMap).prodMap (TensorProduct.map (SuperCommAlgebra.Mod.tensorHom f (CategoryTheory.CategoryStruct.id (SuperCommAlgebra.pointMod P))).oddMap (SuperCommAlgebra.Mod.tensorHom g (CategoryTheory.CategoryStruct.id (SuperCommAlgebra.pointMod P))).oddMap)

The raw comparison is natural in both variables, in even degree.

The comparison intertwines the braidings

theorem RS.superVectMu_braiding {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((N.tensor M).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((N.tensor M).tensor (SuperCommAlgebra.pointMod P)).odd] : CategoryTheory.CategoryStruct.comp (superVectMu P M N) (superVectHom P (β_ M N).hom) = CategoryTheory.CategoryStruct.comp (β_ (toSuperVect P M) (toSuperVect P N)).hom (superVectMu P N M)

The monoidal comparison intertwines the braidings: the Koszul sign of the super vector spaces is the sign of the braiding of the super modules.

theorem RS.superVectMu_braiding_assoc {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ ((N.tensor M).tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ ((N.tensor M).tensor (SuperCommAlgebra.pointMod P)).odd] {Z : SuperVect} (h : toSuperVect P (CategoryTheory.MonoidalCategoryStruct.tensorObj N M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (superVectMu P M N) (CategoryTheory.CategoryStruct.comp (superVectHom P (β_ M N).hom) h) = CategoryTheory.CategoryStruct.comp (β_ (toSuperVect P M) (toSuperVect P N)).hom (CategoryTheory.CategoryStruct.comp (superVectMu P N M) h)

The monoidal comparison intertwines the braidings: the Koszul sign of the super vector spaces is the sign of the braiding of the super modules.