Base change of a free super module to a complex point

Tensoring a super module with the residue module of a complex point (RS.SuperCommAlgebra.pointMod) is base change along that point. This file computes the base change of a free super module of rank (p | q) and records that the answer is a finite-dimensional super vector space of the same rank.

The computation is pure additivity. Tensoring on the right by a fixed module is an additive functor, so it carries a finite biproduct to a finite biproduct; the two summands of a free module are the unit and its parity shift, and tensoring either of them with the residue module is already known — the unit case is the left unitor and the shifted case is RS.SuperCommAlgebra.Mod.shiftUnitTensor. What is left is a biproduct of p copies of the residue module and q copies of its parity shift, whose even part has dimension p and whose odd part has dimension q.

Finite-dimensionality is read off through the two component functors to complex vector spaces. Taking the even part, or the odd part, of a super module is an additive functor to ModuleCat ℂ, so it turns the abstract biproduct of super modules into the concrete product of the component spaces, and a finite product of finite-dimensional spaces is finite-dimensional.

Contents

• RS.SuperCommAlgebra.Mod.evenModFunctor, oddModFunctor: the two component functors, and their additivity.
• RS.SuperCommAlgebra.Mod.evenBiproductEquiv, oddBiproductEquiv: the component of a finite biproduct is the product of the components.
• RS.SuperCommAlgebra.Mod.tensorRightFunctor: tensoring on the right by a fixed module, as an additive functor.
• RS.unitTensorPoint, RS.shiftTensorPoint: base change of the unit and of its parity shift.
• RS.freeTensorPoint: base change of a free module of rank (p | q).
• RS.finiteDimensional_even_of_free, RS.finiteDimensional_odd_of_free: finite-dimensionality of the base change of a free module.
• RS.finrank_even_of_free, RS.finrank_odd_of_free: the two dimensions are p and q.
• RS.toSuperVect: the base change packaged as a super vector space, with RS.toSuperVectEvenEquiv, toSuperVectOddEquiv and the two explicit coordinate equivalences RS.freeEvenEquivFin, freeOddEquivFin.

The two component functors

noncomputable def RS.SuperCommAlgebra.Mod.evenModFunctor (S : SuperCommAlgebra) : CategoryTheory.Functor S.Mod (ModuleCat ℂ)

The even component as a functor to complex vector spaces.

Equations

