The comparison map on a pair of free modules #
Putting the two retract reductions together with the odd-line square: the comparison map of Deligne's (2.11.1) is invertible at any pair of free modules whose objects become mixed sums after base change. Every case but the odd line against itself is a unitor.
instance
RS.isIso_gammaPairComparison_freeL_freeUnit
{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]
:
The comparison map at the odd line against the unit is the right unitor.
theorem
RS.isIso_gammaPairComparison_freeL_mix
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(p q : ℕ)
:
CategoryTheory.IsIso (gammaPairComparison L R (freeMod R L.obj) (freeMod R (L.mix p q)))
The comparison map at the odd line against the free module of a mixed sum.
theorem
RS.isIso_gammaPairComparison_freeL_free
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{Y : D}
{p q : ℕ}
(eY : freeMod R Y ≅ freeMod R (L.mix p q))
:
CategoryTheory.IsIso (gammaPairComparison L R (freeMod R L.obj) (freeMod R Y))
The comparison map at the odd line against any free module that becomes a mixed sum.
theorem
RS.isIso_gammaPairComparison_freeFree
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{X Y : D}
{p q p' q' : ℕ}
(eX : freeMod R X ≅ freeMod R (L.mix p q))
(eY : freeMod R Y ≅ freeMod R (L.mix p' q'))
:
CategoryTheory.IsIso (gammaPairComparison L R (freeMod R X) (freeMod R Y))
The comparison map of (2.11.1) at a pair of free modules.
theorem
RS.isIso_fibreMu_of_mix
{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]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[∀ (X : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft X)]
(L : OddLine D)
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
{X Y : D}
{p q p' q' : ℕ}
(eX : freeMod R X ≅ freeMod R (L.mix p q))
(eY : freeMod R Y ≅ freeMod R (L.mix p' q'))
:
CategoryTheory.IsIso (fibreMu L R X Y)
The monoidal comparison of the fibre functor is an isomorphism at any pair of objects that become mixed sums.