Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.PointMonoidal.Residue

The residue algebra of a complex point #

The residue module of a ℂ-point of a super-commutative algebra S has a copy of ℂ for its even part and a vanishing odd part, and the point makes S act through its value. Multiplication of complex numbers therefore descends to a morphism k ⊗ k ⟶ k of super modules, and the point itself to a morphism from the unit module, so the residue module is a commutative monoid object. Super modules over S are symmetric monoidal, so the middle-four interchange followed by that multiplication is a comparison (M ⊗ k) ⊗ (N ⊗ k) ⟶ (M ⊗ N) ⊗ k, natural in both variables, and the monoid laws are exactly what makes it lax monoidal and braided. The comparison is carried down to super vector spaces in Comparison.lean.

Contents #

RS.pointMulHom, RS.pointUnitHom: the residue module as a commutative algebra over the base, with its associativity RS.pointMulHom_assoc, its two unit laws and its commutativity RS.pointMulHom_comm.
RS.pointBaseMu, RS.pointBaseEps: the comparison morphisms over the algebra, with RS.pointBaseMu_naturality and the four generator formulas RS.pointBaseMu_evenMap_ee and companions.
RS.pointBaseMu_associativity, RS.pointBaseMu_left_unitality, RS.pointBaseMu_right_unitality: the three coherence laws of the comparison over the algebra — base change over the algebra is lax monoidal, and the multiplication of the residue module is what makes it so.
RS.pointBaseMu_braiding: the comparison over the algebra intertwines the braidings, the residue factor contributing nothing because its multiplication is commutative.
RS.modAssociator_hom and its companions: the structural morphisms of the category of super modules, in the form the generator computations consume.

The residue module is a commutative algebra #

instance RS.pointMod_odd_subsingleton {S : SuperCommAlgebra} (P : SuperPoint S) :

Subsingleton (SuperCommAlgebra.pointMod P).odd

The odd part of the residue module has one element.

theorem RS.pointMod_odd_eq_zero {S : SuperCommAlgebra} (P : SuperPoint S) (v : (SuperCommAlgebra.pointMod P).odd) :

v = 0

An element of the odd part of the residue module vanishes.

theorem RS.pointMod_actEE {S : SuperCommAlgebra} (P : SuperPoint S) (x : S.even) (c : (SuperCommAlgebra.pointMod P).even) :

((SuperCommAlgebra.pointMod P).actEE x) c = { down := P.chi x * c.down }

The even action on the residue module is multiplication by the value of the point.

theorem RS.pointMod_actOE {S : SuperCommAlgebra} (P : SuperPoint S) (u : S.odd) (c : (SuperCommAlgebra.pointMod P).even) :

((SuperCommAlgebra.pointMod P).actOE u) c = 0

The odd action on the even part of the residue module vanishes.

theorem RS.pointMod_actOO {S : SuperCommAlgebra} (P : SuperPoint S) (u : S.odd) (v : (SuperCommAlgebra.pointMod P).odd) :

((SuperCommAlgebra.pointMod P).actOO u) v = 0

The odd action on the odd part of the residue module vanishes.

noncomputable def RS.pointMulLin {S : SuperCommAlgebra} (P : SuperPoint S) :

(SuperCommAlgebra.pointMod P).even →ₗ[ℂ ] (SuperCommAlgebra.pointMod P).even →ₗ[ℂ ] (SuperCommAlgebra.pointMod P).even

The multiplication of the residue module, on even parts: the residue module is a copy of ℂ in even degree, and this is the multiplication of ℂ.

Equations

RS.pointMulLin P = LinearMap.mk₂ ℂ (fun (a b : (RS.SuperCommAlgebra.pointMod P).even) => { down := a.down * b.down }) ⋯ ⋯ ⋯ ⋯

Instances For

@[simp]

theorem RS.pointMulLin_apply {S : SuperCommAlgebra} (P : SuperPoint S) (a b : (SuperCommAlgebra.pointMod P).even) :

((pointMulLin P) a) b = { down := a.down * b.down }

The multiplication of the residue module, evaluated.

noncomputable def RS.pointMulData {S : SuperCommAlgebra} (P : SuperPoint S) :

(SuperCommAlgebra.pointMod P).TensorData (SuperCommAlgebra.pointMod P) (SuperCommAlgebra.pointMod P)

The data of the multiplication of the residue module as a morphism out of the tensor square: the even-even block is the multiplication of ℂ and the three remaining blocks vanish, the odd part of the residue module being zero.

Equations

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

Instances For

noncomputable def RS.pointMulHom {S : SuperCommAlgebra} (P : SuperPoint S) :

(SuperCommAlgebra.pointMod P).tensor (SuperCommAlgebra.pointMod P) ⟶ SuperCommAlgebra.pointMod P

The multiplication of the residue module, as a morphism of super modules out of its tensor square.

Equations

RS.pointMulHom P = RS.SuperCommAlgebra.Mod.mkHom (RS.pointMulData P)

