The comparison in super vector spaces, and its inverse

The tensor product of two super vector spaces is the graded tensor product of the components, while the tensor product of two super modules is its quotient by the balancing relations; the quotient map is the second half of the comparison, and composing it with the comparison over the algebra of Residue.lean gives the comparison RS.superVectMu of the fibre functor.

The inverse is built here as well: the residue module is generated in even degree by the image of the unit, so (m ⊗ n) ⊗ a ↦ (m ⊗ a) ⊗ (n ⊗ 1) is well defined — an even scalar crosses either factor as its value at the point, and an odd scalar kills both sides. That the two composites are the identity is proved in Coherence.lean; no freeness and no rank hypothesis is needed.

Contents

• RS.pointOne, RS.pointScale: the unit of the residue module and the scaling it induces, with the four generator identities RS.tmulEE_actEE_pointOne and companions.
• RS.gradedTensorEven, RS.gradedTensorOdd: the quotient maps from the graded tensor product of the components, with their surjectivity and their naturality.
• RS.baseNuEven, RS.baseNuOdd: the inverse comparison, built from the four balanced blocks RS.baseNuFee and companions through an inner and an outer lift.
• RS.superVectMuEvenRaw, RS.superVectMuOddRaw: the comparison before the coordinates are installed.
• RS.superVectMu: the comparison of the fibre functor, in RS.SuperVect, with the four generator formulas RS.superVectMu_evenMap_ee and companions.
• RS.svEvenInl and its three companions: the four summands of a tensor product of super vector spaces.

The inverse comparison

The residue module is generated in even degree by the image of the unit, so the base change of a module is generated by the products m ⊗ 1, and the map that sends (m ⊗ n) ⊗ a to (m ⊗ a) ⊗ (n ⊗ 1) is well defined: an even scalar passes across either factor as its value at the point, and an odd scalar kills both sides.

noncomputable def RS.pointOne {S : SuperCommAlgebra} (P : SuperPoint S) : (SuperCommAlgebra.pointMod P).even

The unit of the residue module.

Equations

• RS.pointOne P = { down := 1 }

noncomputable def RS.pointScale {S : SuperCommAlgebra} (P : SuperPoint S) (X : Type u) [AddCommGroup X] [Module ℂ X] : X →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] X

Scaling by a residue class: a residue class acts on any complex vector space by its underlying complex number. The residue module being one dimensional in even degree, this describes every linear map out of it.

Equations

