The DG local system of a fibration

For a continuous map p : E → B and a point b ∈ B, the fibre F' over b of the Moore-path replacement of p carries a strict continuous right action of the Moore loops Ω_b B, (e, γ) · ω = (e, γ · ω). By TauCeti.AlgebraicTopology.Singular.Cubical.MonoidAlgebra.Action, its normalized cubical chains C_*(F') form a right DG module over C_*(Ω_b B): this is the DG local system of p at b (BDHO §7.1). It involves no choice of lifting function, and it is natural in maps over B.

When p comes with a transitive lifting function Φ, the Moore loops act strictly on the fibre F = p⁻¹(b) itself, f · ω = Φ (f, ω)(end), which gives a second DG local system C_*(F)_Φ, and transport F' → F, (e, γ) ↦ Φ (e, γ)(end), is strictly equivariant, so it induces a strict morphism of DG local systems C_*(F') → C_*(F)_Φ.

Main definitions

• TauCeti.fibrationLocalSystem R p b: the DG local system C_*(F') on (B, b).
• TauCeti.fibrationLocalSystemMap R h hh: its naturality along a map h over B.
• TauCeti.liftingLocalSystem R hΦ b: the DG local system C_*(F)_Φ of a transitive lifting function.
• TauCeti.transportLocalSystemHom R hΦ b: the strict morphism C_*(F') → C_*(F)_Φ induced by transport.

Main results

• TauCeti.fibrationLocalSystemMap_id, TauCeti.fibrationLocalSystemMap_comp: functoriality.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.fibrationLocalSystem {E B : Type u} [TopologicalSpace E] [TopologicalSpace B] (R : Type u_1) [CommRing R] (p : C(E, B)) (b : B) : DGLocalSystem B b R

The DG local system of a map p : E → B at b: the normalized cubical chains of the fibre F' of the Moore-path replacement, a right DG module over C_*(Ω_b B; R) through the strict action of the Moore loops.

noncomputable def TauCeti.fibrationLocalSystemMap {E E' B : Type u} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] (R : Type u_1) [CommRing R] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) : fibrationLocalSystem R p b ⟶ fibrationLocalSystem R p' b

The morphism of DG local systems induced by a map h : E → E' over B.

theorem TauCeti.fibrationLocalSystemMap_apply {E E' B : Type u} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] (R : Type u_1) [CommRing R] {p : C(E, B)} {p' : C(E', B)} {b : B} (h : C(E, E')) (hh : p'.comp h = p) (x : (fibrationLocalSystem R p b).carrier) : (fibrationLocalSystemMap R h hh) x = (cubicalChainModuleLinearMap R (MooreReplacement.Fiber.map h hh)) x

The induced morphism is the push-forward of chains along the map of fibres.

@[simp]

theorem TauCeti.fibrationLocalSystemMap_id {E B : Type u} [TopologicalSpace E] [TopologicalSpace B] (R : Type u_1) [CommRing R] (p : C(E, B)) (b : B) : fibrationLocalSystemMap R (ContinuousMap.id E) ⋯ = CategoryTheory.CategoryStruct.id (fibrationLocalSystem R p b)

The identity induces the identity.

theorem TauCeti.fibrationLocalSystemMap_comp {E E' E'' B : Type u} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] (R : Type u_1) [CommRing R] {p : C(E, B)} {p' : C(E', B)} {p'' : C(E'', B)} {b : B} (h : C(E, E')) (h' : C(E', E'')) (hh : p'.comp h = p) (hh' : p''.comp h' = p') : fibrationLocalSystemMap R (h'.comp h) ⋯ = CategoryTheory.CategoryStruct.comp (fibrationLocalSystemMap R h hh) (fibrationLocalSystemMap R h' hh')

A composite of maps over B induces the composite of the induced morphisms.

@[reducible, inline]

noncomputable abbrev TauCeti.liftingLocalSystem {E B : Type u} [TopologicalSpace E] [TopologicalSpace B] {R : Type u_1} [CommRing R] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) : DGLocalSystem B b R

The DG local system C_*(F)_Φ of a transitive lifting function Φ for p at b: the normalized cubical chains of the fibre F = p⁻¹(b), with the strict action of the Moore loops f · ω = Φ (f, ω)(end).

noncomputable def TauCeti.transportLocalSystemHom {E B : Type u} [TopologicalSpace E] [TopologicalSpace B] {R : Type u_1} [CommRing R] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) : fibrationLocalSystem R p b ⟶ liftingLocalSystem hΦ b

Transport as a strict morphism of DG local systems: transport F' → F, (e, γ) ↦ Φ (e, γ)(end), along a transitive lifting function is strictly equivariant, so it induces a morphism C_*(F') → C_*(F)_Φ of right DG modules over C_*(Ω_b B).

theorem TauCeti.transportLocalSystemHom_apply {E B : Type u} [TopologicalSpace E] [TopologicalSpace B] {R : Type u_1} [CommRing R] {p : C(E, B)} {Φ : MooreLiftingFunction p} (hΦ : Φ.IsTransitive) (b : B) (x : (fibrationLocalSystem R p b).carrier) : (transportLocalSystemHom hΦ b) x = (cubicalChainModuleLinearMap R (Φ.transport b)) x

The morphism induced by transport is the push-forward of chains along transport.