DG local systems

A DG local system on a pointed space (B, b) is a right differential graded module over the chain algebra C_*(Ω_b B; R) of the Moore loop space (the source's Definition 1.8); they form the category DGLocalSystem B b R of right DG modules over that DG algebra. For a path-connected space this is the notion of local coefficients used for Morse and Floer homology with DG coefficients.

The pullback along a based map f : (B, b) → (B', b') is restriction of scalars along the DG algebra morphism C_*(Ωf) of TauCeti.AlgebraicTopology.DGLocalSystem.LoopAlgebra. It is functorial up to the canonical isomorphisms: the pullback along the identity is isomorphic to the identity functor, and the pullback along a composite to the composite of the pullbacks.

For a space that is not path-connected, one chooses a basepoint b_c in each path component c (TauCeti.PathComponentBasepoints), and a DG local system is a family (𝓕_c) of DG local systems on the pointed spaces (B, b_c) (DGLocalSystemFamily). A map f : B' → B that sends each chosen basepoint of B' to the chosen basepoint of the path component of its image pulls such families back component by component (DGLocalSystemFamily.pullback), again functorially up to the canonical isomorphisms. Basepoint change, and hence the pullback along maps that do not preserve the chosen basepoints, needs the derived tensor product and is not treated here.

Main definitions

• TauCeti.DGLocalSystem B b R: DG local systems on (B, b).
• TauCeti.DGLocalSystem.pullback R f hf: the pullback along a based map.
• TauCeti.DGLocalSystem.pullbackId, TauCeti.DGLocalSystem.pullbackComp: its functoriality.
• TauCeti.DGLocalSystemFamily β R: DG local systems on a space with chosen basepoints.
• TauCeti.DGLocalSystemFamily.pullback R f hf: their pullback along a map preserving the chosen basepoints, with pullbackId and pullbackComp.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.4, Definition 1.8.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, Chapters 2 and 7.

@[reducible, inline]

abbrev TauCeti.DGLocalSystem (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2) [CommRing R] : Type (max (max (uM + 1) u_1 u_2) u_2)

The category of DG local systems on a pointed space (B, b): right differential graded modules over the chain algebra C_*(Ω_b B; R) of the Moore loop space.

@[reducible, inline]

noncomputable abbrev TauCeti.DGLocalSystem.pullback {B : Type u_1} {B' : Type u_2} [TopologicalSpace B] [TopologicalSpace B'] {b : B} {b' : B'} (R : Type u_4) [CommRing R] (f : C(B, B')) (hf : f b = b') : CategoryTheory.Functor (DGLocalSystem B' b' R) (DGLocalSystem B b R)

The pullback of DG local systems along a based map f : (B, b) → (B', b'): restriction of scalars along C_*(Ωf) : C_*(Ω_b B) → C_*(Ω_{b'} B').

noncomputable def TauCeti.DGLocalSystem.pullbackId {B : Type u_1} [TopologicalSpace B] {b : B} (R : Type u_4) [CommRing R] : pullback R (ContinuousMap.id B) ⋯ ≅ CategoryTheory.Functor.id (DGLocalSystem B b R)

The pullback along the identity is isomorphic to the identity functor.

@[simp]

theorem TauCeti.DGLocalSystem.pullbackId_hom_app {B : Type u_1} [TopologicalSpace B] {b : B} (R : Type u_4) [CommRing R] (M : DGLocalSystem B b R) : (pullbackId R).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (DGRightModuleCat.restrictScalarsIdApp M).hom

The component of pullbackId at M.

@[simp]

theorem TauCeti.DGLocalSystem.pullbackId_inv_app {B : Type u_1} [TopologicalSpace B] {b : B} (R : Type u_4) [CommRing R] (M : DGLocalSystem B b R) : (pullbackId R).inv.app M = CategoryTheory.CategoryStruct.comp (DGRightModuleCat.restrictScalarsIdApp M).inv (CategoryTheory.eqToHom ⋯)

The component of the inverse of pullbackId at M.

noncomputable def TauCeti.DGLocalSystem.pullbackComp {B : Type u_1} {B' : Type u_2} {B'' : Type u_3} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace B''] {b : B} {b' : B'} {b'' : B''} (R : Type u_4) [CommRing R] (g : C(B', B'')) (f : C(B, B')) (hg : g b' = b'') (hf : f b = b') : pullback R (g.comp f) ⋯ ≅ (pullback R g hg).comp (pullback R f hf)

The pullback along a composite is isomorphic to the composite of the pullbacks.

@[simp]

theorem TauCeti.DGLocalSystem.pullbackComp_hom_app {B : Type u_1} {B' : Type u_2} {B'' : Type u_3} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace B''] {b : B} {b' : B'} {b'' : B''} (R : Type u_4) [CommRing R] (g : C(B', B'')) (f : C(B, B')) (hg : g b' = b'') (hf : f b = b') (M : DGLocalSystem B'' b'' R) : (pullbackComp R g f hg hf).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (DGRightModuleCat.restrictScalarsCompApp (loopChainMap R f hf) (loopChainMap R g hg) M).hom

The component of pullbackComp at M.

@[simp]

theorem TauCeti.DGLocalSystem.pullbackComp_inv_app {B : Type u_1} {B' : Type u_2} {B'' : Type u_3} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace B''] {b : B} {b' : B'} {b'' : B''} (R : Type u_4) [CommRing R] (g : C(B', B'')) (f : C(B, B')) (hg : g b' = b'') (hf : f b = b') (M : DGLocalSystem B'' b'' R) : (pullbackComp R g f hg hf).inv.app M = CategoryTheory.CategoryStruct.comp (DGRightModuleCat.restrictScalarsCompApp (loopChainMap R f hf) (loopChainMap R g hg) M).inv (CategoryTheory.eqToHom ⋯)

The component of the inverse of pullbackComp at M.

@[reducible, inline]

abbrev TauCeti.DGLocalSystemFamily {B : Type u_1} [TopologicalSpace B] (β : PathComponentBasepoints B) (R : Type u_2) [CommRing R] : Type (max (max (uM + 1) u_1) u_2)

The category of DG local systems on a space with chosen basepoints: families (𝓕_c) indexed by the path components c, with 𝓕_c a DG local system on (B, b_c).

@[instance_reducible]

noncomputable instance TauCeti.instCategoryDGLocalSystemFamily {B : Type u_1} [TopologicalSpace B] (β : PathComponentBasepoints B) (R : Type u_2) [CommRing R] : CategoryTheory.Category.{max u_1 uM, max (max (uM + 1) u_2) u_1} (DGLocalSystemFamily β R)

The category structure on families: componentwise (the product of the categories of DG local systems at the chosen basepoints).

noncomputable def TauCeti.DGLocalSystemFamily.pullback {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} (f : C(B', B)) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) : CategoryTheory.Functor (DGLocalSystemFamily β R) (DGLocalSystemFamily β' R)

The pullback of DG local systems along a map f : B' → B sending each chosen basepoint b'_{c'} of B' to the chosen basepoint of the path component of f (b'_{c'}): componentwise, the pullback of the based map f : (B', b'_{c'}) → (B, b_{f(c')}).

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullback_obj {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} (f : C(B', B)) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) (𝓕 : DGLocalSystemFamily β R) (c' : ZerothHomotopy B') : (pullback R f hf).obj 𝓕 c' = (DGLocalSystem.pullback R f ⋯).obj (𝓕 (ZerothHomotopy.mk (f (β'.point c'))))

The component of the pullback of a family at c' is the pullback of the component at the path component of f (b'_{c'}).

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullback_map {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} (f : C(B', B)) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) {𝓕 𝓖 : DGLocalSystemFamily β R} (φ : 𝓕 ⟶ 𝓖) (c' : ZerothHomotopy B') : (pullback R f hf).map φ c' = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((DGLocalSystem.pullback R f ⋯).map (φ (ZerothHomotopy.mk (f (β'.point c'))))) (CategoryTheory.eqToHom ⋯))

The component of the pullback of a morphism of families at c'.

noncomputable def TauCeti.DGLocalSystemFamily.pullbackIdApp {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {c₁ c : ZerothHomotopy B} (h : c₁ = c) (hb : (ContinuousMap.id B) (β.point c) = β.point c₁) (𝓕 : DGLocalSystemFamily β R) : (DGLocalSystem.pullback R (ContinuousMap.id B) hb).obj (𝓕 c₁) ≅ 𝓕 c

The component of pullbackId, for an index c₁ equal to c (transport along h).

theorem TauCeti.DGLocalSystemFamily.pullbackIdApp_naturality {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {c₁ c : ZerothHomotopy B} (h : c₁ = c) (hb : (ContinuousMap.id B) (β.point c) = β.point c₁) {𝓕 𝓖 : DGLocalSystemFamily β R} (φ : 𝓕 ⟶ 𝓖) : CategoryTheory.CategoryStruct.comp ((DGLocalSystem.pullback R (ContinuousMap.id B) hb).map (φ c₁)) (pullbackIdApp R h hb 𝓖).hom = CategoryTheory.CategoryStruct.comp (pullbackIdApp R h hb 𝓕).hom (φ c)

Naturality of pullbackIdApp in the family.

noncomputable def TauCeti.DGLocalSystemFamily.pullbackId {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] : pullback R (ContinuousMap.id B) ⋯ ≅ CategoryTheory.Functor.id (DGLocalSystemFamily β R)

The pullback of families along the identity is isomorphic to the identity functor.

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullbackId_hom_app {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] (𝓕 : DGLocalSystemFamily β R) (c : ZerothHomotopy B) : (pullbackId R).hom.app 𝓕 c = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (pullbackIdApp R ⋯ ⋯ 𝓕).hom

The component of pullbackId at a family 𝓕 and a path component c.

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullbackId_inv_app {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] (𝓕 : DGLocalSystemFamily β R) (c : ZerothHomotopy B) : (pullbackId R).inv.app 𝓕 c = CategoryTheory.CategoryStruct.comp (pullbackIdApp R ⋯ ⋯ 𝓕).inv (CategoryTheory.eqToHom ⋯)

The component of the inverse of pullbackId at a family 𝓕 and a path component c.

noncomputable def TauCeti.DGLocalSystemFamily.pullbackCompApp {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {B'' : Type u_4} [TopologicalSpace B''] {β'' : PathComponentBasepoints B''} (g : C(B, B'')) (f : C(B', B)) {y : B'} {x : B} {c' c : ZerothHomotopy B''} (h : c' = c) (hf : f y = x) (hg : g x = β''.point c) (hgf : (g.comp f) y = β''.point c') (𝓕 : DGLocalSystemFamily β'' R) : (DGLocalSystem.pullback R (g.comp f) hgf).obj (𝓕 c') ≅ (DGLocalSystem.pullback R f hf).obj ((DGLocalSystem.pullback R g hg).obj (𝓕 c))

The component of pullbackComp, for indices c' = c (transport along h).

theorem TauCeti.DGLocalSystemFamily.pullbackCompApp_naturality {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {B'' : Type u_4} [TopologicalSpace B''] {β'' : PathComponentBasepoints B''} (g : C(B, B'')) (f : C(B', B)) {y : B'} {x : B} {c' c : ZerothHomotopy B''} (h : c' = c) (hf : f y = x) (hg : g x = β''.point c) (hgf : (g.comp f) y = β''.point c') {𝓕 𝓖 : DGLocalSystemFamily β'' R} (φ : 𝓕 ⟶ 𝓖) : CategoryTheory.CategoryStruct.comp ((DGLocalSystem.pullback R (g.comp f) hgf).map (φ c')) (pullbackCompApp R g f h hf hg hgf 𝓖).hom = CategoryTheory.CategoryStruct.comp (pullbackCompApp R g f h hf hg hgf 𝓕).hom ((DGLocalSystem.pullback R f hf).map ((DGLocalSystem.pullback R g hg).map (φ c)))

Naturality of pullbackCompApp in the family.

noncomputable def TauCeti.DGLocalSystemFamily.pullbackComp {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} {B'' : Type u_4} [TopologicalSpace B''] {β'' : PathComponentBasepoints B''} (g : C(B, B'')) (f : C(B', B)) (hg : ∀ (c : ZerothHomotopy B), g (β.point c) = β''.point (ZerothHomotopy.mk (g (β.point c)))) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) : pullback R (g.comp f) ⋯ ≅ (pullback R g hg).comp (pullback R f hf)

The pullback of families along a composite is isomorphic to the composite of the pullbacks.

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullbackComp_hom_app {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} {B'' : Type u_4} [TopologicalSpace B''] {β'' : PathComponentBasepoints B''} (g : C(B, B'')) (f : C(B', B)) (hg : ∀ (c : ZerothHomotopy B), g (β.point c) = β''.point (ZerothHomotopy.mk (g (β.point c)))) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) (𝓕 : DGLocalSystemFamily β'' R) (c' : ZerothHomotopy B') : (pullbackComp R g f hg hf).hom.app 𝓕 c' = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (pullbackCompApp R g f ⋯ ⋯ ⋯ ⋯ 𝓕).hom (CategoryTheory.eqToHom ⋯))

The component of pullbackComp at a family 𝓕 and a path component c'.

@[simp]

theorem TauCeti.DGLocalSystemFamily.pullbackComp_inv_app {B : Type u_1} [TopologicalSpace B] {β : PathComponentBasepoints B} (R : Type u_2) [CommRing R] {B' : Type u_3} [TopologicalSpace B'] {β' : PathComponentBasepoints B'} {B'' : Type u_4} [TopologicalSpace B''] {β'' : PathComponentBasepoints B''} (g : C(B, B'')) (f : C(B', B)) (hg : ∀ (c : ZerothHomotopy B), g (β.point c) = β''.point (ZerothHomotopy.mk (g (β.point c)))) (hf : ∀ (c' : ZerothHomotopy B'), f (β'.point c') = β.point (ZerothHomotopy.mk (f (β'.point c')))) (𝓕 : DGLocalSystemFamily β'' R) (c' : ZerothHomotopy B') : (pullbackComp R g f hg hf).inv.app 𝓕 c' = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (pullbackCompApp R g f ⋯ ⋯ ⋯ ⋯ 𝓕).inv (CategoryTheory.eqToHom ⋯))

The component of the inverse of pullbackComp at a family 𝓕 and a path component c'.