Singular chains with local coefficients

A local coefficient system L on a space X is a functor from its fundamental groupoid to modules, so it assigns a module to every point and a transport isomorphism to every path class. Twisting the singular chain complex by L replaces the free module on the singular n-simplices by the coproduct, over singular n-simplices σ, of the fibre of L at the initial vertex of σ. Reindexing a simplex moves its initial vertex inside the simplex, so the structure maps of the resulting simplicial module also transport the coefficients along the image of a path joining the old initial vertex to the new one.

The topological simplex is simply connected, so that path class, and hence the transport, is determined by its endpoints alone. This is what makes the simplicial identities hold: a composite of transports is again the transport between its endpoints, and the boundary of a twisted chain complex therefore squares to zero for the same formal reason as in the untwisted case.

For a constant system the twisting is trivial and the construction returns Mathlib's singular chain complex, while a continuous map f : X ⟶ Y induces a chain map from the chains of X twisted by the system pulled back along f.

Main declarations

• TauCeti.LocalCoefficientSystem.twistedChains: the simplicial module of twisted chains, and twistedChainComplex, twistedHomology for its alternating face map complex and homology.
• TauCeti.LocalCoefficientSystem.twistedChainsFunctor: twisted chains as a functor of the coefficient system, with twistedChainComplexCoefficientMap and twistedHomologyCoefficientMap for the induced maps of complexes and of homology, together with their identity and composition laws.
• TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso: for a constant system, twisted homology is ordinary singular homology, naturally both in the module of coefficients and in the space.
• TauCeti.LocalCoefficientSystem.twistedChainComplexMap: the chain map induced by a continuous map, and twistedHomologyMap the resulting map on twisted homology, together with their identity and composition laws and their naturality in the coefficient system.

References

• A. Hatcher, Algebraic Topology, Section 3.H.

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.initialVertex {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) : FundamentalGroupoid ↑X

The initial vertex of a singular simplex, as an object of the fundamental groupoid.

Equations

• TauCeti.LocalCoefficientSystem.initialVertex σ = { as := (TauCeti.TopCat.simplexMap σ) (Opposite.unop n).toTopInitialVertex }

noncomputable def TauCeti.LocalCoefficientSystem.pathTransport {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z w : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) : { as := (TopCat.simplexMap σ) z } ⟶ { as := (TopCat.simplexMap σ) w }

The morphism of the fundamental groupoid of X obtained by running a singular simplex along the unique path class between two points of its simplex.

Equations

• TauCeti.LocalCoefficientSystem.pathTransport σ z w = (FundamentalGroupoid.map (TauCeti.TopCat.simplexMap σ)).map default

@[simp]

theorem TauCeti.LocalCoefficientSystem.pathTransport_self {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) : pathTransport σ z z = CategoryTheory.CategoryStruct.id { as := (TopCat.simplexMap σ) z }

Transport inside a simplex from a point to itself is the identity.

@[simp]

theorem TauCeti.LocalCoefficientSystem.pathTransport_comp {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z w y : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) : CategoryTheory.CategoryStruct.comp (pathTransport σ z w) (pathTransport σ w y) = pathTransport σ z y

Transports inside a simplex compose: running from z to w and then from w to y is running from z to y.

@[simp]

theorem TauCeti.LocalCoefficientSystem.pathTransport_comp_assoc {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z w y : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) {Z : FundamentalGroupoid ↑X} (h : { as := (TopCat.simplexMap σ) y } ⟶ Z) : CategoryTheory.CategoryStruct.comp (pathTransport σ z w) (CategoryTheory.CategoryStruct.comp (pathTransport σ w y) h) = CategoryTheory.CategoryStruct.comp (pathTransport σ z y) h

Transports inside a simplex compose: running from z to w and then from w to y is running from z to y.

theorem TauCeti.LocalCoefficientSystem.pathTransport_eqToHom {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) {w w' : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))} (h : w = w') : CategoryTheory.CategoryStruct.comp (pathTransport σ z w) (CategoryTheory.eqToHom ⋯) = pathTransport σ z w'

Transport inside a simplex may be moved along an equality of its target point.

