Module

TensorComplexCoefficientFunctor.lean

Nyll.EtaleFundamentalGroups.Purity.TensorComplexCoefficientFunctor

3 declarations indexed from sourceView source ↗

Module documentation

Exactness in the coefficients of a flat tensor complex

Tensoring every term of a fixed complex defines a functor in the coefficient module. When all its terms are flat, coefficient short exact sequences remain short exact sequences of complexes. Consequently an injective acyclicity result gives the usual cohomology dimension shift.

Imports4

Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.HomologicalComplexAbelian
Mathlib.Algebra.Homology.HomologySequence
Mathlib.RingTheory.Flat.CategoryTheory

Imported by2

def

tensorComplexCoefficientFunctor

L32 ↗

EtaleFundamentalGroups.Purity.tensorComplexCoefficientFunctor

Documentation

Tensor coefficients of a fixed nonnegative cochain complex.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · full declaration

def tensorComplexCoefficientFunctor (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    ModuleCat.{u} R ⥤ CochainComplex (ModuleCat.{u} R) ℕ where
  obj M := ((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj K
  map f :=
    { f := fun n => f ▷ K.X n
      comm' := fun i j _ => (whisker_exchange f (K.d i j)).symm }
  map_id M := by
    apply HomologicalComplex.Hom.ext
    funext n
    exact id_whiskerRight M (K.X n)
  map_comp f g := by
    apply HomologicalComplex.Hom.ext
    funext n
    exact comp_whiskerRight f g (K.X n)

instance

(anonymous instance)

L47 ↗

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · full declaration

instance (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    (tensorComplexCoefficientFunctor K).Additive where
  map_add := by
    intro M N f g
    apply HomologicalComplex.Hom.ext
    funext n
    exact MonoidalPreadditive.add_whiskerRight (X := K.X n) f g

theorem

tensorComplexCoefficientFunctor_shortExact

L56 ↗

EtaleFundamentalGroups.Purity.tensorComplexCoefficientFunctor_shortExact

Documentation

Flat terms preserve each coefficient short exact sequence.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem tensorComplexCoefficientFunctor_shortExact
    (K : CochainComplex (ModuleCat.{u} R) ℕ) [∀ n, Module.Flat R (K.X n)]
    {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact) :
    (S.map (tensorComplexCoefficientFunctor K)).ShortExact

Module documentation

Exactness in the coefficients of a flat tensor complex

Declarations

tensorComplexCoefficientFunctor

(anonymous instance)

tensorComplexCoefficientFunctor_shortExact