The comparison map on the free module of a mixed sum #
A mixed sum of copies of the unit and of the odd line presents its
free module as a finite family of retracts of free modules on the
two generators, so the comparison map of Deligne's (2.11.1) on it is
invertible as soon as it is invertible on those two. The unit case
is the left unitor of RS.gammaPairComparison_unitLeft; the odd
line is passed in as a hypothesis and discharged separately.
instance
RS.isIso_gammaPairComparison_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]
(N : CategoryTheory.Mod D R)
:
The comparison map is an isomorphism on the free module of the unit, since that free module is the regular module.
theorem
RS.isIso_gammaPairComparison_freeMix
{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]
{N : CategoryTheory.Mod D R}
(hL : CategoryTheory.IsIso (gammaPairComparison L R (freeMod R L.obj) N))
(p q : ℕ)
:
CategoryTheory.IsIso (gammaPairComparison L R (freeMod R (L.mix p q)) N)
The comparison map is an isomorphism on the free module of a mixed sum, given that it is on the free module of the odd line.
theorem
RS.isIso_gammaPairComparison_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]
{N : CategoryTheory.Mod D R}
(hL : CategoryTheory.IsIso (gammaPairComparison L R (freeMod R L.obj) N))
{X : D}
{p q : ℕ}
(e : freeMod R X ≅ freeMod R (L.mix p q))
:
CategoryTheory.IsIso (gammaPairComparison L R (freeMod R X) N)
The comparison map is an isomorphism on any free module that becomes a mixed sum.