Instances For

@[simp]

theorem RS.pointMulHom_evenMap_tmulEE {S : SuperCommAlgebra} (P : SuperPoint S) (a b : (SuperCommAlgebra.pointMod P).even) :

(pointMulHom P).evenMap ((((SuperCommAlgebra.pointMod P).tmulEE (SuperCommAlgebra.pointMod P)) a) b) = { down := a.down * b.down }

The multiplication on even-even products.

noncomputable def RS.pointUnitHom {S : SuperCommAlgebra} (P : SuperPoint S) :

S.unitMod ⟶ SuperCommAlgebra.pointMod P

The unit of the residue module: the point itself, read as a morphism from the algebra.

Equations

RS.pointUnitHom P = { evenMap := ↑ULift.moduleEquiv.symm ∘ₗ P.chi.toLinearMap, oddMap := 0, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

Instances For

@[simp]

theorem RS.pointUnitHom_evenMap {S : SuperCommAlgebra} (P : SuperPoint S) (x : S.even) :

(pointUnitHom P).evenMap x = { down := P.chi x }

The unit of the residue module, evaluated.

instance RS.finiteDimensional_unitMod_tensor_point_even {S : SuperCommAlgebra} (P : SuperPoint S) :

FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).even

The base change of the unit module is finite dimensional in even degree: the left unitor identifies it with the residue module.

instance RS.finiteDimensional_unitMod_tensor_point_odd {S : SuperCommAlgebra} (P : SuperPoint S) :

FiniteDimensional ℂ (S.unitMod.tensor (SuperCommAlgebra.pointMod P)).odd

The base change of the unit module is finite dimensional in odd degree.

The comparison over the algebra #

Base change is the functor M ↦ M ⊗ k for k the residue module of the point. The residue module is a commutative algebra, so the usual middle-four interchange followed by its multiplication is a comparison morphism (M ⊗ k) ⊗ (N ⊗ k) ⟶ (M ⊗ N) ⊗ k.

noncomputable def RS.pointBaseMu {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) :

(M.tensor (SuperCommAlgebra.pointMod P)).tensor (N.tensor (SuperCommAlgebra.pointMod P)) ⟶ (M.tensor N).tensor (SuperCommAlgebra.pointMod P)

The comparison morphism of base change, over the algebra: interchange the middle two factors and multiply the two copies of the residue module.

Equations

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

Instances For

noncomputable def RS.pointBaseEps {S : SuperCommAlgebra} (P : SuperPoint S) :

S.unitMod ⟶ S.unitMod.tensor (SuperCommAlgebra.pointMod P)

The unit of base change, over the algebra: the point read as a morphism from the unit, followed by the inverse left unitor.

Equations

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

Instances For

The comparison over the algebra is natural in both variables: this is naturality of the middle-four interchange.

The comparison over the algebra, on generators #

theorem RS.modAssociator_hom {S : SuperCommAlgebra} (X Y Z : S.Mod) :

(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = X.assocHom Y Z

The monoidal associator of the super modules is the explicit associator.

theorem RS.modAssociator_inv {S : SuperCommAlgebra} (X Y Z : S.Mod) :

(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = X.assocInv Y Z

The inverse associator of the super modules is explicit.

theorem RS.modBraiding_hom {S : SuperCommAlgebra} (X Y : S.Mod) :

(β_ X Y).hom = X.braidingHom Y

The braiding of the super modules is the Koszul swap.

theorem RS.modWhiskerLeft {S : SuperCommAlgebra} (X : S.Mod) {Y Z : S.Mod} (f : Y ⟶ Z) :

CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = SuperCommAlgebra.Mod.tensorHom (CategoryTheory.CategoryStruct.id X) f

Left whiskering of super modules is a tensor product of morphisms.

theorem RS.modWhiskerRight {S : SuperCommAlgebra} {Y Z : S.Mod} (f : Y ⟶ Z) (X : S.Mod) :

CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = SuperCommAlgebra.Mod.tensorHom f (CategoryTheory.CategoryStruct.id X)

Right whiskering of super modules is a tensor product of morphisms.

theorem RS.modTensorObj {S : SuperCommAlgebra} (X Y : S.Mod) :

CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = X.tensor Y

The monoidal tensor product of super modules is the balanced tensor product.

theorem RS.modLeftUnitor_hom {S : SuperCommAlgebra} (X : S.Mod) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = X.leftUnitorHom

The left unitor of the super modules is explicit.

theorem RS.modRightUnitor_hom {S : SuperCommAlgebra} (X : S.Mod) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = X.rightUnitorHom

The right unitor of the super modules is explicit.

theorem RS.modTensorUnit {S : SuperCommAlgebra} :

CategoryTheory.MonoidalCategoryStruct.tensorUnit S.Mod = S.unitMod

The monoidal unit of the super modules is the algebra.

theorem RS.pointBaseMu_evenMap_ee {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (m : M.even) (a : (SuperCommAlgebra.pointMod P).even) (n : N.even) (b : (SuperCommAlgebra.pointMod P).even) :

(pointBaseMu P M N).evenMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulEE (N.tensor (SuperCommAlgebra.pointMod P))) (((M.tmulEE (SuperCommAlgebra.pointMod P)) m) a)) (((N.tmulEE (SuperCommAlgebra.pointMod P)) n) b)) = (((M.tensor N).tmulEE (SuperCommAlgebra.pointMod P)) (((M.tmulEE N) m) n)) { down := a.down * b.down }

