The tensor complex with a coefficient module concentrated in degree zero is naturally identified degreewise with tensoring each original term by that coefficient module. The construction uses the unique nonzero summand in each degree, and verifies compatibility with the differential.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]abbrev coefficientSingle (M : ModuleCat.{u} R)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]def singleTensorInto (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
M ⊗ K.X n ⟶ (HomologicalComplex.tensorObj (coefficientSingle M) K).X nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]def singleTensorSummandOut (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n i j : ℕ)
(hij : ComplexShape.π (ComplexShape.up ℕ) (ComplexShape.up ℕ)
(ComplexShape.up ℕ) (i, j) = n) :
((curriedTensor (ModuleCat.{u} R)).obj (coefficientSingle M |>.X i)).obj
(K.X j) ⟶ M ⊗ K.X nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]def singleTensorOut (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
(HomologicalComplex.tensorObj (coefficientSingle M) K).X n ⟶ M ⊗ K.X nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]theorem singleTensorInto_out (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
singleTensorInto M K n ≫ singleTensorOut M K n = 𝟙 _Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]theorem singleTensorOut_into (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
singleTensorOut M K n ≫ singleTensorInto M K n = 𝟙 _Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]def singleTensorXIso (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
M ⊗ K.X n ≅ (HomologicalComplex.tensorObj (coefficientSingle M) K).X n where
hom := singleTensorInto M K n
inv := singleTensorOut M K n
hom_inv_id := singleTensorInto_out M K n
inv_hom_id := singleTensorOut_into M K nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]theorem single_tensor_d₁ (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (i j n : ℕ) :
mapBifunctor.d₁ (coefficientSingle M) K (curriedTensor (ModuleCat.{u} R))
(ComplexShape.up ℕ) i j n = 0Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]theorem singleTensorInto_comm (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (i j : ℕ) :
singleTensorInto M K i ≫ (HomologicalComplex.tensorObj (coefficientSingle M) K).d i j =
((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ) |>.obj K).d i j ≫
singleTensorInto M K jTensoring a complex with a module concentrated in degree zero is the same complex as tensoring every term with that module.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]def singleTensorComplexIso (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) :
((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj K ≅
HomologicalComplex.tensorObj ((HomologicalComplex.single (ModuleCat.{u} R)
(ComplexShape.up ℕ) 0).obj M) KThe coefficient comparison includes the unique single-factor summand in each degree.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]theorem singleTensorComplexIso_hom_f (M : ModuleCat.{u} R)
(K : CochainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
(singleTensorComplexIso M K).hom.f n =
((singleObjXSelf (ComplexShape.up ℕ) 0 M).inv ▷ K.X n) ≫
ιTensorObj ((HomologicalComplex.single (ModuleCat.{u} R)
(ComplexShape.up ℕ) 0).obj M) K 0 n n (zero_add n)