theorem TauCeti.LocalCoefficientSystem.pathTransport_eqToHom_assoc {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) (z : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) {w w' : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))} (h : w = w') {Z : FundamentalGroupoid ↑X} (h✝ : { as := (TopCat.simplexMap σ) w' } ⟶ Z) : CategoryTheory.CategoryStruct.comp (pathTransport σ z w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝) = CategoryTheory.CategoryStruct.comp (pathTransport σ z w') h✝

Transport inside a simplex may be moved along an equality of its target point.

theorem TauCeti.LocalCoefficientSystem.pathTransport_map {X : TopCat} {m n : SimplexCategoryᵒᵖ} (α : m ⟶ n) (σ : (TopCat.toSSet.obj X).obj m) (z w : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) : pathTransport ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ) z w = pathTransport σ ((CategoryTheory.ConcreteCategory.hom (SimplexCategory.toTop.{v}.map α.unop)) z) ((CategoryTheory.ConcreteCategory.hom (SimplexCategory.toTop.{v}.map α.unop)) w)

Transport inside a reindexed simplex is transport inside the original simplex, between the images of the two points under the reindexing.

theorem TauCeti.LocalCoefficientSystem.map_pathTransport {X Y : TopCat} {n : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (σ : (TopCat.toSSet.obj X).obj n) (z w : ↑(SimplexCategory.toTop.{v}.obj (Opposite.unop n))) : (FundamentalGroupoid.map (TopCat.Hom.hom f)).map (pathTransport σ z w) = pathTransport ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) σ) z w

Pushing a singular simplex forward along a continuous map carries transport inside it to transport inside the image simplex.

noncomputable def TauCeti.LocalCoefficientSystem.vertexTransport {X : TopCat} {m n : SimplexCategoryᵒᵖ} (α : m ⟶ n) (σ : (TopCat.toSSet.obj X).obj m) : initialVertex σ ⟶ initialVertex ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ)

The transport from the initial vertex of a singular m-simplex σ to the initial vertex of the singular n-simplex obtained from σ by reindexing along α.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LocalCoefficientSystem.vertexTransport_id {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) : vertexTransport (CategoryTheory.CategoryStruct.id n) σ = CategoryTheory.eqToHom ⋯

Reindexing along an identity does not move the initial vertex, so the transport it induces is the canonical identification of the two coefficient modules.

theorem TauCeti.LocalCoefficientSystem.vertexTransport_comp {X : TopCat} {m n p : SimplexCategoryᵒᵖ} (α : m ⟶ n) (β : n ⟶ p) (σ : (TopCat.toSSet.obj X).obj m) : CategoryTheory.CategoryStruct.comp (vertexTransport α σ) (vertexTransport β ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ)) = CategoryTheory.CategoryStruct.comp (vertexTransport (CategoryTheory.CategoryStruct.comp α β) σ) (CategoryTheory.eqToHom ⋯)

Reindexing along a composite induces the composite of the two vertex transports, up to the canonical identification of the two resulting simplices.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChains {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : CategoryTheory.SimplicialObject (ModuleCat R)

The simplicial object of singular chains of X twisted by the local coefficient system L. In degree n it is the coproduct, over the singular n-simplices σ of X, of the fibre of L at the initial vertex of σ; a reindexing acts on the summands by transport along the initial vertices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.LocalCoefficientSystem.ιTwistedChains {R : Type u} [Ring R] {X : TopCat} {n : SimplexCategoryᵒᵖ} (L : LocalCoefficientSystem R X) (σ : (TopCat.toSSet.obj X).obj n) : L.obj (initialVertex σ) ⟶ L.twistedChains.obj n

The inclusion into twisted chains of the coefficient module attached to a singular simplex.

Equations

• L.ιTwistedChains σ = CategoryTheory.Limits.Sigma.ι (fun (τ : (TopCat.toSSet.obj X).obj n) => L.obj (TauCeti.LocalCoefficientSystem.initialVertex τ)) σ

theorem TauCeti.LocalCoefficientSystem.twistedChains_hom_ext {R : Type u} [Ring R] {X : TopCat} {n : SimplexCategoryᵒᵖ} (L : LocalCoefficientSystem R X) {A : ModuleCat R} {f g : L.twistedChains.obj n ⟶ A} (h : ∀ (σ : (TopCat.toSSet.obj X).obj n), CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) f = CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) g) : f = g

Two maps out of a module of twisted chains agree as soon as they agree on every summand.

theorem TauCeti.LocalCoefficientSystem.twistedChains_hom_ext_iff {R : Type u} [Ring R] {X : TopCat} {n : SimplexCategoryᵒᵖ} {L : LocalCoefficientSystem R X} {A : ModuleCat R} {f g : L.twistedChains.obj n ⟶ A} : f = g ↔ ∀ (σ : (TopCat.toSSet.obj X).obj n), CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) f = CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) g

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_map {R : Type u} [Ring R] {X : TopCat} {m n : SimplexCategoryᵒᵖ} (L : LocalCoefficientSystem R X) (α : m ⟶ n) (σ : (TopCat.toSSet.obj X).obj m) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) (L.twistedChains.map α) = CategoryTheory.CategoryStruct.comp (L.map (vertexTransport α σ)) (L.ιTwistedChains ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ))

