Local coefficient systems on topological spaces

A local coefficient system of modules on a space X is a functor from the fundamental groupoid of X to ModuleCat. Thus a path class supplies a linear transport map, and the groupoid laws give all compatibility with concatenation and reversal of paths.

This file provides the categorical operations needed before constructing singular chains with local coefficients: constant systems, pullback along continuous maps, evaluation at a point, path transport, and the monodromy representation of the fundamental group. It also proves that these constructions interact in the expected way. In particular, a morphism of local systems induces an intertwining map on monodromy representations, and transport along a path identifies the monodromy at its endpoints. Homotopic maps have canonically isomorphic pullback functors, with components given by transport along the pointwise paths of the homotopy.

The functorial definition and the monodromy interpretation follow Hatcher, Algebraic Topology, Section 3.H.

@[reducible, inline]

abbrev TauCeti.LocalCoefficientSystem (R : Type u) [Ring R] (X : TopCat) : Type (max v w v (w + 1) u)

An R-module-valued local coefficient system on X is a functor from the fundamental groupoid of X to ModuleCat R.

Equations

• TauCeti.LocalCoefficientSystem R X = CategoryTheory.Functor (FundamentalGroupoid ↑X) (ModuleCat R)

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

The constant local coefficient system with fibre M.

Equations

• TauCeti.LocalCoefficientSystem.constantFunctor X = CategoryTheory.Functor.const (FundamentalGroupoid ↑X)

@[simp]

theorem TauCeti.LocalCoefficientSystem.constantFunctor_obj_obj {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (x : FundamentalGroupoid ↑X) : ((constantFunctor X).obj M).obj x = M

@[simp]

theorem TauCeti.LocalCoefficientSystem.constantFunctor_obj_map {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) {x y : FundamentalGroupoid ↑X} (p : x ⟶ y) : ((constantFunctor X).obj M).map p = CategoryTheory.CategoryStruct.id M

@[simp]

theorem TauCeti.LocalCoefficientSystem.constantFunctor_map_app {R : Type u} [Ring R] (X : TopCat) {M N : ModuleCat R} (f : M ⟶ N) (x : FundamentalGroupoid ↑X) : ((constantFunctor X).map f).app x = f

noncomputable def TauCeti.LocalCoefficientSystem.pullback {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) : CategoryTheory.Functor (LocalCoefficientSystem R Y) (LocalCoefficientSystem R X)

Pull back local coefficient systems along a continuous map.

Equations

• TauCeti.LocalCoefficientSystem.pullback f = (CategoryTheory.Functor.whiskeringLeft (FundamentalGroupoid ↑X) (FundamentalGroupoid ↑Y) (ModuleCat R)).obj (FundamentalGroupoid.map f)

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullback_obj_obj {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (x : FundamentalGroupoid ↑X) : ((pullback f).obj L).obj x = L.obj ((FundamentalGroupoid.map f).obj x)

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullback_obj_map {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) {x y : FundamentalGroupoid ↑X} (p : x ⟶ y) : ((pullback f).obj L).map p = L.map ((FundamentalGroupoid.map f).map p)

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullback_map_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) (x : FundamentalGroupoid ↑X) : ((pullback f).map η).app x = η.app ((FundamentalGroupoid.map f).obj x)

noncomputable def TauCeti.LocalCoefficientSystem.pullbackIdIso {R : Type u} [Ring R] (X : TopCat) : pullback (ContinuousMap.id ↑X) ≅ CategoryTheory.Functor.id (LocalCoefficientSystem R X)

Pullback along the identity map is naturally isomorphic to the identity functor.

Equations

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackIdIso_hom_app_app {R : Type u} [Ring R] (X : TopCat) (L : LocalCoefficientSystem R X) (x : FundamentalGroupoid ↑X) : ((pullbackIdIso X).hom.app L).app x = CategoryTheory.CategoryStruct.id (((pullback (ContinuousMap.id ↑X)).obj L).obj x)

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackIdIso_inv_app_app {R : Type u} [Ring R] (X : TopCat) (L : LocalCoefficientSystem R X) (x : FundamentalGroupoid ↑X) : ((pullbackIdIso X).inv.app L).app x = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (LocalCoefficientSystem R X)).obj L).obj x)