• RS.pointScale P X = { toFun := fun (x : X) => (↑ULift.moduleEquiv).smulRight x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.pointScale_apply {S : SuperCommAlgebra} (P : SuperPoint S) (X : Type u) [AddCommGroup X] [Module ℂ X] (x : X) (a : (SuperCommAlgebra.pointMod P).even) : ((pointScale P X) x) a = a.down • x

Scaling by a residue class, evaluated.

theorem RS.tmulEE_actEE_pointOne {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) (b : S.even) (m : M.even) : ((M.tmulEE (SuperCommAlgebra.pointMod P)) ((M.actEE b) m)) (pointOne P) = P.chi b • ((M.tmulEE (SuperCommAlgebra.pointMod P)) m) (pointOne P)

An even scalar crosses an even product with the unit as its value at the point.

theorem RS.tmulOE_actEO_pointOne {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) (b : S.even) (m : M.odd) : ((M.tmulOE (SuperCommAlgebra.pointMod P)) ((M.actEO b) m)) (pointOne P) = P.chi b • ((M.tmulOE (SuperCommAlgebra.pointMod P)) m) (pointOne P)

An even scalar crosses an odd product with the unit as its value at the point.

theorem RS.tmulEE_actOO_pointOne {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) (c : S.odd) (m : M.odd) : ((M.tmulEE (SuperCommAlgebra.pointMod P)) ((M.actOO c) m)) (pointOne P) = 0

An odd scalar kills the even products with the unit.

theorem RS.tmulOE_actOE_pointOne {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) (c : S.odd) (m : M.even) : ((M.tmulOE (SuperCommAlgebra.pointMod P)) ((M.actOE c) m)) (pointOne P) = 0

An odd scalar kills the odd products with the unit.

The comparison of the graded tensor product

The even part of the tensor product of two super modules is a quotient of the graded tensor product of their components, and likewise in odd degree. The quotient maps are the comparison between the tensor product of super vector spaces — which is the graded tensor product of the components — and the tensor product of super modules.

noncomputable def RS.gradedTensorEven {S : SuperCommAlgebra} (A B : S.Mod) : TensorProduct ℂ A.even B.even × TensorProduct ℂ A.odd B.odd →ₗ[ℂ] (A.tensor B).even

The graded comparison in even degree: the quotient map onto the even part of the tensor product.

Equations

• RS.gradedTensorEven A B = (A.balEven B).mkQ

noncomputable def RS.gradedTensorOdd {S : SuperCommAlgebra} (A B : S.Mod) : TensorProduct ℂ A.even B.odd × TensorProduct ℂ A.odd B.even →ₗ[ℂ] (A.tensor B).odd

The graded comparison in odd degree: the quotient map onto the odd part of the tensor product.

Equations

• RS.gradedTensorOdd A B = (A.balOdd B).mkQ

@[simp]

theorem RS.gradedTensorEven_ee {S : SuperCommAlgebra} (A B : S.Mod) (a : A.even) (b : B.even) : (gradedTensorEven A B) (a ⊗ₜ[ℂ] b, 0) = ((A.tmulEE B) a) b

The even comparison on an even-even product.

@[simp]

theorem RS.gradedTensorEven_oo {S : SuperCommAlgebra} (A B : S.Mod) (a : A.odd) (b : B.odd) : (gradedTensorEven A B) (0, a ⊗ₜ[ℂ] b) = ((A.tmulOO B) a) b

The even comparison on an odd-odd product.

@[simp]

theorem RS.gradedTensorOdd_eo {S : SuperCommAlgebra} (A B : S.Mod) (a : A.even) (b : B.odd) : (gradedTensorOdd A B) (a ⊗ₜ[ℂ] b, 0) = ((A.tmulEO B) a) b

The odd comparison on an even-odd product.

@[simp]

theorem RS.gradedTensorOdd_oe {S : SuperCommAlgebra} (A B : S.Mod) (a : A.odd) (b : B.even) : (gradedTensorOdd A B) (0, a ⊗ₜ[ℂ] b) = ((A.tmulOE B) a) b

The odd comparison on an odd-even product.

theorem RS.gradedTensorEven_naturality {S : SuperCommAlgebra} (A B : S.Mod) {A' B' : S.Mod} (uu : A ⟶ A') (vv : B ⟶ B') : (SuperCommAlgebra.Mod.tensorHom uu vv).evenMap ∘ₗ gradedTensorEven A B = gradedTensorEven A' B' ∘ₗ (TensorProduct.map uu.evenMap vv.evenMap).prodMap (TensorProduct.map uu.oddMap vv.oddMap)

The graded comparison is natural: the quotient maps commute with the tensor product of two morphisms.

theorem RS.gradedTensorOdd_naturality {S : SuperCommAlgebra} (A B : S.Mod) {A' B' : S.Mod} (uu : A ⟶ A') (vv : B ⟶ B') : (SuperCommAlgebra.Mod.tensorHom uu vv).oddMap ∘ₗ gradedTensorOdd A B = gradedTensorOdd A' B' ∘ₗ (TensorProduct.map uu.evenMap vv.oddMap).prodMap (TensorProduct.map uu.oddMap vv.evenMap)

The graded comparison is natural, in odd degree.

The inverse of the comparison

The comparison morphism is invertible: base change along a point is strong monoidal, not merely lax. The inverse sends (m ⊗ n) ⊗ a to (m ⊗ a) ⊗ (n ⊗ 1); it is well defined because an even scalar crosses both factors as its value at the point and an odd scalar kills both sides.

@[reducible, inline]

abbrev RS.basePairEven {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : Type u

The even part of the graded tensor product of the two base changes: the codomain of the inverse comparison in even degree.

Equations

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

@[reducible, inline]

abbrev RS.basePairOdd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : Type u

The odd part of the graded tensor product of the two base changes.

Equations

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

noncomputable def RS.baseNuFee {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : M.even →ₗ[ℂ] N.even →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairEven P M N

The even-even block of the inverse comparison.

Equations

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

noncomputable def RS.baseNuFoo {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairEven P M N

The odd-odd block of the inverse comparison.

Equations

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

noncomputable def RS.baseNuFeo {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairOdd P M N

The even-odd block of the inverse comparison.

Equations

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

noncomputable def RS.baseNuFoe {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairOdd P M N

The odd-even block of the inverse comparison.

Equations

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

@[simp]

theorem RS.baseNuFee_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.even) (n : N.even) (a : (SuperCommAlgebra.pointMod P).even) : (((baseNuFee P M N) m) n) a = a.down • (((M.tmulEE (SuperCommAlgebra.pointMod P)) m) (pointOne P) ⊗ₜ[ℂ] ((N.tmulEE (SuperCommAlgebra.pointMod P)) n) (pointOne P), 0)

The even-even block, evaluated.

@[simp]

theorem RS.baseNuFoo_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.odd) (n : N.odd) (a : (SuperCommAlgebra.pointMod P).even) : (((baseNuFoo P M N) m) n) a = a.down • (0, ((M.tmulOE (SuperCommAlgebra.pointMod P)) m) (pointOne P) ⊗ₜ[ℂ] ((N.tmulOE (SuperCommAlgebra.pointMod P)) n) (pointOne P))

The odd-odd block, evaluated.

@[simp]

theorem RS.baseNuFeo_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.even) (n : N.odd) (a : (SuperCommAlgebra.pointMod P).even) : (((baseNuFeo P M N) m) n) a = a.down • (((M.tmulEE (SuperCommAlgebra.pointMod P)) m) (pointOne P) ⊗ₜ[ℂ] ((N.tmulOE (SuperCommAlgebra.pointMod P)) n) (pointOne P), 0)

The even-odd block, evaluated.

@[simp]

theorem RS.baseNuFoe_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.odd) (n : N.even) (a : (SuperCommAlgebra.pointMod P).even) : (((baseNuFoe P M N) m) n) a = a.down • (0, ((M.tmulOE (SuperCommAlgebra.pointMod P)) m) (pointOne P) ⊗ₜ[ℂ] ((N.tmulEE (SuperCommAlgebra.pointMod P)) n) (pointOne P))

The odd-even block, evaluated.

The inner lift of the inverse comparison

theorem RS.baseNuFee_balanced_eee {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (m : M.even) (n : N.even) : ((baseNuFee P M N) ((M.actEE b) m)) n = ((baseNuFee P M N) m) ((N.actEE b) n)

Balancing of the even-even block against an even scalar.

theorem RS.baseNuFoo_balanced_eoo {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (m : M.odd) (n : N.odd) : ((baseNuFoo P M N) ((M.actEO b) m)) n = ((baseNuFoo P M N) m) ((N.actEO b) n)

Balancing of the odd-odd block against an even scalar.

theorem RS.baseNuFoo_balanced_oeo {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (m : M.even) (n : N.odd) : ((baseNuFoo P M N) ((M.actOE c) m)) n = ((baseNuFee P M N) m) ((N.actOO c) n)

Balancing of the blocks against an odd scalar, even-odd.

theorem RS.baseNuFee_balanced_ooe {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (m : M.odd) (n : N.even) : ((baseNuFee P M N) ((M.actOO c) m)) n = -((baseNuFoo P M N) m) ((N.actOE c) n)

Balancing of the blocks against an odd scalar, odd-even.

theorem RS.baseNuFeo_balanced_eeo {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (m : M.even) (n : N.odd) : ((baseNuFeo P M N) ((M.actEE b) m)) n = ((baseNuFeo P M N) m) ((N.actEO b) n)

Balancing of the even-odd block against an even scalar.

theorem RS.baseNuFoe_balanced_eoe {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (m : M.odd) (n : N.even) : ((baseNuFoe P M N) ((M.actEO b) m)) n = ((baseNuFoe P M N) m) ((N.actEE b) n)

Balancing of the odd-even block against an even scalar.

theorem RS.baseNuFoe_balanced_oee {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (m : M.even) (n : N.even) : ((baseNuFoe P M N) ((M.actOE c) m)) n = ((baseNuFeo P M N) m) ((N.actOE c) n)

Balancing of the odd blocks against an odd scalar, even-even.

theorem RS.baseNuFeo_balanced_ooo {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (m : M.odd) (n : N.odd) : ((baseNuFeo P M N) ((M.actOO c) m)) n = -((baseNuFoe P M N) m) ((N.actOO c) n)

Balancing of the odd blocks against an odd scalar, odd-odd.

noncomputable def RS.baseNuInnerEven {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : (M.tensor N).even →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairEven P M N

The inner lift of the inverse comparison, in even degree: the two even blocks descend to the tensor product of the two modules.

Equations

• RS.baseNuInnerEven P M N = M.liftEven N (RS.baseNuFee P M N) (RS.baseNuFoo P M N) ⋯ ⋯ ⋯ ⋯

noncomputable def RS.baseNuInnerOdd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : (M.tensor N).odd →ₗ[ℂ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ] basePairOdd P M N

The inner lift of the inverse comparison, in odd degree.

Equations

• RS.baseNuInnerOdd P M N = M.liftOdd N (RS.baseNuFeo P M N) (RS.baseNuFoe P M N) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.baseNuInnerEven_tmulEE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.even) (n : N.even) : (baseNuInnerEven P M N) (((M.tmulEE N) m) n) = ((baseNuFee P M N) m) n

The inner lift on even-even products.

@[simp]

theorem RS.baseNuInnerEven_tmulOO {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.odd) (n : N.odd) : (baseNuInnerEven P M N) (((M.tmulOO N) m) n) = ((baseNuFoo P M N) m) n

The inner lift on odd-odd products.

@[simp]

theorem RS.baseNuInnerOdd_tmulEO {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.even) (n : N.odd) : (baseNuInnerOdd P M N) (((M.tmulEO N) m) n) = ((baseNuFeo P M N) m) n

The inner lift on even-odd products.

@[simp]

theorem RS.baseNuInnerOdd_tmulOE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (m : M.odd) (n : N.even) : (baseNuInnerOdd P M N) (((M.tmulOE N) m) n) = ((baseNuFoe P M N) m) n

The inner lift on odd-even products.

The outer lift of the inverse comparison

@[simp]

theorem RS.pointMod_actEE_down {S : SuperCommAlgebra} (P : SuperPoint S) (b : S.even) (a : (SuperCommAlgebra.pointMod P).even) : (((SuperCommAlgebra.pointMod P).actEE b) a).down = P.chi b * a.down

The even action of the residue module, on coordinates.

theorem RS.baseNuInnerEven_actEE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (t : (M.tensor N).even) (a : (SuperCommAlgebra.pointMod P).even) : ((baseNuInnerEven P M N) (((M.tensor N).actEE b) t)) a = ((baseNuInnerEven P M N) t) (((SuperCommAlgebra.pointMod P).actEE b) a)

An even scalar crosses the inner lift in even degree.

theorem RS.baseNuInnerEven_actOO {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (t : (M.tensor N).odd) (a : (SuperCommAlgebra.pointMod P).even) : ((baseNuInnerEven P M N) (((M.tensor N).actOO c) t)) a = 0

An odd scalar kills the inner lift in even degree.

theorem RS.baseNuInnerOdd_actEO {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (b : S.even) (t : (M.tensor N).odd) (a : (SuperCommAlgebra.pointMod P).even) : ((baseNuInnerOdd P M N) (((M.tensor N).actEO b) t)) a = ((baseNuInnerOdd P M N) t) (((SuperCommAlgebra.pointMod P).actEE b) a)

An even scalar crosses the inner lift in odd degree.

theorem RS.baseNuInnerOdd_actOE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (c : S.odd) (t : (M.tensor N).even) (a : (SuperCommAlgebra.pointMod P).even) : ((baseNuInnerOdd P M N) (((M.tensor N).actOE c) t)) a = 0

An odd scalar kills the inner lift in odd degree.

noncomputable def RS.baseNuEven {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even →ₗ[ℂ] basePairEven P M N

The inverse comparison in even degree.

Equations

• RS.baseNuEven P M N = (M.tensor N).liftEven (RS.SuperCommAlgebra.pointMod P) (RS.baseNuInnerEven P M N) 0 ⋯ ⋯ ⋯ ⋯

noncomputable def RS.baseNuOdd {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd →ₗ[ℂ] basePairOdd P M N

The inverse comparison in odd degree.

Equations

• RS.baseNuOdd P M N = (M.tensor N).liftOdd (RS.SuperCommAlgebra.pointMod P) 0 (RS.baseNuInnerOdd P M N) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.baseNuEven_tmulEE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (t : (M.tensor N).even) (a : (SuperCommAlgebra.pointMod P).even) : (baseNuEven P M N) ((((M.tensor N).tmulEE (SuperCommAlgebra.pointMod P)) t) a) = ((baseNuInnerEven P M N) t) a

The inverse comparison in even degree, on generators.

@[simp]

theorem RS.baseNuOdd_tmulOE {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} (t : (M.tensor N).odd) (a : (SuperCommAlgebra.pointMod P).even) : (baseNuOdd P M N) ((((M.tensor N).tmulOE (SuperCommAlgebra.pointMod P)) t) a) = ((baseNuInnerOdd P M N) t) a

The inverse comparison in odd degree, on generators.

The comparison in super vector spaces

noncomputable def RS.superVectMuEvenRaw {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : 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 →ₗ[ℂ] ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).even

The comparison morphism in super vector spaces, in even degree, before the coordinates are installed.

Equations

• RS.superVectMuEvenRaw P M N = (RS.pointBaseMu P M N).evenMap ∘ₗ RS.gradedTensorEven (M.tensor (RS.SuperCommAlgebra.pointMod P)) (N.tensor (RS.SuperCommAlgebra.pointMod P))

noncomputable def RS.superVectMuOddRaw {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) : 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 →ₗ[ℂ] ((M.tensor N).tensor (SuperCommAlgebra.pointMod P)).odd

The comparison morphism in super vector spaces, in odd degree, before the coordinates are installed.

Equations

• RS.superVectMuOddRaw P M N = (RS.pointBaseMu P M N).oddMap ∘ₗ RS.gradedTensorOdd (M.tensor (RS.SuperCommAlgebra.pointMod P)) (N.tensor (RS.SuperCommAlgebra.pointMod P))

noncomputable def RS.superVectPairEvenEquiv {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] : basePairEven P M N ≃ₗ[ℂ] (CategoryTheory.MonoidalCategoryStruct.tensorObj (toSuperVect P M) (toSuperVect P N)).even

The coordinates on the even part of the tensor product of the two base changes.

Equations

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

noncomputable def RS.superVectPairOddEquiv {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] : basePairOdd P M N ≃ₗ[ℂ] (CategoryTheory.MonoidalCategoryStruct.tensorObj (toSuperVect P M) (toSuperVect P N)).odd

The coordinates on the odd part of the tensor product of the two base changes.

Equations

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

noncomputable def RS.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.MonoidalCategoryStruct.tensorObj (toSuperVect P M) (toSuperVect P N) ⟶ toSuperVect P (M.tensor N)

The monoidal comparison of the fibre functor: the tensor product of the base changes maps to the base change of the tensor product. It is the raw comparison, read in the coordinates that RS.toSuperVect installs.

Equations

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

The four summands of a tensor product of super vector spaces

The even part of V ⊗ W is a sum of two blocks and so is the odd part. Naming the four inclusions keeps every generator below at its structural type, which is what lets the rewriting see through the tensor product of super vector spaces.

def RS.svEvenInl {V W : SuperVect} (t : TensorProduct ℂ V.even W.even) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).even

The even-even block of the even part.

Equations

• RS.svEvenInl t = (t, 0)

def RS.svEvenInr {V W : SuperVect} (t : TensorProduct ℂ V.odd W.odd) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).even

The odd-odd block of the even part.

Equations

• RS.svEvenInr t = (0, t)

def RS.svOddInl {V W : SuperVect} (t : TensorProduct ℂ V.even W.odd) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).odd

The even-odd block of the odd part.

Equations

• RS.svOddInl t = (t, 0)

def RS.svOddInr {V W : SuperVect} (t : TensorProduct ℂ V.odd W.even) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).odd

The odd-even block of the odd part.

Equations

• RS.svOddInr t = (0, t)

theorem RS.svEvenInr_zero {V W : SuperVect} : svEvenInr 0 = 0

The odd-odd block of zero vanishes.

theorem RS.svOddInl_zero {V W : SuperVect} : svOddInl 0 = 0

The even-odd block of zero vanishes.

theorem RS.svOddInr_zero {V W : SuperVect} : svOddInr 0 = 0

The odd-even block of zero vanishes.

The comparison on generators of the tensor product

theorem RS.superVectMu_evenMap_ee {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] (x : (toSuperVect P M).even) (y : (toSuperVect P N).even) : (superVectMu P M N).evenMap (svEvenInl (x ⊗ₜ[ℂ] y)) = (toSuperVectEvenEquiv P (M.tensor N)) ((pointBaseMu P M N).evenMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulEE (N.tensor (SuperCommAlgebra.pointMod P))) ((toSuperVectEvenEquiv P M).symm x)) ((toSuperVectEvenEquiv P N).symm y)))

The comparison on an even-even generator.

theorem RS.superVectMu_evenMap_oo {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] (x : (toSuperVect P M).odd) (y : (toSuperVect P N).odd) : (superVectMu P M N).evenMap (svEvenInr (x ⊗ₜ[ℂ] y)) = (toSuperVectEvenEquiv P (M.tensor N)) ((pointBaseMu P M N).evenMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulOO (N.tensor (SuperCommAlgebra.pointMod P))) ((toSuperVectOddEquiv P M).symm x)) ((toSuperVectOddEquiv P N).symm y)))

The comparison on an odd-odd generator.

theorem RS.superVectMu_oddMap_eo {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] (x : (toSuperVect P M).even) (y : (toSuperVect P N).odd) : (superVectMu P M N).oddMap (svOddInl (x ⊗ₜ[ℂ] y)) = (toSuperVectOddEquiv P (M.tensor N)) ((pointBaseMu P M N).oddMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulEO (N.tensor (SuperCommAlgebra.pointMod P))) ((toSuperVectEvenEquiv P M).symm x)) ((toSuperVectOddEquiv P N).symm y)))

The comparison on an even-odd generator.

theorem RS.superVectMu_oddMap_oe {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] (x : (toSuperVect P M).odd) (y : (toSuperVect P N).even) : (superVectMu P M N).oddMap (svOddInr (x ⊗ₜ[ℂ] y)) = (toSuperVectOddEquiv P (M.tensor N)) ((pointBaseMu P M N).oddMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulOE (N.tensor (SuperCommAlgebra.pointMod P))) ((toSuperVectOddEquiv P M).symm x)) ((toSuperVectEvenEquiv P N).symm y)))

The comparison on an odd-even generator.