A structure map of twisted chains sends the summand of a simplex σ into the summand of the reindexed simplex, after transporting the coefficients along the initial vertices.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_map_assoc {R : Type u} [Ring R] {X : TopCat} {m n : SimplexCategoryᵒᵖ} (L : LocalCoefficientSystem R X) (α : m ⟶ n) (σ : (TopCat.toSSet.obj X).obj m) {Z : ModuleCat R} (h : L.twistedChains.obj n ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) (CategoryTheory.CategoryStruct.comp (L.twistedChains.map α) h) = CategoryTheory.CategoryStruct.comp (L.map (vertexTransport α σ)) (CategoryTheory.CategoryStruct.comp (L.ιTwistedChains ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ)) h)

A structure map of twisted chains sends the summand of a simplex σ into the summand of the reindexed simplex, after transporting the coefficients along the initial vertices.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainComplex {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : ChainComplex (ModuleCat R) ℕ

The chain complex of singular chains of X twisted by the local coefficient system L.

Equations

• L.twistedChainComplex = (AlgebraicTopology.alternatingFaceMapComplex (ModuleCat R)).obj L.twistedChains

noncomputable def TauCeti.LocalCoefficientSystem.ιTwistedChainComplex {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : L.obj (initialVertex σ) ⟶ L.twistedChainComplex.X k

The inclusion into the degree-k term of the twisted chain complex of the coefficient module attached to a singular k-simplex.

Equations

• L.ιTwistedChainComplex k σ = L.ιTwistedChains σ

theorem TauCeti.LocalCoefficientSystem.twistedChainComplex_hom_ext {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {k : ℕ} {A : ModuleCat R} {f g : L.twistedChainComplex.X k ⟶ A} (h : ∀ (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })), CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) f = CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) g) : f = g

Two maps out of a degree of the twisted chain complex agree as soon as they agree on every summand.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplex_hom_ext_iff {R : Type u} [Ring R] {X : TopCat} {L : LocalCoefficientSystem R X} {k : ℕ} {A : ModuleCat R} {f g : L.twistedChainComplex.X k ⟶ A} : f = g ↔ ∀ (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })), CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) f = CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) g

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_d {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k + 1 })) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex (k + 1) σ) (L.twistedChainComplex.d (k + 1) k) = ∑ i : Fin (k + 2), (-1) ^ ↑i • CategoryTheory.CategoryStruct.comp (L.map (vertexTransport (SimplexCategory.δ i).op σ)) (L.ιTwistedChainComplex k ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SimplexCategory.δ i).op)) σ))

The boundary of the twisted chain complex sends the summand of a singular (k + 1)-simplex σ to the alternating sum of the summands of the faces of σ, the coefficients being transported from the initial vertex of σ to the initial vertex of each face.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_d_assoc {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k + 1 })) {Z : ModuleCat R} (h : L.twistedChainComplex.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex (k + 1) σ) (CategoryTheory.CategoryStruct.comp (L.twistedChainComplex.d (k + 1) k) h) = CategoryTheory.CategoryStruct.comp (∑ x : Fin (k + 2), (-1) ^ ↑x • CategoryTheory.CategoryStruct.comp (L.map (vertexTransport (SimplexCategory.δ x).op σ)) (L.ιTwistedChainComplex k ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SimplexCategory.δ x).op)) σ))) h

The boundary of the twisted chain complex sends the summand of a singular (k + 1)-simplex σ to the alternating sum of the summands of the faces of σ, the coefficients being transported from the initial vertex of σ to the initial vertex of each face.

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedHomology {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) : ModuleCat R

Singular homology of X with coefficients in the local coefficient system L.

Equations

• L.twistedHomology k = HomologicalComplex.homology L.twistedChainComplex k

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainsCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) : L.twistedChains ⟶ K.twistedChains

The morphism of twisted chains induced by a morphism of local coefficient systems.

Equations

• TauCeti.LocalCoefficientSystem.twistedChainsCoefficientMap η = { app := TauCeti.LocalCoefficientSystem.twistedChainsCoefficientApp✝ η, naturality := ⋯ }

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) ((twistedChainsCoefficientMap η).app n) = CategoryTheory.CategoryStruct.comp (η.app (initialVertex σ)) (K.ιTwistedChains σ)

