The comparison map on a family of retracts, second variable #
The mirror of RS.isIso_gammaPairComparison_of_retracts: a finite
family of retracts in the second module variable, total in the same
sense, transports invertibility of the comparison map of Deligne's
(2.11.1) in exactly the same way.
theorem
RS.SuperCommAlgebra.Mod.tensorHom_zero_right
{S : SuperCommAlgebra}
{M N P Q : S.Mod}
(f : M ⟶ P)
:
The tensor product of super modules kills the zero morphism in the right variable.
theorem
RS.SuperCommAlgebra.Mod.tensorHom_sum_right
{S : SuperCommAlgebra}
{M N P Q : S.Mod}
{ι : Type u_1}
(s : Finset ι)
(f : M ⟶ P)
(g : ι → (N ⟶ Q))
:
The tensor product of super modules takes a finite sum in the right variable to a finite sum.
theorem
RS.sum_modTensorMapMod_right
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive 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]
{ι : Type u_1}
(s : Finset ι)
{M N : CategoryTheory.Mod D R}
(g : ι → (N ⟶ N))
(h : ∑ i ∈ s, (g i).hom = CategoryTheory.CategoryStruct.id N.X)
:
∑ i ∈ s, (modTensorMapMod R (CategoryTheory.CategoryStruct.id M) (g i)).hom = CategoryTheory.CategoryStruct.id (modTensorMod R M N).X
The mirror of RS.sum_modTensorMapMod, in the second
variable.
theorem
RS.isIso_gammaPairComparison_of_retracts_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]
{ι : Type u_1}
[Fintype ι]
(M : CategoryTheory.Mod D R)
{N : CategoryTheory.Mod D R}
{N' : ι → CategoryTheory.Mod D R}
(s : (i : ι) → N' i ⟶ N)
(r : (i : ι) → N ⟶ N' i)
(htot : ∑ i : ι, CategoryTheory.CategoryStruct.comp (r i).hom (s i).hom = CategoryTheory.CategoryStruct.id N.X)
(h : ∀ (i : ι), CategoryTheory.IsIso (gammaPairComparison L R M (N' i)))
:
CategoryTheory.IsIso (gammaPairComparison L R M N)
The comparison map on a family of retracts in the second variable.