The comparison over the algebra on even-even generators.

theorem RS.pointBaseMu_evenMap_oo {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (m : M.odd) (a : (SuperCommAlgebra.pointMod P).even) (n : N.odd) (b : (SuperCommAlgebra.pointMod P).even) :

(pointBaseMu P M N).evenMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulOO (N.tensor (SuperCommAlgebra.pointMod P))) (((M.tmulOE (SuperCommAlgebra.pointMod P)) m) a)) (((N.tmulOE (SuperCommAlgebra.pointMod P)) n) b)) = (((M.tensor N).tmulEE (SuperCommAlgebra.pointMod P)) (((M.tmulOO N) m) n)) { down := a.down * b.down }

The comparison over the algebra on odd-odd generators.

theorem RS.pointBaseMu_oddMap_eo {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (m : M.even) (a : (SuperCommAlgebra.pointMod P).even) (n : N.odd) (b : (SuperCommAlgebra.pointMod P).even) :

(pointBaseMu P M N).oddMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulEO (N.tensor (SuperCommAlgebra.pointMod P))) (((M.tmulEE (SuperCommAlgebra.pointMod P)) m) a)) (((N.tmulOE (SuperCommAlgebra.pointMod P)) n) b)) = (((M.tensor N).tmulOE (SuperCommAlgebra.pointMod P)) (((M.tmulEO N) m) n)) { down := a.down * b.down }

The comparison over the algebra on even-odd generators.

theorem RS.pointBaseMu_oddMap_oe {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) (m : M.odd) (a : (SuperCommAlgebra.pointMod P).even) (n : N.even) (b : (SuperCommAlgebra.pointMod P).even) :

(pointBaseMu P M N).oddMap ((((M.tensor (SuperCommAlgebra.pointMod P)).tmulOE (N.tensor (SuperCommAlgebra.pointMod P))) (((M.tmulOE (SuperCommAlgebra.pointMod P)) m) a)) (((N.tmulEE (SuperCommAlgebra.pointMod P)) n) b)) = (((M.tensor N).tmulOE (SuperCommAlgebra.pointMod P)) (((M.tmulOE N) m) n)) { down := a.down * b.down }

The comparison over the algebra on odd-even generators.

The residue module is a commutative monoid object #

The three monoid laws and commutativity, in the form the lax structure of base change consumes. Every law is an identity of complex numbers in the even-even-even block, and every other block lands in the odd part of the residue module, which vanishes.

The multiplication of the residue module is associative.

theorem RS.pointMulHom_left_unit {S : SuperCommAlgebra} (P : SuperPoint S) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pointUnitHom P) (SuperCommAlgebra.pointMod P)) (pointMulHom P) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (SuperCommAlgebra.pointMod P)).hom

The point is a left unit for the multiplication of the residue module.

theorem RS.pointMulHom_right_unit {S : SuperCommAlgebra} (P : SuperPoint S) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (SuperCommAlgebra.pointMod P) (pointUnitHom P)) (pointMulHom P) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (SuperCommAlgebra.pointMod P)).hom

The point is a right unit for the multiplication of the residue module.

theorem RS.pointMulHom_comm {S : SuperCommAlgebra} (P : SuperPoint S) :

CategoryTheory.CategoryStruct.comp (β_ (SuperCommAlgebra.pointMod P) (SuperCommAlgebra.pointMod P)).hom (pointMulHom P) = pointMulHom P

The multiplication of the residue module is commutative.

Base change over the algebra is lax monoidal #

theorem RS.pointBaseMu_associativity {S : SuperCommAlgebra} (P : SuperPoint S) (M N Q : S.Mod) :

Associativity of the comparison over the algebra.

Left unitality of the comparison over the algebra.

Right unitality of the comparison over the algebra.

theorem RS.pointBaseMu_braiding {S : SuperCommAlgebra} (P : SuperPoint S) (M N : S.Mod) :

CategoryTheory.CategoryStruct.comp (pointBaseMu P M N) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M N).hom (SuperCommAlgebra.pointMod P)) = CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj M (SuperCommAlgebra.pointMod P)) (CategoryTheory.MonoidalCategoryStruct.tensorObj N (SuperCommAlgebra.pointMod P))).hom (pointBaseMu P N M)

The comparison over the algebra intertwines the braidings. The interchange does so by RS.tensorμ_braiding, and the residue factor by commutativity of its multiplication.