A morphism of local coefficient systems acts on the summand of a simplex σ through its component at the initial vertex of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsCoefficientMap_assoc {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) {Z : ModuleCat R} (h : K.twistedChains.obj n ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChains σ) (CategoryTheory.CategoryStruct.comp ((twistedChainsCoefficientMap η).app n) h) = CategoryTheory.CategoryStruct.comp (η.app (initialVertex σ)) (CategoryTheory.CategoryStruct.comp (K.ιTwistedChains σ) h)

A morphism of local coefficient systems acts on the summand of a simplex σ through its component at the initial vertex of σ.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainsFunctor (R : Type u) [Ring R] (X : TopCat) : CategoryTheory.Functor (LocalCoefficientSystem R X) (CategoryTheory.SimplicialObject (ModuleCat R))

Twisted singular chains as a functor of the local coefficient system.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainsCoefficientMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : twistedChainsCoefficientMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id L.twistedChains

The identity morphism of a coefficient system induces the identity of twisted chains.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainsCoefficientMap_comp {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) : twistedChainsCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap η) (twistedChainsCoefficientMap θ)

A composite of morphisms of coefficient systems induces the composite of the two induced morphisms of twisted chains.

theorem TauCeti.LocalCoefficientSystem.twistedChainsCoefficientMap_comp_assoc {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) {Z : CategoryTheory.SimplicialObject (ModuleCat R)} (h : J.twistedChains ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap η) (CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap θ) h)

A composite of morphisms of coefficient systems induces the composite of the two induced morphisms of twisted chains.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) : L.twistedChainComplex ⟶ K.twistedChainComplex

The morphism of twisted chain complexes induced by a morphism of local coefficient systems.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) ((twistedChainComplexCoefficientMap η).f k) = CategoryTheory.CategoryStruct.comp (η.app (initialVertex σ)) (K.ιTwistedChainComplex k σ)

In each degree, a morphism of local coefficient systems acts on the summand of a simplex σ through its component at the initial vertex of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexCoefficientMap_assoc {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) {Z : ModuleCat R} (h : K.twistedChainComplex.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k σ) (CategoryTheory.CategoryStruct.comp ((twistedChainComplexCoefficientMap η).f k) h) = CategoryTheory.CategoryStruct.comp (η.app (initialVertex σ)) (CategoryTheory.CategoryStruct.comp (K.ιTwistedChainComplex k σ) h)

In each degree, a morphism of local coefficient systems acts on the summand of a simplex σ through its component at the initial vertex of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id L.twistedChainComplex

The identity morphism of a coefficient system induces the identity of twisted chain complexes.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap_comp {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) : twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap η) (twistedChainComplexCoefficientMap θ)

A composite of morphisms of coefficient systems induces the composite of the two induced morphisms of twisted chain complexes.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap_comp_assoc {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) {Z : ChainComplex (ModuleCat R) ℕ} (h : J.twistedChainComplex ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap η) (CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap θ) h)

A composite of morphisms of coefficient systems induces the composite of the two induced morphisms of twisted chain complexes.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientIso {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : L.twistedChainComplex ≅ K.twistedChainComplex

An isomorphism of local coefficient systems induces an isomorphism of twisted chain complexes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientIso_hom {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : (twistedChainComplexCoefficientIso e).hom = twistedChainComplexCoefficientMap e.hom

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientIso_inv {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : (twistedChainComplexCoefficientIso e).inv = twistedChainComplexCoefficientMap e.inv

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (k : ℕ) : L.twistedHomology k ⟶ K.twistedHomology k

The map on twisted homology induced by a morphism of local coefficient systems.

Equations

• TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap η k = HomologicalComplex.homologyMap (TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap η) k

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) : twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.id L) k = CategoryTheory.CategoryStruct.id (L.twistedHomology k)

The identity morphism of a coefficient system induces the identity of twisted homology.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap_comp {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) (k : ℕ) : twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) k = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap η k) (twistedHomologyCoefficientMap θ k)

A composite of morphisms of coefficient systems induces the composite of the two induced maps of twisted homology.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap_comp_assoc {R : Type u} [Ring R] {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) (k : ℕ) {Z : ModuleCat R} (h : J.twistedHomology k ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) k) h = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap η k) (CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap θ k) h)

A composite of morphisms of coefficient systems induces the composite of the two induced maps of twisted homology.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainsConstantIso {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) : ((constantFunctor X).obj M).twistedChains ≅ CategoryTheory.Functor.comp (TopCat.toSSet.obj X) (CategoryTheory.Limits.sigmaConst.obj M)

For a constant local coefficient system, twisted chains are the ordinary singular chains.

Equations

• TauCeti.LocalCoefficientSystem.twistedChainsConstantIso X M = CategoryTheory.Iso.refl ((TauCeti.LocalCoefficientSystem.constantFunctor X).obj M).twistedChains

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsConstantIso_hom {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) : CategoryTheory.CategoryStruct.comp (((constantFunctor X).obj M).ιTwistedChains σ) ((twistedChainsConstantIso X M).hom.app n) = CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj n) => M) σ

In each degree, the comparison of twisted chains with ordinary singular chains carries the summand of a simplex σ onto the summand of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsConstantIso_hom_assoc {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) {Z : ModuleCat R} (h : (CategoryTheory.Limits.sigmaConst.obj M).obj ((TopCat.toSSet.obj X).obj n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((constantFunctor X).obj M).ιTwistedChains σ) (CategoryTheory.CategoryStruct.comp ((twistedChainsConstantIso X M).hom.app n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj n) => M) σ) h

In each degree, the comparison of twisted chains with ordinary singular chains carries the summand of a simplex σ onto the summand of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ι_twistedChainsConstantIso_inv {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj n) => M) σ) ((twistedChainsConstantIso X M).inv.app n) = ((constantFunctor X).obj M).ιTwistedChains σ

In each degree, the inverse of the comparison of twisted chains with ordinary singular chains carries the summand of a simplex σ onto the twisted summand of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ι_twistedChainsConstantIso_inv_assoc {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) {Z : ModuleCat R} (h : ((constantFunctor X).obj M).twistedChains.obj n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj n) => M) σ) (CategoryTheory.CategoryStruct.comp ((twistedChainsConstantIso X M).inv.app n) h) = CategoryTheory.CategoryStruct.comp (((constantFunctor X).obj M).ιTwistedChains σ) h

In each degree, the inverse of the comparison of twisted chains with ordinary singular chains carries the summand of a simplex σ onto the twisted summand of σ.

theorem TauCeti.LocalCoefficientSystem.twistedChainsConstantIso_hom_naturality {R : Type u} [Ring R] (X : TopCat) {M N : ModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap ((constantFunctor X).map φ)) (twistedChainsConstantIso X N).hom = CategoryTheory.CategoryStruct.comp (twistedChainsConstantIso X M).hom (CategoryTheory.Functor.whiskerLeft (TopCat.toSSet.obj X) (CategoryTheory.Limits.sigmaConst.map φ))

The comparison of twisted chains with ordinary singular chains is natural in the coefficient module: a morphism of modules acts on the twisted side through the constant systems it induces, and on the singular side summandwise.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) : ((constantFunctor X).obj M).twistedChainComplex ≅ ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).obj X

For a constant local coefficient system, the twisted chain complex is the ordinary singular chain complex with coefficients in the same module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexConstantIso_hom {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : CategoryTheory.CategoryStruct.comp (((constantFunctor X).obj M).ιTwistedChainComplex k σ) ((twistedChainComplexConstantIso X M).hom.f k) = CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) => M) σ

In each degree, the comparison of the twisted chain complex with the ordinary singular chain complex carries the summand of a simplex σ onto the summand of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexConstantIso_hom_assoc {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) {Z : ModuleCat R} (h : (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).obj X).X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (((constantFunctor X).obj M).ιTwistedChainComplex k σ) (CategoryTheory.CategoryStruct.comp ((twistedChainComplexConstantIso X M).hom.f k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) => M) σ) h

In each degree, the comparison of the twisted chain complex with the ordinary singular chain complex carries the summand of a simplex σ onto the summand of σ.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ι_twistedChainComplexConstantIso_inv {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) => M) σ) ((twistedChainComplexConstantIso X M).inv.f k) = ((constantFunctor X).obj M).ιTwistedChainComplex k σ

In each degree, the inverse of the comparison of the twisted chain complex with the ordinary singular chain complex carries the summand of a simplex σ onto the twisted summand of σ.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso_hom_naturality {R : Type u} [Ring R] (X : TopCat) {M N : ModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((constantFunctor X).map φ)) (twistedChainComplexConstantIso X N).hom = CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso X M).hom (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).map φ).app X)

The comparison of the twisted chain complex with the ordinary singular chain complex is natural in the coefficient module.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso_hom_naturality_assoc {R : Type u} [Ring R] (X : TopCat) {M N : ModuleCat R} (φ : M ⟶ N) {Z : ChainComplex (ModuleCat R) ℕ} (h : ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj N).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((constantFunctor X).map φ)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso X N).hom h) = CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso X M).hom (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).map φ).app X) h)

