The comparison map of Deligne's (2.11.1) #
For two module objects M, N over a commutative monoid object
R of a symmetric ℂ-linear monoidal category carrying an odd line
L, the Γ-modules of M and of N may be tensored over the
Γ-algebra of R (RS.SuperCommAlgebra.Mod.tensor), and the
relative tensor product RS.modTensor of the module objects has a
Γ-module of its own. This file builds the comparison map between
them, RS.gammaPairComparison, as a morphism of super modules.
Everything rests on one ungraded operation, RS.gpair: the
pairing (m ⊗ₘ n) ≫ π of a morphism into M against a morphism
into N, at arbitrary sources, followed by the projection onto
the relative tensor product. It obeys two structural laws, which
between them carry the whole construction.
- The balance law
RS.gpair_balance:gpair (gact a m) n = (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ gpair m (gact a n). A scalar may be moved from the left argument to the right one at the cost of braiding it past the source of the left argument. This is the defining relationRS.modTensor_conditionof the coequalizer, written in the language of the pairing: the leg acting onMdoes so throughRS.actRight, which is the left action conjugated by the braiding. - The action law
RS.gact_gpair:gact a (gpair m n) = (α_ X Y Z).inv ≫ gpair (gact a m) n. The descended action ofRon the relative tensor product is the action on the left factor.
Instantiating the balance law at the four source identifications
(λ_ (𝟙_ D)).inv, (λ_ L.obj).inv, (ρ_ L.obj).inv and
L.sq.inv gives the eight balancing laws RS.gpair_balanced_xyz
that the universal property of RS.SuperCommAlgebra.Mod.tensor
requires; the Koszul sign appears in exactly the two patterns
ooe and ooo, where the scalar and the left argument are both
odd, and it is RS.OddLine.braid_neg. Instantiating the action
law at the same four identifications gives the eight action laws
RS.gpair_act_xyz, which say that the resulting map is a morphism
of super modules.
The only identity not implied by coherence is the odd-odd-odd one,
RS.oddLine_sq_assoc: it is the first triangle identity of the
self-duality of the odd line,
RS.OddLine.evaluation_coevaluation.
The ungraded pairing #
noncomputable def
RS.gpair
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
{X Y : D}
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The pairing of a morphism into one module object with a morphism into another, taken at arbitrary sources: tensor the two morphisms and project to the relative tensor product.
Equations
Instances For
theorem
RS.gpair_def
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
{X Y : D}
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The pairing unfolded.
theorem
RS.comp_gpair
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
{W X Y : D}
(f : W ⟶ X)
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
Reindexing the left source of a pairing.
theorem
RS.gpair_comp
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
{X Y Z : D}
(m : X ⟶ M.X)
(g : Z ⟶ Y)
(n : Y ⟶ N.X)
:
Reindexing the right source of a pairing.
theorem
RS.add_gpair
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
{X Y : D}
(m m' : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The pairing is additive in its left argument.
theorem
RS.gpair_add
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
{X Y : D}
(m : X ⟶ M.X)
(n n' : Y ⟶ N.X)
:
The pairing is additive in its right argument.
theorem
RS.smul_gpair
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
(r : ℂ)
{X Y : D}
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The pairing is ℂ-homogeneous in its left argument.
theorem
RS.gpair_smul
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
(r : ℂ)
{X Y : D}
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The pairing is ℂ-homogeneous in its right argument.
The bundled bilinear pairing #
noncomputable def
RS.gpairLin
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
(M N : CategoryTheory.Mod D R)
{W X Y : D}
(s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
:
The pairing as a ℂ-bilinear map of hom-modules, transported
along a chosen morphism s from the intended source into the
tensor product of the two given sources. The four graded blocks of
the comparison map of RS.gammaPairComparison are the four
instances of this construction.
Equations
- RS.gpairLin M N s = LinearMap.mk₂ ℂ (fun (m : X ⟶ M.X) (n : Y ⟶ N.X) => CategoryTheory.CategoryStruct.comp s (RS.gpair m n)) ⋯ ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
RS.gpairLin_apply
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
(M N : CategoryTheory.Mod D R)
{W X Y : D}
(s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
(m : X ⟶ M.X)
(n : Y ⟶ N.X)
:
The balance law #
theorem
RS.gpair_balance
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
{X Y Z : D}
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
gpair (gact a m) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
(gpair m (gact a n)))
The balance law: a scalar may be moved from the left
argument of the pairing to the right one, at the cost of braiding
the scalar past the left source. This is the defining relation of
the relative tensor product, RS.modTensor_condition, written in
the language of the pairing.
The transported balance law #
theorem
RS.gpairLin_balance_comp
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
{W V X Y Z : D}
(s₁ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V Z)
(s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
((gpairLin M N s₁) (((gactLin s₂) a) m)) n = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp s₁
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp s₂ (β_ X Y).hom) Z)
(CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom))
(gpair m (gact a n))
The balance law with both sources reindexed, in the form used to discharge the eight balancing hypotheses: the two source identifications may be replaced by a single comparison morphism.
theorem
RS.gpairLin_balance
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
{W V U X Y Z : D}
(s₁ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V Z)
(s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
(s₃ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y U)
(s₄ : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
(h :
CategoryTheory.CategoryStruct.comp s₁
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp s₂ (β_ X Y).hom) Z)
(CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y s₄))
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
The transported balance law: given a coherence identity between the two ways of reindexing the sources, a scalar may be moved from the left argument of the pairing to the right one.
theorem
RS.gpairLin_balance_neg
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
{W V U X Y Z : D}
(s₁ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V Z)
(s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
(s₃ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y U)
(s₄ : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
(h :
CategoryTheory.CategoryStruct.comp s₁
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp s₂ (β_ X Y).hom) Z)
(CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom) = -CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y s₄))
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
The transported balance law with a Koszul sign: the
coherence identity may hold only up to sign, and then so does the
balance law. The sign arises from RS.OddLine.braid_neg, in
exactly the two cases where the scalar and the left argument are
both odd.
The action law #
theorem
RS.gact_gpair
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{M N : CategoryTheory.Mod D R}
{X Y Z : D}
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
gact a (gpair m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (gpair (gact a m) n)
The action law: the descended action of R on the
relative tensor product is the action on the left factor of a
pairing, up to the associator of the three sources.
theorem
RS.gpair_modTensorAct
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{M N : CategoryTheory.Mod D R}
{X Y Z : D}
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
The action law with the descended action named explicitly.
This is RS.gact_gpair retyped along RS.modTensorMod_X, and is
the form in which the law is transported.
theorem
RS.gpairLin_act
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{M N : CategoryTheory.Mod D R}
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
{W V U X Y Z : D}
(s₁ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X V)
(s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
(s₃ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj U Z)
(s₄ : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
(h :
CategoryTheory.CategoryStruct.comp s₁
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X s₂)
(CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerRight s₄ Z))
(a : X ⟶ R)
(m : Y ⟶ M.X)
(n : Z ⟶ N.X)
:
CategoryTheory.CategoryStruct.comp s₁
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a (((gpairLin M N s₂) m) n))
(modTensorAct R M N)) = ((gpairLin M N s₃) (((gactLin s₄) a) m)) n
The transported action law: given a coherence identity between the two ways of reindexing the sources, acting on the relative tensor product is acting on the left factor.
Coherence for the four source identifications #
theorem
RS.leftUnitor_inv_braiding
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
(Y : D)
:
Braiding past the unit on the left turns the left unitor into the right one.
theorem
RS.rightUnitor_inv_braiding
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
(Y : D)
:
Braiding past the unit on the right turns the right unitor into the left one.
theorem
RS.oddLine_sq_inv_braiding
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
(L : OddLine D)
:
The Koszul sign: braiding the square trivialisation of the
odd line past itself is RS.OddLine.braid_neg.
theorem
RS.oddLine_sq_leftUnitor
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp L.sq.inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv
L.obj)
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj
L.obj).hom) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.sq.inv)
Reassociating the square trivialisation against a left unitor: the odd-even-odd source identifications agree.
theorem
RS.oddLine_sq_leftUnitor'
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.sq.inv)
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj
L.obj).inv) = CategoryTheory.CategoryStruct.comp L.sq.inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv
L.obj)
The same identity read from the other end.
theorem
RS.oddLine_sq_rightUnitor
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.inv (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
(CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj
(CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom) = CategoryTheory.CategoryStruct.comp L.sq.inv
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj
(CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
Reassociating the square trivialisation against a right unitor: the odd-odd-even source identifications agree.
theorem
RS.oddLine_sq_rightUnitor'
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp L.sq.inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj
(CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
(CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj
(CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.inv (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
The same identity read from the other end.
theorem
RS.oddLine_sq_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.inv L.obj)
(CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj L.sq.inv)
The odd-odd-odd coherence identity, the one identity not implied by coherence alone: it is the first triangle identity of the self-duality of the odd line.
theorem
RS.oddLine_sq_assoc'
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
(L : OddLine D)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj L.sq.inv)
(CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj L.obj).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.inv L.obj)
The same identity read from the other end.
The eight balancing laws #
theorem
RS.gpair_balanced_eee
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
b)
m))
n = ((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
m)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
b)
n)
Balancing at parity pattern even-even-even.
theorem
RS.gpair_balanced_eoo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : L.obj ⟶ M.X)
(n : L.obj ⟶ N.X)
:
Balancing at parity pattern even-odd-odd.
theorem
RS.gpair_balanced_oeo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(c : L.obj ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : L.obj ⟶ N.X)
:
((gpairLin M N L.sq.inv) (((gactLin (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) c) m)) n = ((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
m)
(((gactLin L.sq.inv) c) n)
Balancing at parity pattern odd-even-odd: the scalar is odd and the left argument even, so there is no sign.
theorem
RS.gpair_balanced_ooe
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(c : L.obj ⟶ R)
(m : L.obj ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
Balancing at parity pattern odd-odd-even: the scalar and the left argument are both odd, so the Koszul sign appears.
theorem
RS.gpair_balanced_eeo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : L.obj ⟶ N.X)
:
((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
b)
m))
n = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) m)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) b) n)
Balancing at parity pattern even-even-odd.
theorem
RS.gpair_balanced_eoe
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : L.obj ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) b) m))
n = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) m)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
b)
n)
Balancing at parity pattern even-odd-even.
theorem
RS.gpair_balanced_oee
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(c : L.obj ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) c) m))
n = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) m)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) c) n)
Balancing at parity pattern odd-even-even: the left argument is even, so there is no sign.
theorem
RS.gpair_balanced_ooo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
(M N : CategoryTheory.Mod D R)
(c : L.obj ⟶ R)
(m : L.obj ⟶ M.X)
(n : L.obj ⟶ N.X)
:
Balancing at parity pattern odd-odd-odd: the scalar and the left argument are both odd, so the Koszul sign appears.
The eight action laws #
theorem
RS.gpair_act_eee
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
x)
(((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
m)
n) = ((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
x)
m))
n
The action law at parity pattern even-even-even.
theorem
RS.gpair_act_eoo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : L.obj ⟶ M.X)
(n : L.obj ⟶ N.X)
:
((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
x)
(((gpairLin M N L.sq.inv) m) n) = ((gpairLin M N L.sq.inv) (((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) x) m)) n
The action law at parity pattern even-odd-odd.
theorem
RS.gpair_act_eeo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : L.obj ⟶ N.X)
:
((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) x)
(((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) m) n) = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv)
(((gactLin
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
x)
m))
n
The action law at parity pattern even-even-odd.
theorem
RS.gpair_act_eoe
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(m : L.obj ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) x)
(((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) m) n) = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) x) m))
n
The action law at parity pattern even-odd-even.
theorem
RS.gpair_act_oee
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gactLin (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) u)
(((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
m)
n) = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv)
(((gactLin (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) u) m))
n
The action law at parity pattern odd-even-even.
theorem
RS.gpair_act_ooo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(m : L.obj ⟶ M.X)
(n : L.obj ⟶ N.X)
:
The action law at parity pattern odd-odd-odd.
theorem
RS.gpair_act_oeo
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : L.obj ⟶ N.X)
:
The action law at parity pattern odd-even-odd.
theorem
RS.gpair_act_ooe
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
{R : D}
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(m : L.obj ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
((gactLin L.sq.inv) u) (((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) m) n) = ((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
(((gactLin L.sq.inv) u) m))
n
The action law at parity pattern odd-odd-even.
The comparison map #
noncomputable def
RS.gammaPairEven
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
:
((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).even →ₗ[ℂ] (gammaModule D L R (modTensorMod R M N).X).even
The even block of the comparison map: the pairing on the even-even and odd-odd blocks, factored through the even part of the tensor product of super modules by its universal property.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
RS.gammaPairOdd
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
:
((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).odd →ₗ[ℂ] (gammaModule D L R (modTensorMod R M N).X).odd
The odd block of the comparison map: the pairing on the even-odd and odd-even blocks, factored through the odd part of the tensor product of super modules by its universal property.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
RS.gammaPairEven_tmulEE
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
(gammaPairEven L R M N) ((((gammaModule D L R M.X).tmulEE (gammaModule D L R N.X)) m) n) = ((gpairLin M N
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv)
m)
n
The even block on even-even generators.
@[simp]
theorem
RS.gammaPairEven_tmulOO
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(m : L.obj ⟶ M.X)
(n : L.obj ⟶ N.X)
:
(gammaPairEven L R M N) ((((gammaModule D L R M.X).tmulOO (gammaModule D L R N.X)) m) n) = ((gpairLin M N L.sq.inv) m) n
The even block on odd-odd generators.
@[simp]
theorem
RS.gammaPairOdd_tmulEO
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M.X)
(n : L.obj ⟶ N.X)
:
(gammaPairOdd L R M N) ((((gammaModule D L R M.X).tmulEO (gammaModule D L R N.X)) m) n) = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv) m) n
The odd block on even-odd generators.
@[simp]
theorem
RS.gammaPairOdd_tmulOE
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(m : L.obj ⟶ M.X)
(n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ N.X)
:
(gammaPairOdd L R M N) ((((gammaModule D L R M.X).tmulOE (gammaModule D L R N.X)) m) n) = ((gpairLin M N (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv) m) n
The odd block on odd-even generators.
theorem
RS.gammaPairEven_actEE
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(t : ((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).even)
:
(gammaPairEven L R M N) ((((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).actEE x) t) = ((gammaModule D L R (modTensorMod R M N).X).actEE x) ((gammaPairEven L R M N) t)
The even block intertwines the action of an even scalar.
theorem
RS.gammaPairOdd_actEO
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)
(t : ((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).odd)
:
(gammaPairOdd L R M N) ((((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).actEO x) t) = ((gammaModule D L R (modTensorMod R M N).X).actEO x) ((gammaPairOdd L R M N) t)
The odd block intertwines the action of an even scalar.
theorem
RS.gammaPairOdd_actOE
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(t : ((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).even)
:
(gammaPairOdd L R M N) ((((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).actOE u) t) = ((gammaModule D L R (modTensorMod R M N).X).actOE u) ((gammaPairEven L R M N) t)
The two blocks intertwine the action of an odd scalar on the even part.
theorem
RS.gammaPairEven_actOO
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
(u : L.obj ⟶ R)
(t : ((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).odd)
:
(gammaPairEven L R M N) ((((gammaModule D L R M.X).tensor (gammaModule D L R N.X)).actOO u) t) = ((gammaModule D L R (modTensorMod R M N).X).actOO u) ((gammaPairOdd L R M N) t)
The two blocks intertwine the action of an odd scalar on the odd part.
noncomputable def
RS.gammaPairComparison
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Linear ℂ D]
[CategoryTheory.MonoidalLinear ℂ D]
[CategoryTheory.Limits.HasCoequalizers D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(M N : CategoryTheory.Mod D R)
:
The comparison map of Deligne's (2.11.1): the tensor product over the Γ-algebra of the two Γ-modules maps to the Γ-module of the relative tensor product of the two module objects.
The two blocks are the pairing RS.gpair conjugated by the four
source identifications, and they descend by the universal property
of RS.SuperCommAlgebra.Mod.tensor because the eight balancing
laws hold; that they are morphisms of super modules is the eight
action laws.
Equations
- RS.gammaPairComparison L R M N = { evenMap := RS.gammaPairEven L R M N, oddMap := RS.gammaPairOdd L R M N, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }