Naturality of the comparison map

The comparison map RS.gammaPairComparison of Deligne's (2.11.1) is natural in each of its two module variables: realization RS.gammaModuleFunctor carries a morphism of module objects to a morphism of Γ-modules, both sides of the comparison map are functorial in that morphism, and the resulting square commutes.

Everything rests on one identity, RS.gpair_naturality: the ungraded pairing RS.gpair of a morphism into M against a morphism into N is natural, that is, gpair (m ≫ f.hom) (n ≫ g.hom) = gpair m n ≫ modTensorMap R f g. This is the defining equation of RS.modTensorMap against RS.modTensorπ, read through the interchange law. Transported along a source identification it becomes RS.gpairLin_naturality, and the four graded blocks of the comparison map are four instances of that one statement, one for each family of generators of the tensor product of super modules. The extensionality principle RS.SuperCommAlgebra.Mod.hom_ext reduces the naturality square to exactly those four instances.

Contents

• RS.gpair_naturality, RS.gpairLin_naturality: naturality of the ungraded pairing, plain and transported.
• RS.modTensorMapMod_id', RS.modTensorMapMod_comp', RS.modTensorMapModIso: functoriality of the bundled relative tensor product, and the isomorphism it yields from a pair of isomorphisms.
• RS.SuperCommAlgebra.Mod.tensorIso: the tensor product of two isomorphisms of super modules.
• RS.gammaPairComparison_naturality_left, RS.gammaPairComparison_naturality_right, RS.gammaPairComparison_naturality: the naturality squares.
• RS.gammaPairComparison_isIso_of_iso: whether the comparison map is an isomorphism depends only on the isomorphism classes of the two module objects.

Naturality of the ungraded pairing

theorem RS.gpair_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] (R : D) [CategoryTheory.MonObj R] {M M' N N' : CategoryTheory.Mod D R} {X Y : D} (f : M ⟶ M') (g : N ⟶ N') (m : X ⟶ M.X) (n : Y ⟶ N.X) : gpair (CategoryTheory.CategoryStruct.comp m f.hom) (CategoryTheory.CategoryStruct.comp n g.hom) = CategoryTheory.CategoryStruct.comp (gpair m n) (modTensorMap R f g)

Naturality of the pairing: pairing after postcomposition with a pair of module morphisms is pairing followed by the functorial map of the relative tensor product.

theorem RS.gpairLin_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] (R : D) [CategoryTheory.MonObj R] {M M' N N' : CategoryTheory.Mod D R} {W X Y : D} (s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f : M ⟶ M') (g : N ⟶ N') (m : X ⟶ M.X) (n : Y ⟶ N.X) : CategoryTheory.CategoryStruct.comp s (gpair (CategoryTheory.CategoryStruct.comp m f.hom) (CategoryTheory.CategoryStruct.comp n g.hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (gpair m n)) (modTensorMap R f g)

The transported naturality of the pairing: the form taken by RS.gpair_naturality at a source identification, that is, at one graded block of the comparison map.

Functoriality of the bundled relative tensor product

theorem RS.modTensorMapMod_id' {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) : modTensorMapMod R (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (modTensorMod R M N)

The bundled functorial map preserves identities.

theorem RS.modTensorMapMod_comp' {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 M' M'' N N' N'' : CategoryTheory.Mod D R} (f : M ⟶ M') (f' : M' ⟶ M'') (g : N ⟶ N') (g' : N' ⟶ N'') : modTensorMapMod R (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (modTensorMapMod R f g) (modTensorMapMod R f' g')

The bundled functorial map preserves composition.

noncomputable def RS.modTensorMapModIso {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 M' N N' : CategoryTheory.Mod D R} (e : M ≅ M') (e' : N ≅ N') : modTensorMod R M N ≅ modTensorMod R M' N'

The relative tensor product of two isomorphisms of module objects.

Equations

• RS.modTensorMapModIso R e e' = { hom := RS.modTensorMapMod R e.hom e'.hom, inv := RS.modTensorMapMod R e.inv e'.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Two conveniences for super modules

theorem RS.SuperCommAlgebra.Mod.comp_evenMap_apply {S : SuperCommAlgebra} {P Q T : S.Mod} (a : P ⟶ Q) (b : Q ⟶ T) (t : P.even) : (CategoryTheory.CategoryStruct.comp a b).evenMap t = b.evenMap (a.evenMap t)

The even component of a composite, applied to an element.

theorem RS.SuperCommAlgebra.Mod.comp_oddMap_apply {S : SuperCommAlgebra} {P Q T : S.Mod} (a : P ⟶ Q) (b : Q ⟶ T) (t : P.odd) : (CategoryTheory.CategoryStruct.comp a b).oddMap t = b.oddMap (a.oddMap t)

The odd component of a composite, applied to an element.

noncomputable def RS.SuperCommAlgebra.Mod.tensorIso {S : SuperCommAlgebra} {P P' Q Q' : S.Mod} (a : P ≅ P') (b : Q ≅ Q') : P.tensor Q ≅ P'.tensor Q'

The tensor product of two isomorphisms of super modules.

Equations

• RS.SuperCommAlgebra.Mod.tensorIso a b = { hom := RS.SuperCommAlgebra.Mod.tensorHom a.hom b.hom, inv := RS.SuperCommAlgebra.Mod.tensorHom a.inv b.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Naturality of the comparison map

@[reducible, inline]

noncomputable abbrev RS.gammaFunMap {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] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {M M' : CategoryTheory.Mod D R} (f : M ⟶ M') : gammaModule D L R M.X ⟶ gammaModule D L R M'.X

Realization of a morphism of module objects, with its type written at the Γ-modules themselves. This is RS.gammaModuleFunctor on morphisms, and is reducibly equal to it; naming it keeps the two ends of a naturality square typed by the same expressions.

Equations

• RS.gammaFunMap L R f = (RS.gammaModuleFunctor L R).map f

theorem RS.gammaFunMap_id {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] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) : gammaFunMap L R (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (gammaModule D L R M.X)

Realization takes an identity to an identity.

@[simp]

theorem RS.gammaPairComparison_evenMap {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) : (gammaPairComparison L R M N).evenMap = gammaPairEven L R M N

@[simp]

theorem RS.gammaPairComparison_oddMap {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) : (gammaPairComparison L R M N).oddMap = gammaPairOdd L R M N

theorem RS.gammaPairComparison_naturality_aux {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 M' N N' : CategoryTheory.Mod D R} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (gammaFunMap L R f) (gammaFunMap L R g)) (gammaPairComparison L R M' N') = CategoryTheory.CategoryStruct.comp (gammaPairComparison L R M N) (gammaFunMap L R (modTensorMapMod R f g))

The naturality square, with the realized morphisms typed at the Γ-modules. This is RS.gammaPairComparison_naturality in the form in which it is proved.

theorem RS.gammaPairComparison_naturality {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 M' N N' : CategoryTheory.Mod D R} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom ((gammaModuleFunctor L R).map f) ((gammaModuleFunctor L R).map g)) (gammaPairComparison L R M' N') = CategoryTheory.CategoryStruct.comp (gammaPairComparison L R M N) ((gammaModuleFunctor L R).map (modTensorMapMod R f g))

The naturality square of the comparison map, in both module variables at once.

theorem RS.gammaPairComparison_naturality_left {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 M' : CategoryTheory.Mod D R} (f : M ⟶ M') (N : CategoryTheory.Mod D R) : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom ((gammaModuleFunctor L R).map f) (CategoryTheory.CategoryStruct.id (gammaModule D L R N.X))) (gammaPairComparison L R M' N) = CategoryTheory.CategoryStruct.comp (gammaPairComparison L R M N) ((gammaModuleFunctor L R).map (modTensorMapMod R f (CategoryTheory.CategoryStruct.id N)))

The naturality square of the comparison map in the first module variable.

theorem RS.gammaPairComparison_naturality_right {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] {N N' : CategoryTheory.Mod D R} (M : CategoryTheory.Mod D R) (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (CategoryTheory.CategoryStruct.id (gammaModule D L R M.X)) ((gammaModuleFunctor L R).map g)) (gammaPairComparison L R M N') = CategoryTheory.CategoryStruct.comp (gammaPairComparison L R M N) ((gammaModuleFunctor L R).map (modTensorMapMod R (CategoryTheory.CategoryStruct.id M) g))

The naturality square of the comparison map in the second module variable.

theorem RS.gammaPairComparison_isIso_of_iso {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 M' N N' : CategoryTheory.Mod D R} (e : M ≅ M') (e' : N ≅ N') (h : CategoryTheory.IsIso (gammaPairComparison L R M' N')) : CategoryTheory.IsIso (gammaPairComparison L R M N)

Invariance of the comparison map under isomorphism: whether the comparison map is an isomorphism depends only on the isomorphism classes of the two module objects.