The comparison of the twisted chain complex with the ordinary singular chain complex is natural in the coefficient module.

noncomputable def TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) : ((constantFunctor X).obj M).twistedHomology k ≅ ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj M).obj X

For a constant local coefficient system, twisted homology is ordinary singular homology.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso_hom {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) : (twistedHomologyConstantIso X M k).hom = HomologicalComplex.homologyMap (twistedChainComplexConstantIso X M).hom k

The comparison of twisted homology with ordinary singular homology is the map induced on homology by the comparison of the chain complexes.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso_inv {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (k : ℕ) : (twistedHomologyConstantIso X M k).inv = HomologicalComplex.homologyMap (twistedChainComplexConstantIso X M).inv k

The inverse of the comparison of twisted homology with ordinary singular homology is the map induced on homology by the inverse comparison of the chain complexes.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso_hom_naturality {R : Type u} [Ring R] (X : TopCat) {M N : ModuleCat R} (φ : M ⟶ N) (k : ℕ) : CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap ((constantFunctor X).map φ) k) (twistedHomologyConstantIso X N k).hom = CategoryTheory.CategoryStruct.comp (twistedHomologyConstantIso X M k).hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).map φ).app X)

The comparison of twisted homology with ordinary singular homology is natural in the coefficient module.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainsMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) : ((pullback (TopCat.Hom.hom f)).obj L).twistedChains ⟶ L.twistedChains

The morphism of twisted chains induced by a continuous map, from the chains twisted by the pullback system to the chains twisted by L.

Equations

• TauCeti.LocalCoefficientSystem.twistedChainsMap f L = { app := TauCeti.LocalCoefficientSystem.twistedChainsMapApp✝ f L, naturality := ⋯ }

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) : CategoryTheory.CategoryStruct.comp (((pullback (TopCat.Hom.hom f)).obj L).ιTwistedChains σ) ((twistedChainsMap f L).app n) = L.ιTwistedChains ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) σ)

A continuous map sends the summand of a simplex σ of X identically onto the summand of its image simplex in Y.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChains_twistedChainsMap_assoc {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) {Z : ModuleCat R} (h : L.twistedChains.obj n ⟶ Z) : CategoryTheory.CategoryStruct.comp (((pullback (TopCat.Hom.hom f)).obj L).ιTwistedChains σ) (CategoryTheory.CategoryStruct.comp ((twistedChainsMap f L).app n) h) = CategoryTheory.CategoryStruct.comp (L.ιTwistedChains ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) σ)) h

A continuous map sends the summand of a simplex σ of X identically onto the summand of its image simplex in Y.

noncomputable def TauCeti.LocalCoefficientSystem.twistedChainComplexMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) : ((pullback (TopCat.Hom.hom f)).obj L).twistedChainComplex ⟶ L.twistedChainComplex

The morphism of twisted chain complexes induced by a continuous map.

Equations

• TauCeti.LocalCoefficientSystem.twistedChainComplexMap f L = (AlgebraicTopology.alternatingFaceMapComplex (ModuleCat R)).map (TauCeti.LocalCoefficientSystem.twistedChainsMap f L)

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_congr {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) {g : X ⟶ Y} (h : f = g) : twistedChainComplexMap f L = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap (CategoryTheory.eqToIso ⋯).hom) (twistedChainComplexMap g L)

Equal continuous maps induce the same map on twisted chain complexes, after the canonical identification of their pullback coefficient systems.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : CategoryTheory.CategoryStruct.comp (((pullback (TopCat.Hom.hom f)).obj L).ιTwistedChainComplex k σ) ((twistedChainComplexMap f L).f k) = L.ιTwistedChainComplex k ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := k }))) σ)

In each degree, a continuous map sends the summand of a simplex σ of X identically onto the summand of its image simplex in Y.

@[simp]

theorem TauCeti.LocalCoefficientSystem.ιTwistedChainComplex_twistedChainComplexMap_assoc {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) (k : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) {Z : ModuleCat R} (h : L.twistedChainComplex.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (((pullback (TopCat.Hom.hom f)).obj L).ιTwistedChainComplex k σ) (CategoryTheory.CategoryStruct.comp ((twistedChainComplexMap f L).f k) h) = CategoryTheory.CategoryStruct.comp (L.ιTwistedChainComplex k ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := k }))) σ)) h