noncomputable def TauCeti.LocalCoefficientSystem.pullbackCompIso {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {Z : TopCat} (f : C(↑X, ↑Y)) (g : C(↑Y, ↑Z)) : pullback (g.comp f) ≅ (pullback g).comp (pullback f)

Pullback along a composite is naturally isomorphic to the composite of the two pullback functors, in contravariant order.

Equations

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackCompIso_hom_app_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {Z : TopCat} (f : C(↑X, ↑Y)) (g : C(↑Y, ↑Z)) (L : LocalCoefficientSystem R Z) (x : FundamentalGroupoid ↑X) : ((pullbackCompIso f g).hom.app L).app x = CategoryTheory.CategoryStruct.id (((pullback (g.comp f)).obj L).obj x)

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackCompIso_inv_app_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {Z : TopCat} (f : C(↑X, ↑Y)) (g : C(↑Y, ↑Z)) (L : LocalCoefficientSystem R Z) (x : FundamentalGroupoid ↑X) : ((pullbackCompIso f g).inv.app L).app x = CategoryTheory.CategoryStruct.id ((((pullback g).comp (pullback f)).obj L).obj x)

noncomputable def TauCeti.LocalCoefficientSystem.pullbackConstantIso {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (M : ModuleCat R) : (pullback f).obj ((constantFunctor Y).obj M) ≅ (constantFunctor X).obj M

Pulling back a constant local coefficient system leaves it constant.

Equations

• TauCeti.LocalCoefficientSystem.pullbackConstantIso f M = CategoryTheory.Iso.refl ((TauCeti.LocalCoefficientSystem.pullback f).obj ((TauCeti.LocalCoefficientSystem.constantFunctor Y).obj M))

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackConstantIso_hom_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (M : ModuleCat R) (x : FundamentalGroupoid ↑X) : (pullbackConstantIso f M).hom.app x = CategoryTheory.CategoryStruct.id M

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackConstantIso_inv_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (M : ModuleCat R) (x : FundamentalGroupoid ↑X) : (pullbackConstantIso f M).inv.app x = CategoryTheory.CategoryStruct.id M

noncomputable def TauCeti.LocalCoefficientSystem.pullbackHomotopyIso {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) : pullback f ≅ pullback g

Pullback of local coefficient systems along homotopic maps gives naturally isomorphic systems. At a point x, the comparison is transport by the path t ↦ H (t, x) traced by the homotopy.

Equations

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackHomotopyIso_hom_app_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) (L : LocalCoefficientSystem R Y) (x : FundamentalGroupoid ↑X) : ((pullbackHomotopyIso H).hom.app L).app x = L.map ⟦H.evalAt x.as⟧

At a point, the pullback comparison acts by the local system on the path traced by the homotopy.

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullbackHomotopyIso_inv_app_app {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) (L : LocalCoefficientSystem R Y) (x : FundamentalGroupoid ↑X) : ((pullbackHomotopyIso H).inv.app L).app x = L.map ⟦(H.evalAt x.as).symm⟧

At a point, the inverse pullback comparison acts by the local system on the reversed path traced by the homotopy.

noncomputable def TauCeti.LocalCoefficientSystem.fiberFunctor (R : Type u) [Ring R] (X : TopCat) (x : ↑X) : CategoryTheory.Functor (LocalCoefficientSystem R X) (ModuleCat R)

Evaluation of a local coefficient system at a point of the space.

Equations

• TauCeti.LocalCoefficientSystem.fiberFunctor R X x = (CategoryTheory.evaluation (FundamentalGroupoid ↑X) (ModuleCat R)).obj { as := x }

@[simp]

theorem TauCeti.LocalCoefficientSystem.fiberFunctor_obj {R : Type u} [Ring R] {X : TopCat} (x : ↑X) (L : LocalCoefficientSystem R X) : (fiberFunctor R X x).obj L = L.obj { as := x }

@[simp]

theorem TauCeti.LocalCoefficientSystem.fiberFunctor_map {R : Type u} [Ring R] {X : TopCat} (x : ↑X) {L K : LocalCoefficientSystem R X} (η : L ⟶ K) : (fiberFunctor R X x).map η = η.app { as := x }

noncomputable def TauCeti.LocalCoefficientSystem.transport {R : Type u} [Ring R] {X : TopCat} {x y : ↑X} (L : LocalCoefficientSystem R X) (p : Path.Homotopic.Quotient x y) : ↑(L.obj { as := x }) ≃ₗ[R] ↑(L.obj { as := y })

Parallel transport along a path class, as a linear equivalence between the endpoint fibres.

Equations

• L.transport p = (CategoryTheory.Functor.mapIso L ((CategoryTheory.Groupoid.isoEquivHom { as := x } { as := y }).symm p)).toLinearEquiv

@[simp]

theorem TauCeti.LocalCoefficientSystem.transport_apply {R : Type u} [Ring R] {X : TopCat} {x y : ↑X} (L : LocalCoefficientSystem R X) (p : Path.Homotopic.Quotient x y) (a : ↑(L.obj { as := x })) : (L.transport p) a = (CategoryTheory.ConcreteCategory.hom (L.map p)) a

@[simp]

theorem TauCeti.LocalCoefficientSystem.transport_refl {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (x : ↑X) : L.transport (Path.Homotopic.Quotient.refl x) = LinearEquiv.refl R ↑(L.obj { as := x })

Transport along the constant path is the identity.

@[simp]

theorem TauCeti.LocalCoefficientSystem.transport_trans {R : Type u} [Ring R] {X : TopCat} {x y z : ↑X} (L : LocalCoefficientSystem R X) (p : Path.Homotopic.Quotient x y) (q : Path.Homotopic.Quotient y z) : L.transport (p.trans q) = L.transport p ≪≫ₗ L.transport q

Transport along a concatenation of paths is the composite of the two transports.

@[simp]

theorem TauCeti.LocalCoefficientSystem.transport_symm {R : Type u} [Ring R] {X : TopCat} {x y : ↑X} (L : LocalCoefficientSystem R X) (p : Path.Homotopic.Quotient x y) : L.transport p.symm = (L.transport p).symm

Transport along the reversed path is the inverse of transport along the path.

theorem TauCeti.LocalCoefficientSystem.transport_naturality {R : Type u} [Ring R] {X : TopCat} {x y : ↑X} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (p : Path.Homotopic.Quotient x y) (a : ↑(L.obj { as := x })) : (CategoryTheory.ConcreteCategory.hom (η.app { as := y })) ((L.transport p) a) = (K.transport p) ((CategoryTheory.ConcreteCategory.hom (η.app { as := x })) a)

Transport commutes with a morphism of local coefficient systems.

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullback_transport {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) {x y : ↑X} (p : Path.Homotopic.Quotient x y) : ((pullback f).obj L).transport p = L.transport (p.map f)

Pullback transport is transport along the image path.

def TauCeti.LocalCoefficientSystem.monodromyRepresentation {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (x : ↑X) : Representation R (FundamentalGroup (↑X) x) ↑(L.obj { as := x })

The monodromy representation of a local coefficient system at a basepoint.

Equations

• L.monodromyRepresentation x = { toFun := fun (g : FundamentalGroup (↑X) x) => ModuleCat.Hom.hom (L.map g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.LocalCoefficientSystem.monodromyRepresentation_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) (x : ↑X) (g : FundamentalGroup (↑X) x) (a : ↑(L.obj { as := x })) : ((L.monodromyRepresentation x) g) a = (CategoryTheory.ConcreteCategory.hom (L.map g)) a

@[simp]

theorem TauCeti.LocalCoefficientSystem.constant_monodromyRepresentation {R : Type u} [Ring R] (X : TopCat) (M : ModuleCat R) (x : ↑X) : ((constantFunctor X).obj M).monodromyRepresentation x = Representation.trivial R (FundamentalGroup (↑X) x) ↑M

The monodromy representation of a constant local coefficient system is trivial.

@[simp]

theorem TauCeti.LocalCoefficientSystem.pullback_monodromyRepresentation {R : Type u} [Ring R] {X : TopCat} {Y : TopCat} (f : C(↑X, ↑Y)) (L : LocalCoefficientSystem R Y) (x : ↑X) : ((pullback f).obj L).monodromyRepresentation x = MonoidHom.comp (L.monodromyRepresentation (f x)) (FundamentalGroup.map f x)

The monodromy representation of a pullback is the monodromy representation at the image point, restricted along the induced map of fundamental groups.

def TauCeti.LocalCoefficientSystem.monodromyMap {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (x : ↑X) : (L.monodromyRepresentation x).IntertwiningMap (K.monodromyRepresentation x)

A morphism of local coefficient systems induces an intertwining map between the monodromy representations on each fibre.

Equations

• TauCeti.LocalCoefficientSystem.monodromyMap η x = { toLinearMap := ModuleCat.Hom.hom (η.app { as := x }), isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.LocalCoefficientSystem.monodromyMap_apply {R : Type u} [Ring R] {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (x : ↑X) (a : ↑(L.obj { as := x })) : (monodromyMap η x) a = (CategoryTheory.ConcreteCategory.hom (η.app { as := x })) a

noncomputable def TauCeti.LocalCoefficientSystem.monodromyFunctor (R : Type u) [Ring R] (X : TopCat) (x : ↑X) : CategoryTheory.Functor (LocalCoefficientSystem R X) (Rep R (FundamentalGroup (↑X) x))

Evaluation at a basepoint, equipped with monodromy, is a functor from local coefficient systems to representations of the fundamental group.

Equations

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

@[simp]

theorem TauCeti.LocalCoefficientSystem.monodromyFunctor_obj_V {R : Type u} [Ring R] {X : TopCat} (x : ↑X) (L : LocalCoefficientSystem R X) : ↑((monodromyFunctor R X x).obj L) = ↑(L.obj { as := x })

@[simp]

theorem TauCeti.LocalCoefficientSystem.monodromyFunctor_obj_ρ {R : Type u} [Ring R] {X : TopCat} (x : ↑X) (L : LocalCoefficientSystem R X) : ((monodromyFunctor R X x).obj L).ρ = L.monodromyRepresentation x

@[simp]

theorem TauCeti.LocalCoefficientSystem.monodromyFunctor_map_hom {R : Type u} [Ring R] {X : TopCat} (x : ↑X) {L K : LocalCoefficientSystem R X} (η : L ⟶ K) : Rep.Hom.hom ((monodromyFunctor R X x).map η) = monodromyMap η x

noncomputable def TauCeti.LocalCoefficientSystem.basepointChangeEquiv {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {x y : ↑X} (p : Path x y) : (L.monodromyRepresentation x).Equiv (MonoidHom.comp (L.monodromyRepresentation y) (FundamentalGroup.fundamentalGroupMulEquivOfPath p).toMonoidHom)

Transport along a path intertwines monodromy after changing the basepoint along that path.

Equations

• L.basepointChangeEquiv p = Representation.Equiv.mk (L.transport ⟦p⟧) ⋯

@[simp]

theorem TauCeti.LocalCoefficientSystem.basepointChangeEquiv_apply {R : Type u} [Ring R] {X : TopCat} (L : LocalCoefficientSystem R X) {x y : ↑X} (p : Path x y) (a : ↑(L.obj { as := x })) : (L.basepointChangeEquiv p) a = (L.transport ⟦p⟧) a