The method of acyclic models #
Let F and G be functors from a category C to chain complexes of modules over a ring k.
Suppose that F is free on models: in each degree n there are a model Mₙ : C and a
generator uₙ ∈ Fₙ(Mₙ), and every element of Fₙ(X) is a combination of the images of uₙ
under the maps σ : Mₙ ⟶ X, with coefficients chosen naturally in X
(ModelPresentation; the coefficients need not be unique, so this is a presentation rather than
a basis). Suppose that G is acyclic on the models: its homology vanishes in positive
degrees on every model, and in degree zero a chain of augmentation zero is a boundary
(IsAcyclicOn). Then:
- a natural chain map
F ⟶ Gexists as soon as it exists in degree zero compatibly with the augmentations, provided the augmentation ofFvanishes on boundaries (ModelPresentation.chainMap); - two natural chain maps
F ⟶ Gwhich agree after augmentation in degree zero are chain homotopic (ModelPresentation.homotopy).
Both are built degree by degree. A natural map out of Fₙ is determined by its value on the
generator uₙ, and every element t ∈ Gₘ(Mₙ) determines one,
ModelPresentation.extend t. Its value on the generator need not be t itself, since the
coefficients of uₙ need not be those of a single basis element; what matters is that the
boundary of the extended map is controlled by the boundary of t
(ModelPresentation.d_extend). So at each step it suffices to choose an element of G(Mₙ)
whose boundary is a prescribed chain; that chain is a cycle by the previous step, hence a
boundary by acyclicity. The chosen elements are internal to the construction.
This is the form of the theorem of Eilenberg and Mac Lane used for the comparison of cubical and
simplicial singular chains. The coefficients σ ↦ aσ need not be unique: the normalized cubical
chains are only a natural retract of the free modules on the cubes.
The method is also available with several models in each degree
(MultiModelPresentation, IsAcyclicOnMulti): the generator and the model are then indexed by
a type ι n in each degree n, as for the tensor product of two chain complexes, where the
models of degree n are indexed by the bidegrees (p, q) with p + q = n. The single-model
statements above are the special case of one index, and are derived from the general ones
(ModelPresentation.toMulti).
Main definitions #
TauCeti.AcyclicModels.ModelPresentation: a functor free on models.TauCeti.AcyclicModels.ModelPresentation.extend: the natural map determined by an element on a model.TauCeti.AcyclicModels.IsAcyclicOn: acyclicity of a functor on the models.TauCeti.AcyclicModels.ModelPresentation.chainMap: the natural chain map extending a degree-zero map.TauCeti.AcyclicModels.ModelPresentation.homotopy: the chain homotopy between two natural chain maps.TauCeti.AcyclicModels.MultiModelPresentation,TauCeti.AcyclicModels.IsAcyclicOnMulti,TauCeti.AcyclicModels.MultiModelPresentation.chainMap,TauCeti.AcyclicModels.MultiModelPresentation.homotopy: the same with several models in each degree.
References #
- S. Eilenberg and S. Mac Lane, Acyclic models, Amer. J. Math. 75 (1953).
- W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII.
A functor to chain complexes is free on models when, in each degree n, every element
of Fₙ(X) is a combination Σ aσ • F(σ)(uₙ) of the images of a generator uₙ ∈ Fₙ(Mₙ) on a
model Mₙ, with coefficients σ ↦ aσ depending linearly and naturally on the element.
- model : ℕ → C
The model in degree
n. The generator in degree
n, a chain of the model.The coefficients of a chain in terms of the images of the generator.
- coord_map {X Y : C} (f : X ⟶ Y) (n : ℕ) (x : ↑((F.obj X).X n)) : (self.coord Y n) ((CategoryTheory.ConcreteCategory.hom ((F.map f).f n)) x) = Finsupp.mapDomain (fun (x : self.model n ⟶ X) => CategoryTheory.CategoryStruct.comp x f) ((self.coord X n) x)
The coefficients are natural.
- sum_coord (X : C) (n : ℕ) (x : ↑((F.obj X).X n)) : (((self.coord X n) x).sum fun (σ : self.model n ⟶ X) (a : k) => a • (CategoryTheory.ConcreteCategory.hom ((F.map σ).f n)) (self.gen n)) = x
Every chain is the combination of the images of the generator with its coefficients.
Instances For
A functor to chain complexes is acyclic on the models M for the augmentation ε when,
on every model, its cycles of positive degree are boundaries and its 0-chains of augmentation
zero are boundaries.
Instances For
The natural map Fₙ(X) → Gₘ(X) determined by an element t ∈ Gₘ(Mₙ):
Σ aσ • F(σ)(uₙ) ↦ Σ aσ • G(σ)(t).
Instances For
A functor to chain complexes is free on a family of models when, in each degree n, there
is a family of models Mₙᵢ indexed by i : ι n, with generators uₙᵢ ∈ Fₙ(Mₙᵢ), such that every
element of Fₙ(X) is a combination Σ aσ • F(σ)(uₙᵢ) over the pairs (i, σ : Mₙᵢ ⟶ X), with
coefficients depending linearly and naturally on the element. With ι n a singleton this is
ModelPresentation.
- model (n : ℕ) : ι n → C
The models in degree
n. The generators in degree
n, chains of the models.The coefficients of a chain in terms of the images of the generators.
- coord_map {X Y : C} (f : X ⟶ Y) (n : ℕ) (x : ↑((F.obj X).X n)) : (self.coord Y n) ((CategoryTheory.ConcreteCategory.hom ((F.map f).f n)) x) = Finsupp.mapDomain (fun (p : (i : ι n) × (self.model n i ⟶ X)) => ⟨p.fst, CategoryTheory.CategoryStruct.comp p.snd f⟩) ((self.coord X n) x)
The coefficients are natural.
- sum_coord (X : C) (n : ℕ) (x : ↑((F.obj X).X n)) : (((self.coord X n) x).sum fun (p : (i : ι n) × (self.model n i ⟶ X)) (a : k) => a • (CategoryTheory.ConcreteCategory.hom ((F.map p.snd).f n)) (self.gen n p.fst)) = x
Every chain is the combination of the images of the generators with its coefficients.
Instances For
A functor to chain complexes is acyclic on a family of models M for the augmentation
ε when, on every model of every degree, its cycles of positive degree are boundaries and its
0-chains of augmentation zero are boundaries.
Instances For
The natural map Fₙ(X) → Gₘ(X) determined by elements tᵢ ∈ Gₘ(Mₙᵢ) of the models:
Σ aσ • F(σ)(uₙᵢ) ↦ Σ aσ • G(σ)(tᵢ).
Instances For
The map determined by elements on the models is natural.
The map extend t determined by elements tᵢ ∈ Gₘ(Mₙᵢ) of the models, as a natural
transformation from the degree-n chains of F to the degree-m chains of G.
Instances For
The component of extendNatTrans t at X is the map extend t X.
A natural map φ : Fₙ ⟶ Gₘ is the map determined, through extend, by its values φ(uₙᵢ) on
the generators; in particular, it is determined by these values.
The augmentation of the map determined by elements tᵢ of the models is the augmentation of
the source, when the augmentations are natural and each tᵢ has the augmentation of the
generator.
Two natural chain maps f, g : F ⟶ G have the same augmentation in degree zero as soon as they
have the same augmentation on the generators of the models of degree zero, when the augmentation
of G is natural. It reduces the hypothesis of MultiModelPresentation.homotopy to a check on
the generators.
The boundary of a map determined on the models: if the boundary of each tᵢ is the value
on the generator uₙᵢ of a natural transformation R, then the boundary of the map determined by
the tᵢ is R.
Existence of natural chain maps: if G is acyclic on the models of F and the augmentation
of F vanishes on boundaries, the natural map F₀ → G₀ determined by t₀, compatible with the
augmentations, extends to a natural chain map F ⟶ G.
Instances For
In degree zero the natural chain map is the map determined by t₀.
Uniqueness up to homotopy of natural chain maps: two natural chain maps F ⟶ G which
agree after augmentation in degree zero are chain homotopic, if G is acyclic on the models of
F. The homotopy is natural (MultiModelPresentation.homotopy_hom_naturality).
Instances For
The components of the chain homotopy vanish off the shape of the complexes.
The chain homotopy is natural.
A presentation by one model in each degree is a presentation by a family of models indexed by a singleton.
Instances For
The models of toMulti are the models of the presentation.
The generators of toMulti are the generators of the presentation.
The coefficients of toMulti are those of the presentation, indexed by the singleton.
The map determined by one element on the model is the map determined by the corresponding family of elements.
The augmentation of the map determined by an element t on the model is the augmentation of
the source, when the augmentations are natural and t has the augmentation of the generator.
Two natural chain maps f, g : F ⟶ G have the same augmentation in degree zero as soon as they
have the same augmentation on the generator of the model of degree zero, when the augmentation of
G is natural.
The map determined by an element on the model is natural.
The map extend t determined by an element t ∈ Gₘ(Mₙ) on the model, as a natural
transformation from the degree-n chains of F to the degree-m chains of G.
Instances For
The component of extendNatTrans t at X is the map extend t X.
A natural map φ : Fₙ ⟶ Gₘ is the map determined, through extend, by its value φ(uₙ) on
the generator; in particular, it is determined by this value.
The boundary of a map determined on the model: if the boundary of t is the value on
the generator uₙ of a natural transformation R, then the boundary of the map determined by
t is R.
Acyclicity on the models of a presentation by one model in each degree is acyclicity on the
family of models of toMulti.
Existence of natural chain maps: if G is acyclic on the models of F and the augmentation
of F vanishes on boundaries, the natural map F₀ → G₀ determined by t₀, compatible with the
augmentations, extends to a natural chain map F ⟶ G. This is the case of one model in each
degree of MultiModelPresentation.chainMap.
Instances For
In degree zero the natural chain map is the map determined by t₀.
Uniqueness up to homotopy of natural chain maps: two natural chain maps F ⟶ G which
agree after augmentation in degree zero are chain homotopic, if G is acyclic on the models of
F. The homotopy is natural (ModelPresentation.homotopy_hom_naturality).
Instances For
The components of the chain homotopy vanish off the shape of the complexes.
The chain homotopy is natural.