In each degree, a continuous map sends the summand of a simplex σ of X identically onto the summand of its image simplex in Y.

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedHomologyMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) (k : ℕ) : ((pullback (TopCat.Hom.hom f)).obj L).twistedHomology k ⟶ L.twistedHomology k

The map on twisted homology induced by a continuous map, from the homology of X twisted by the pullback system to the homology of Y twisted by L.

Equations

• TauCeti.LocalCoefficientSystem.twistedHomologyMap f L k = HomologicalComplex.homologyMap (TauCeti.LocalCoefficientSystem.twistedChainComplexMap f L) k

instance TauCeti.LocalCoefficientSystem.isSplitMono_twistedChainsMap_app {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) [CategoryTheory.Mono f] (k : SimplexCategoryᵒᵖ) : CategoryTheory.IsSplitMono ((twistedChainsMap f L).app k)

The monomorphism of twisted chains induced by a monomorphism of spaces is split in every degree: the retraction keeps the summands of the simplices coming from the subspace and kills the others. This is what makes the twisted chain sequence of a pair stay exact after applying a contravariant Hom(-, M).

instance TauCeti.LocalCoefficientSystem.isSplitMono_twistedChainComplexMap_f {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) [CategoryTheory.Mono f] (k : ℕ) : CategoryTheory.IsSplitMono ((twistedChainComplexMap f L).f k)

A monomorphism of spaces induces a degreewise split monomorphism of twisted chain complexes.

instance TauCeti.LocalCoefficientSystem.mono_twistedChainComplexMap {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (L : LocalCoefficientSystem R Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (twistedChainComplexMap f L)

A monomorphism of spaces induces a monomorphism of twisted chain complexes.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainsMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : twistedChainsMap (CategoryTheory.CategoryStruct.id X) L = twistedChainsCoefficientMap ((pullbackIdIso X).hom.app L)

The identity map induces on twisted chains the map coming from the identification of a coefficient system with its pullback along the identity.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainsMap_comp {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) : twistedChainsMap (CategoryTheory.CategoryStruct.comp f g) L = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)) (CategoryTheory.CategoryStruct.comp (twistedChainsMap f ((pullback (TopCat.Hom.hom g)).obj L)) (twistedChainsMap g L))

A composite of continuous maps induces on twisted chains the composite of the two induced maps, after the identification of the pullback along the composite with the iterated pullback.

theorem TauCeti.LocalCoefficientSystem.twistedChainsMap_comp_assoc {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) {Z✝ : CategoryTheory.SimplicialObject (ModuleCat R)} (h : L.twistedChains ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (twistedChainsMap (CategoryTheory.CategoryStruct.comp f g) L) h = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)) (CategoryTheory.CategoryStruct.comp (twistedChainsMap f ((pullback (TopCat.Hom.hom g)).obj L)) (CategoryTheory.CategoryStruct.comp (twistedChainsMap g L) h))

A composite of continuous maps induces on twisted chains the composite of the two induced maps, after the identification of the pullback along the composite with the iterated pullback.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) : twistedChainComplexMap (CategoryTheory.CategoryStruct.id X) L = twistedChainComplexCoefficientMap ((pullbackIdIso X).hom.app L)

The chain-complex form of twistedChainsMap_id.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_comp {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) : twistedChainComplexMap (CategoryTheory.CategoryStruct.comp f g) L = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((pullback (TopCat.Hom.hom g)).obj L)) (twistedChainComplexMap g L))

The chain-complex form of twistedChainsMap_comp.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_comp_assoc {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) {Z✝ : ChainComplex (ModuleCat R) ℕ} (h : L.twistedChainComplex ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap (CategoryTheory.CategoryStruct.comp f g) L) h = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((pullback (TopCat.Hom.hom g)).obj L)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap g L) h))

The chain-complex form of twistedChainsMap_comp.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedHomologyMap_id {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (k : ℕ) : twistedHomologyMap (CategoryTheory.CategoryStruct.id X) L k = twistedHomologyCoefficientMap ((pullbackIdIso X).hom.app L) k

The homology form of twistedChainsMap_id.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedHomologyMap_comp {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) (k : ℕ) : twistedHomologyMap (CategoryTheory.CategoryStruct.comp f g) L k = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((pullback (TopCat.Hom.hom g)).obj L) k) (twistedHomologyMap g L k))

The homology form of twistedChainsMap_comp.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyMap_comp_assoc {R : Type u} [Ring R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) (k : ℕ) {Z✝ : ModuleCat R} (h : L.twistedHomology k ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap (CategoryTheory.CategoryStruct.comp f g) L k) h = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((pullback (TopCat.Hom.hom g)).obj L) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap g L k) h))