• RS.SuperCommAlgebra.Mod.evenModFunctor S = { obj := fun (M : S.Mod) => ↧M.even, map := fun {X Y : S.Mod} (f : X ⟶ Y) => ModuleCat.ofHom f.evenMap, map_id := ⋯, map_comp := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.oddModFunctor (S : SuperCommAlgebra) : CategoryTheory.Functor S.Mod (ModuleCat ℂ)

The odd component as a functor to complex vector spaces.

Equations

• RS.SuperCommAlgebra.Mod.oddModFunctor S = { obj := fun (M : S.Mod) => ↧M.odd, map := fun {X Y : S.Mod} (f : X ⟶ Y) => ModuleCat.ofHom f.oddMap, map_id := ⋯, map_comp := ⋯ }

instance RS.SuperCommAlgebra.Mod.evenModFunctor_additive (S : SuperCommAlgebra) : (evenModFunctor S).Additive

The even component functor is additive.

instance RS.SuperCommAlgebra.Mod.oddModFunctor_additive (S : SuperCommAlgebra) : (oddModFunctor S).Additive

The odd component functor is additive.

noncomputable def RS.SuperCommAlgebra.Mod.evenEquiv {S : SuperCommAlgebra} {M N : S.Mod} (e : M ≅ N) : M.even ≃ₗ[ℂ] N.even

An isomorphism of super modules is a linear equivalence on even components.

Equations

• RS.SuperCommAlgebra.Mod.evenEquiv e = ((RS.SuperCommAlgebra.Mod.evenModFunctor S).mapIso e).toLinearEquiv

noncomputable def RS.SuperCommAlgebra.Mod.oddEquiv {S : SuperCommAlgebra} {M N : S.Mod} (e : M ≅ N) : M.odd ≃ₗ[ℂ] N.odd

An isomorphism of super modules is a linear equivalence on odd components.

Equations

• RS.SuperCommAlgebra.Mod.oddEquiv e = ((RS.SuperCommAlgebra.Mod.oddModFunctor S).mapIso e).toLinearEquiv

Components of a finite biproduct

noncomputable def RS.SuperCommAlgebra.Mod.evenBiproductEquiv {S : SuperCommAlgebra} {J : Type} [Fintype J] (g : J → S.Mod) : (⨁ g).even ≃ₗ[ℂ] (j : J) → (g j).even

The even component of a finite biproduct is the product of the even components.

Equations

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

noncomputable def RS.SuperCommAlgebra.Mod.oddBiproductEquiv {S : SuperCommAlgebra} {J : Type} [Fintype J] (g : J → S.Mod) : (⨁ g).odd ≃ₗ[ℂ] (j : J) → (g j).odd

The odd component of a finite biproduct is the product of the odd components.

Equations

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

Tensoring on the right

noncomputable def RS.SuperCommAlgebra.Mod.tensorRightFunctor {S : SuperCommAlgebra} (N : S.Mod) : CategoryTheory.Functor S.Mod S.Mod

Tensoring on the right by a fixed module, as a functor.

Equations

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

@[simp]

theorem RS.SuperCommAlgebra.Mod.tensorRightFunctor_obj {S : SuperCommAlgebra} (N M : S.Mod) : N.tensorRightFunctor.obj M = M.tensor N

instance RS.SuperCommAlgebra.Mod.tensorRightFunctor_additive {S : SuperCommAlgebra} (N : S.Mod) : N.tensorRightFunctor.Additive

Tensoring on the right by a fixed module is additive: this is additivity of the tensor product in the left variable.

Base change of the two free generators

noncomputable def RS.unitTensorPoint {S : SuperCommAlgebra} (P : SuperPoint S) : S.unitMod.tensor (SuperCommAlgebra.pointMod P) ≅ SuperCommAlgebra.pointMod P

Base change of the unit module: tensoring the unit with the residue module of a point returns the residue module. This is the left unitor.

Equations

• RS.unitTensorPoint P = (RS.SuperCommAlgebra.pointMod P).leftUnitor

noncomputable def RS.shiftTensorPoint {S : SuperCommAlgebra} (P : SuperPoint S) : S.unitMod.shift.tensor (SuperCommAlgebra.pointMod P) ≅ (SuperCommAlgebra.pointMod P).shift

Base change of the shifted unit module: tensoring the parity shift of the unit with the residue module of a point returns the parity shift of the residue module.

Equations

• RS.shiftTensorPoint P = (RS.SuperCommAlgebra.pointMod P).shiftUnitTensor

Base change of a free module

noncomputable def RS.freeTensorPoint {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : (⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i).tensor (SuperCommAlgebra.pointMod P) ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => SuperCommAlgebra.pointMod P) (fun (x : Fin q) => (SuperCommAlgebra.pointMod P).shift) i

Base change of a free super module of rank (p | q): the result is the biproduct of p copies of the residue module and q copies of its parity shift. Tensoring on the right is additive, so it carries the defining biproduct across, and the two summands are handled by RS.unitTensorPoint and RS.shiftTensorPoint.

Equations

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

The residue module is one-dimensional in even degree

instance RS.finiteDimensional_pointMod_even {S : SuperCommAlgebra} (P : SuperPoint S) : FiniteDimensional ℂ (SuperCommAlgebra.pointMod P).even

The even part of the residue module of a point is finite-dimensional: it is a copy of the complex numbers.

instance RS.finiteDimensional_pointMod_odd {S : SuperCommAlgebra} (P : SuperPoint S) : FiniteDimensional ℂ (SuperCommAlgebra.pointMod P).odd

The odd part of the residue module of a point is finite-dimensional: it is zero.

theorem RS.finrank_pointMod_even {S : SuperCommAlgebra} (P : SuperPoint S) : Module.finrank ℂ (SuperCommAlgebra.pointMod P).even = 1

The even part of the residue module of a point is one-dimensional.

theorem RS.finrank_pointMod_odd {S : SuperCommAlgebra} (P : SuperPoint S) : Module.finrank ℂ (SuperCommAlgebra.pointMod P).odd = 0

The odd part of the residue module of a point is zero.

The biproduct of residue modules

noncomputable def RS.residueShape {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : Fin p ⊕ Fin q → S.Mod

The family of summands of the base change of a free module of rank (p | q): p copies of the residue module of the point and q copies of its parity shift.

Equations

• RS.residueShape P p q i = Sum.elim (fun (x : Fin p) => RS.SuperCommAlgebra.pointMod P) (fun (x : Fin q) => (RS.SuperCommAlgebra.pointMod P).shift) i

instance RS.finiteDimensional_residueShape_even {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (i : Fin p ⊕ Fin q) : FiniteDimensional ℂ (residueShape P p q i).even

Every summand has finite-dimensional even part.

instance RS.finiteDimensional_residueShape_odd {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (i : Fin p ⊕ Fin q) : FiniteDimensional ℂ (residueShape P p q i).odd

Every summand has finite-dimensional odd part.

instance RS.finiteDimensional_biproduct_even {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : FiniteDimensional ℂ (⨁ residueShape P p q).even

The even part of the biproduct of residue modules is finite-dimensional.

instance RS.finiteDimensional_biproduct_odd {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : FiniteDimensional ℂ (⨁ residueShape P p q).odd

The odd part of the biproduct of residue modules is finite-dimensional.

theorem RS.finrank_biproduct_even {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : Module.finrank ℂ (⨁ residueShape P p q).even = p

The even part of the biproduct of residue modules has dimension p.

theorem RS.finrank_biproduct_odd {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) : Module.finrank ℂ (⨁ residueShape P p q).odd = q

The odd part of the biproduct of residue modules has dimension q.

Base change of a module known to be free

noncomputable def RS.tensorPointIso {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : M.tensor (SuperCommAlgebra.pointMod P) ≅ ⨁ residueShape P p q

The base change of a free module of rank (p | q), in the form used below: a module isomorphic to a free module of rank (p | q) has base change the biproduct of residue modules.

Equations

• RS.tensorPointIso P p q M e = (RS.SuperCommAlgebra.pointMod P).tensorRightFunctor.mapIso e ≪≫ RS.freeTensorPoint P p q

theorem RS.finiteDimensional_even_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even

The base change of a free module of rank (p | q) has finite-dimensional even part.

theorem RS.finiteDimensional_odd_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd

The base change of a free module of rank (p | q) has finite-dimensional odd part.

theorem RS.finrank_even_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even = p

The even dimension of the base change of a free module of rank (p | q) is p.

theorem RS.finrank_odd_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd = q

The odd dimension of the base change of a free module of rank (p | q) is q.

The super vector space of a base change

noncomputable def RS.toSuperVect {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) : SuperVect

The base change of a super module along a point, packaged as a super vector space. The components of a super module live in an arbitrary universe, while RS.SuperVect asks for types in Type, so the packaging is by coordinates: each component is replaced by the space of coordinate vectors of its dimension. The two equivalences RS.toSuperVectEvenEquiv and RS.toSuperVectOddEquiv identify the components of the base change with the components of this super vector space.

Equations

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

@[simp]

theorem RS.toSuperVect_even {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) : (toSuperVect P M).even = (Fin (Module.finrank ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even) → ℂ)

@[simp]

theorem RS.toSuperVect_odd {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) : (toSuperVect P M).odd = (Fin (Module.finrank ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd) → ℂ)

@[irreducible]

noncomputable def RS.toSuperVectEvenEquiv {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] : (M.tensor (SuperCommAlgebra.pointMod P)).even ≃ₗ[ℂ] (toSuperVect P M).even

The even part of the base change is the even part of the super vector space attached to it.

Equations

• RS.toSuperVectEvenEquiv P M = (Module.finBasis ℂ (M.tensor (RS.SuperCommAlgebra.pointMod P)).even).equivFun

@[irreducible]

noncomputable def RS.toSuperVectOddEquiv {S : SuperCommAlgebra} (P : SuperPoint S) (M : S.Mod) [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] : (M.tensor (SuperCommAlgebra.pointMod P)).odd ≃ₗ[ℂ] (toSuperVect P M).odd

The odd part of the base change is the odd part of the super vector space attached to it.

Equations

• RS.toSuperVectOddEquiv P M = (Module.finBasis ℂ (M.tensor (RS.SuperCommAlgebra.pointMod P)).odd).equivFun

Explicit coordinates in the free case

noncomputable def RS.freeEvenEquivFin {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : (M.tensor (SuperCommAlgebra.pointMod P)).even ≃ₗ[ℂ] Fin p → ℂ

Coordinates on the even part: the base change of a free module of rank (p | q) has even part the space of p-tuples of complex numbers.

Equations

• RS.freeEvenEquivFin P p q M e = (Module.finBasisOfFinrankEq ℂ (M.tensor (RS.SuperCommAlgebra.pointMod P)).even ⋯).equivFun

noncomputable def RS.freeOddEquivFin {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : (M.tensor (SuperCommAlgebra.pointMod P)).odd ≃ₗ[ℂ] Fin q → ℂ

Coordinates on the odd part: the base change of a free module of rank (p | q) has odd part the space of q-tuples of complex numbers.

Equations

• RS.freeOddEquivFin P p q M e = (Module.finBasisOfFinrankEq ℂ (M.tensor (RS.SuperCommAlgebra.pointMod P)).odd ⋯).equivFun

theorem RS.finrank_toSuperVect_even_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ (toSuperVect P M).even = p

The super vector space of the base change of a free module of rank (p | q) has even part of dimension p.

theorem RS.finrank_toSuperVect_odd_of_free {S : SuperCommAlgebra} (P : SuperPoint S) (p q : ℕ) (M : S.Mod) (e : M ≅ ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => S.unitMod) (fun (x : Fin q) => S.unitMod.shift) i) : Module.finrank ℂ (toSuperVect P M).odd = q

The super vector space of the base change of a free module of rank (p | q) has odd part of dimension q.

Sealing the coordinates

The two coordinate equivalences are chosen bases, and nothing below should depend on how they were chosen. Sealing them keeps simp from unfolding a base change into a composite of Module.finBasis coordinates, which is what makes the coherence laws of the base change unmanageable downstream.