The homology form of twistedChainsMap_comp.

theorem TauCeti.LocalCoefficientSystem.twistedChainsMap_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (twistedChainsMap f L) (twistedChainsCoefficientMap η) = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap ((pullback (TopCat.Hom.hom f)).map η)) (twistedChainsMap f K)

The morphism of twisted chains induced by a continuous map is natural in the coefficient system: pushing simplices forward along f and then applying a morphism of systems on Y is the same as applying the pulled back morphism on X and then pushing forward.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) (twistedChainComplexCoefficientMap η) = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((pullback (TopCat.Hom.hom f)).map η)) (twistedChainComplexMap f K)

The chain-complex form of twistedChainsMap_naturality.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_naturality_assoc {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) {Z : ChainComplex (ModuleCat R) ℕ} (h : K.twistedChainComplex ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) (CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap η) h) = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap ((pullback (TopCat.Hom.hom f)).map η)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f K) h)

The chain-complex form of twistedChainsMap_naturality.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyMap_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) (k : ℕ) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap f L k) (twistedHomologyCoefficientMap η k) = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap ((pullback (TopCat.Hom.hom f)).map η) k) (twistedHomologyMap f K k)

The homology form of twistedChainsMap_naturality.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexMap_naturality_square {R : Type u} [Ring R] {A B C D : TopCat} (a : A ⟶ B) (b : B ⟶ D) (c : A ⟶ C) (d : C ⟶ D) (L : LocalCoefficientSystem R D) (h : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp c d) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap a ((pullback (TopCat.Hom.hom b)).obj L)) (twistedChainComplexMap b L) = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap (((pullbackCompIso (TopCat.Hom.hom a) (TopCat.Hom.hom b)).app L).symm ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ (pullbackCompIso (TopCat.Hom.hom c) (TopCat.Hom.hom d)).app L).hom) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap c ((pullback (TopCat.Hom.hom d)).obj L)) (twistedChainComplexMap d L))

A commutative square of spaces induces a commutative square of twisted chain maps after comparing the two iterated pullbacks of the coefficient system.

theorem TauCeti.LocalCoefficientSystem.twistedChainsConstantIso_hom_space_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (M : ModuleCat R) : CategoryTheory.CategoryStruct.comp (twistedChainsMap f ((constantFunctor Y).obj M)) (twistedChainsConstantIso Y M).hom = CategoryTheory.CategoryStruct.comp (twistedChainsCoefficientMap (pullbackConstantIso (TopCat.Hom.hom f) M).hom) (CategoryTheory.CategoryStruct.comp (twistedChainsConstantIso X M).hom (CategoryTheory.Functor.whiskerRight (TopCat.toSSet.map f) (CategoryTheory.Limits.sigmaConst.obj M)))

The comparison of twisted chains with ordinary singular chains is natural in the space: a continuous map acts on both sides by pushing singular simplices forward, once the pullback of a constant system is identified with the constant system.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso_hom_space_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (M : ModuleCat R) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((constantFunctor Y).obj M)) (twistedChainComplexConstantIso Y M).hom = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap (pullbackConstantIso (TopCat.Hom.hom f) M).hom) (CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso X M).hom (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map f))

The chain-complex form of twistedChainsConstantIso_hom_space_naturality.

theorem TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso_hom_space_naturality_assoc {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (M : ModuleCat R) {Z : ChainComplex (ModuleCat R) ℕ} (h : ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((constantFunctor Y).obj M)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso Y M).hom h) = CategoryTheory.CategoryStruct.comp (twistedChainComplexCoefficientMap (pullbackConstantIso (TopCat.Hom.hom f) M).hom) (CategoryTheory.CategoryStruct.comp (twistedChainComplexConstantIso X M).hom (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map f) h))

The chain-complex form of twistedChainsConstantIso_hom_space_naturality.

theorem TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso_hom_space_naturality {R : Type u} [Ring R] {X Y : TopCat} (f : X ⟶ Y) (M : ModuleCat R) (k : ℕ) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((constantFunctor Y).obj M) k) (twistedHomologyConstantIso Y M k).hom = CategoryTheory.CategoryStruct.comp (twistedHomologyCoefficientMap (pullbackConstantIso (TopCat.Hom.hom f) M).hom k) (CategoryTheory.CategoryStruct.comp (twistedHomologyConstantIso X M k).hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj M).map f))

The homology form of twistedChainsConstantIso_hom_space_naturality.