def CoveringSpaces.IsCoveringSpace {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] (p : E → B) : Prop

(Definition 31.1) A continuous map p : E → B is a covering space if every point preimage is discrete and every b ∈ B has a neighborhood V so that p⁻¹(V) splits homeomorphically as V × p⁻¹(b) over V. Defined here as IsCoveringMap p.

def CoveringSpaces.IsPrincipalAction (π : Type u_3) (X : Type u_4) [Group π] [TopologicalSpace X] [MulAction π X] : Prop

(Definition 31.3) The action of a group π on a space X is principal (equivalently, totally discontinuous) if every x has a neighborhood U such that gU ∩ U ≠ ∅ forces g = 1.

theorem CoveringSpaces.IsPrincipalAction.isQuotientCoveringMap {π : Type u_3} {X : Type u_4} [Group π] [TopologicalSpace X] [MulAction π X] [ContinuousConstSMul π X] (h : IsPrincipalAction π X) : IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel π X)) π

Packaging of a principal action as a IsQuotientCoveringMap for the orbit projection, used to derive that the orbit projection is a covering map.

theorem CoveringSpaces.isCoveringMap_orbitProjection_of_principalAction {π : Type u_3} {X : Type u_4} [Group π] [TopologicalSpace X] [MulAction π X] [ContinuousConstSMul π X] (h : IsPrincipalAction π X) : IsCoveringMap (Quotient.mk (MulAction.orbitRel π X))

(Lemma 31.4) If π acts principally on X then the orbit projection X → π\X is a covering space.

theorem CoveringSpaces.unique_path_lifting {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsCoveringMap p) (γ : C(↑unitInterval, B)) (e : E) (he : γ 0 = p e) : ∃! Γ : C(↑unitInterval, E), p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

(Theorem 31.5, Unique path lifting) For any covering space p : E → B, path γ : I → B in the base, and e ∈ E with p e = γ 0, there is a unique lift Γ : I → E with p ∘ Γ = γ and Γ 0 = e.

class CoveringSpaces.IsSemiLocallySimplyConnected (B : Type u) [TopologicalSpace B] : Prop

A typeclass asserting that B is path connected and semi-locally simply connected: every point has arbitrarily small neighborhoods V whose loops at the basepoint become null-homotopic in B. Hypothesis used in the classification of covering spaces.

• pathConnected : PathConnectedSpace B
• semilocal (b : B) (U : Set B) : U ∈ nhds b → ∃ V ∈ nhds b, V ⊆ U ∧ ∀ (hb : b ∈ V) (γ : Path ⟨b, hb⟩ ⟨b, hb⟩), (γ.map ⋯).Homotopic (Path.refl b)

structure CoveringSpaces.CoveringSpaceOver (B : Type u) [TopologicalSpace B] : Type (u + 1)

The data of a covering space over a fixed base B: a total space E together with its topology, a continuous projection proj : E → B, and a proof that proj is a covering map.

• E : Type u
• topE : TopologicalSpace self.E
• proj : self.E → B
• continuous_proj : Continuous self.proj
• isCoveringMap : IsCoveringMap self.proj

structure CoveringSpaces.CoveringSpaceOver.Hom {B : Type u} [TopologicalSpace B] (E₁ E₂ : CoveringSpaceOver B) : Type u

A morphism of covering spaces over B: a continuous map between the total spaces that commutes with the projections.

• toFun : E₁.E → E₂.E
• continuous_toFun : Continuous self.toFun
• proj_comm : E₂.proj ∘ self.toFun = E₁.proj

@[implicit_reducible]

instance CoveringSpaces.coveringSpaceOverCategory {B : Type u} [TopologicalSpace B] : CategoryTheory.Category.{u, u + 1} (CoveringSpaceOver B)

The category Cov_B of covering spaces over B, with morphisms given by projection-preserving continuous maps.

noncomputable def CoveringSpaces.fiberAction {B : Type u} [TopologicalSpace B] (b : B) {E : Type u} [TopologicalSpace E] {p : E → B} (cov : IsCoveringMap p) : FundamentalGroup B b →* CategoryTheory.End (cov.monodromyFunctor.obj { as := b })

The monodromy action of π₁(B, b) on the fiber p⁻¹(b), realised as a group homomorphism into the endomorphism monoid of the fiber under the monodromy functor.

noncomputable def CoveringSpaces.fiberActionObj {B : Type u} [TopologicalSpace B] (b : B) (covSpace : CoveringSpaceOver B) : Action (Type u) (FundamentalGroup B b)

The fiber of a covering space over b packaged as a π₁(B, b)-set via the monodromy action.

theorem CoveringSpaces.liftPath_comp_covMorphism {E₁ E₂ B' : Type u} {t₁ : TopologicalSpace E₁} {t₂ : TopologicalSpace E₂} [TopologicalSpace B'] {p₁ : E₁ → B'} {p₂ : E₂ → B'} (cov₁ : IsCoveringMap p₁) (cov₂ : IsCoveringMap p₂) (f : E₁ → E₂) (hf_cont : Continuous f) (hf_comm : p₂ ∘ f = p₁) (γ : C(↑unitInterval, B')) (e : E₁) (he : γ 0 = p₁ e) : { toFun := f, continuous_toFun := hf_cont }.comp (cov₁.liftPath γ e he) = cov₂.liftPath γ (f e) ⋯

A morphism of covering spaces over B' commutes with path lifting: postcomposing the lift of a path in E₁ by the morphism f : E₁ → E₂ gives the lift of the same path starting at f e.

theorem CoveringSpaces.fiberMap_monodromy_comm {E₁ E₂ B' : Type u} {t₁ : TopologicalSpace E₁} {t₂ : TopologicalSpace E₂} [TopologicalSpace B'] {p₁ : E₁ → B'} {p₂ : E₂ → B'} (cov₁ : IsCoveringMap p₁) (cov₂ : IsCoveringMap p₂) (f : E₁ → E₂) (hf_cont : Continuous f) (hf_comm : p₂ ∘ f = p₁) {b : B'} (γ : Path.Homotopic.Quotient b b) (e : ↑(p₁ ⁻¹' {b})) : f ↑(cov₁.monodromy γ e) = ↑(cov₂.monodromy γ ⟨f ↑e, ⋯⟩)

Equivariance of the fiber map induced by a morphism of covering spaces: the map f : E₁ → E₂ intertwines the monodromy actions of π₁(B', b) on the fibers p₁⁻¹(b) and p₂⁻¹(b).

noncomputable def CoveringSpaces.fiberFunctor {B : Type u} [TopologicalSpace B] (b : B) : CategoryTheory.Functor (CoveringSpaceOver B) (Action (Type u) (FundamentalGroup B b))

The "take the fiber at b" functor Cov_B → π₁(B, b)-Set sending a covering space to its fiber equipped with the monodromy action, and a morphism to its restriction between fibers.

theorem CoveringSpaces.coveringSpacesClassification {B : Type u} [TopologicalSpace B] [IsSemiLocallySimplyConnected B] (b : B) : (fiberFunctor b).IsEquivalence

(Theorem 31.6) If B is semi-locally simply connected, the fiber functor Cov_B → π₁(B, b)-Set is an equivalence of categories.

@[reducible, inline]

noncomputable abbrev OrientationHomology.singularChainFunctor (R : Type) [CommRing R] : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat R) ℕ)

The singular chain complex functor Top → Ch_*(ModuleCat R) with coefficients in R, obtained by tensoring the integral singular chain complex with R.

def OrientationHomology.subsetIncl (M : Type) [TopologicalSpace M] (A : Set M) : TopCat.of ↑A ⟶ TopCat.of M

The inclusion of a subspace A ⊆ M as a morphism in TopCat.

noncomputable def OrientationHomology.relativeChainComplex (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (A : Set M) : ChainComplex (ModuleCat R) ℕ

The relative singular chain complex S_*(M, A; R), defined as the cokernel of the chain map induced by the inclusion A ↪ M.

noncomputable def OrientationHomology.relativeHomologyModule (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] (A : Set M) : ModuleCat R

The relative singular homology module H_n(M, A; R) of the pair (M, A).

noncomputable def OrientationHomology.localHomologyModule (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] (x : M) : ModuleCat R

The local homology module H_n(M, M − {x}; R) at the point x; the stalk of the orientation sheaf in degree n.

def OrientationHomology.subsetToSubset (M : Type) [TopologicalSpace M] (A B : Set M) (h : A ⊆ B) : TopCat.of ↑A ⟶ TopCat.of ↑B

The inclusion A ↪ B as a morphism in TopCat, given A ⊆ B.

noncomputable def OrientationHomology.restrictionChainMap (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (A B : Set M) (h : A ⊆ B) : relativeChainComplex R M A ⟶ relativeChainComplex R M B

For A ⊆ B, the natural chain map between the relative chain complexes S_*(M, A; R) → S_*(M, B; R) induced by the inclusion of subcomplexes.

noncomputable def OrientationHomology.restrictionHomologyMap (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] (A B : Set M) (h : A ⊆ B) : relativeHomologyModule R n M A ⟶ relativeHomologyModule R n M B

The induced map on relative homology H_n(M, A; R) → H_n(M, B; R) for A ⊆ B.

noncomputable def OrientationHomology.restrictToPoint (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] (U : Set M) (y : M) (hy : y ∈ U) : relativeHomologyModule R n M Uᶜ ⟶ localHomologyModule R n M y

The restriction map H_n(M, M − U; R) → H_n(M, M − {y}; R) = (o_M)_y from a "compatible class over U" to its local-homology value at any point y ∈ U.

def OrientationHomology.IsLocallyCompatibleSection (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] (μ : (x : M) → ↑(localHomologyModule R n M x)) : Prop

A choice of local-homology element at each point is locally compatible if every point has an open neighborhood U and a relative-homology class on (M, M − U) that restricts to the chosen element at every point of U.

noncomputable def OrientationHomology.orientationSectionModule (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] : ModuleCat R

The R-module Γ(M; o_M ⊗ R) of (not-necessarily continuous) sections of the orientation sheaf with R-coefficients, given here as the product of the local-homology fibers.

noncomputable def OrientationHomology.orientationComparisonMap (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] : ↑(relativeHomologyModule R n M ∅) →ₗ[R] (x : M) → ↑(localHomologyModule R n M x)

The comparison map j : H_n(M; R) → Γ(M; o_M ⊗ R) of the Orientation Theorem, sending a homology class to the family of its restrictions to each local-homology fiber.

structure OrientationHomology.ROrientation (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] : Type

(Definition 31.8) An R-orientation of an n-manifold M: a choice of generator μ x in each local-homology module H_n(M, M − {x}; R), depending locally compatibly on x. Equivalently, a section of the unit twisted local system (o_M ⊗ R)^×.

• μ (x : M) : ↑(localHomologyModule R n M x)
• generates (x : M) : R ∙ self.μ x = ⊤
• locallyCompatible (x : M) : ∃ (U : Set M) (_ : IsOpen U) (_ : x ∈ U) (α : ↑(relativeHomologyModule R n M Uᶜ)), ∀ (y : M) (hy : y ∈ U), (ModuleCat.Hom.hom (restrictToPoint R n M U y hy)) α = self.μ y

def OrientationHomology.IsROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] : Prop

The manifold M is R-orientable if it admits some R-orientation.

@[reducible, inline]

abbrev OrientationHomology.twoTorsion (R : Type) [CommRing R] : Submodule R R

The submodule R[2] := {r ∈ R : 2r = 0} of 2-torsion elements of R.

noncomputable def OrientationHomology.singularHomology_iso_relativeHomology_empty (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] : SingularCohomology.singularHomologyModule R (TopCat.of M) n ≅ relativeHomologyModule R n M ∅

Absolute singular homology agrees with relative homology against the empty subspace, H_n(M; R) ≅ H_n(M, ∅; R).

theorem OrientationHomology.manifold_t2Space (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] : T2Space M

A compact, connected charted space modelled on Euclidean space is Hausdorff. Used as a convenience hypothesis for the orientation theorem on a manifold.

theorem OrientationHomology.excision_transfer_OT_to_chart (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [AlgebraicTopologyI.TopologicalManifold n M] (K : Set M) (_hK : IsCompact K) (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (_he : e ∈ atlas (EuclideanSpace ℝ (Fin n)) M) (_hKe : K ⊆ e.source) : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) K

Excision step in the proof of the Orientation Theorem: if K is contained in the source of a chart, the Orientation Theorem for K reduces to the model case of a compact convex subset of Euclidean space.

theorem OrientationHomology.orientation_theorem_base_case (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [AlgebraicTopologyI.TopologicalManifold n M] (K : Set M) (hK : IsCompact K) (hChart : ∃ e ∈ atlas (EuclideanSpace ℝ (Fin n)) M, K ⊆ e.source) : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) K

Base case of the inductive proof of the Orientation Theorem: the result holds for any compact K contained in some chart of M.

theorem OrientationHomology.orientation_theorem_union_step (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [AlgebraicTopologyI.TopologicalManifold n M] (K₁ K₂ : Set M) (hK₁ : IsClosed K₁) (hK₂ : IsClosed K₂) (h₁ : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) K₁) (h₂ : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) K₂) (h₁₂ : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) (K₁ ∩ K₂)) : OrientationTheorem.OrientationTheoremResult n (fun (x : ℕ) (x_1 : Set M) => ↑(relativeHomologyModule R n M ∅)) (fun (x : Set M) => (x : M) → ↑(localHomologyModule R n M x)) (fun (x : Set M) => (orientationComparisonMap R n M).toAddMonoidHom) (K₁ ∪ K₂)

Union (Mayer–Vietoris) step in the proof of the Orientation Theorem: if the result holds for two closed sets K₁, K₂ and for their intersection, then it holds for their union.

noncomputable def OrientationHomology.orientation_theorem_singular_iso (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] : relativeHomologyModule R n M ∅ ≅ orientationSectionModule R n M

(Theorem 31.9, Orientation Theorem) For a compact connected n-manifold M and a commutative ring R, the comparison map gives an isomorphism H_n(M; R) ≅ Γ(M; o_M ⊗ R).

noncomputable def OrientationHomology.excision_localHomology_chartedSpace (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (x : M) : localHomologyModule R n M x ≅ localHomologyModule R n (EuclideanSpace ℝ (Fin n)) 0

Excision identifies the local homology of M at x with the local homology of Euclidean space at the origin, via a chart.

noncomputable def OrientationHomology.euclidean_localHomology_iso (n : ℕ) (R : Type) [CommRing R] : localHomologyModule R n (EuclideanSpace ℝ (Fin n)) 0 ≅ ModuleCat.of R R

The local homology of ℝⁿ at the origin in degree n is free of rank one over R: H_n(ℝⁿ, ℝⁿ − {0}; R) ≅ R.

noncomputable def OrientationHomology.localHomologyModule_iso_of_chartedSpace (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (x : M) : localHomologyModule R n M x ≅ ModuleCat.of R R

Combining excision with the Euclidean computation: for any x in an n-manifold, H_n(M, M − {x}; R) ≅ R.

theorem OrientationHomology.scalar_function_isLocallyConstant (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (o : ROrientation n M R) (σ : (x : M) → ↑(localHomologyModule R n M x)) (s : M → R) (hs : ∀ (x : M), σ x = s x • o.μ x) : IsLocallyConstant s

If σ is a (locally compatible) section of the orientation sheaf written in the form σ x = s x • μ x for a fixed R-orientation μ, then the scalar s : M → R is locally constant.

theorem OrientationHomology.orientationSectionModule_span_orientation (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (o : ROrientation n M R) (σ : (x : M) → ↑(localHomologyModule R n M x)) : ∃ (r : R), σ = fun (x : M) => r • o.μ x

On a compact connected n-manifold, any element of Γ(M; o_M ⊗ R) is a constant R-multiple of a fixed R-orientation.

theorem OrientationHomology.annihilator_trivial_of_span_top_iso_R {R : Type} [CommRing R] {N : ModuleCat R} (e : N ≅ ModuleCat.of R R) {v : ↑N} (hgen : R ∙ v = ⊤) {r : R} (hr : r • v = 0) : r = 0

If N is R-linearly isomorphic to R and v ∈ N spans N, then v has trivial annihilator: r • v = 0 implies r = 0.

noncomputable def OrientationHomology.orientationSections_iso_of_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : IsROrientable n M R) : orientationSectionModule R n M ≅ ModuleCat.of R R

For a compact connected R-orientable n-manifold, the module of orientation sections is free of rank one: Γ(M; o_M ⊗ R) ≅ R. Used to deduce Corollary 31.10 in the orientable case.

noncomputable def OrientationHomology.orientationSectionModule_iso_twoTorsion_of_not_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : ¬IsROrientable n M R) : orientationSectionModule R n M ≅ ModuleCat.of R ↥(twoTorsion R)

For a compact connected n-manifold that is not R-orientable, the orientation section module is isomorphic to the 2-torsion of R: Γ(M; o_M ⊗ R) ≅ R[2].

noncomputable def OrientationHomology.relativeHomology_iso_twoTorsion_of_not_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : ¬IsROrientable n M R) : relativeHomologyModule R n M ∅ ≅ ModuleCat.of R ↥(twoTorsion R)

In the non-orientable case, transporting the previous isomorphism through the Orientation Theorem gives H_n(M, ∅; R) ≅ R[2].

noncomputable def OrientationHomology.orientationSections_iso_twoTorsion_of_not_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : ¬IsROrientable n M R) : orientationSectionModule R n M ≅ ModuleCat.of R ↥(twoTorsion R)

Variant of the previous result, going through the singular-homology side of the Orientation Theorem and back.

theorem OrientationHomology.singularHomology_top_iso_of_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : IsROrientable n M R) : Nonempty (SingularCohomology.singularHomologyModule R (TopCat.of M) n ≅ ModuleCat.of R R)

(Corollary 31.10, orientable case) For a compact connected R-orientable n-manifold M, the top singular homology is free of rank one over R: H_n(M; R) ≅ R.

theorem OrientationHomology.singularHomology_top_iso_twoTorsion_of_not_isROrientable (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] (h : ¬IsROrientable n M R) : Nonempty (SingularCohomology.singularHomologyModule R (TopCat.of M) n ≅ ModuleCat.of R ↥(twoTorsion R))

(Corollary 31.10, non-orientable case) For a compact connected n-manifold M that is not R-orientable, the top singular homology is the 2-torsion of R: H_n(M; R) ≅ R[2].

theorem OrientationHomology.singularHomology_top_compact_manifold (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (R : Type) [CommRing R] : (IsROrientable n M R → Nonempty (SingularCohomology.singularHomologyModule R (TopCat.of M) n ≅ ModuleCat.of R R)) ∧ (¬IsROrientable n M R → Nonempty (SingularCohomology.singularHomologyModule R (TopCat.of M) n ≅ ModuleCat.of R ↥(twoTorsion R)))

(Corollary 31.10) Combined statement: for a compact connected n-manifold, H_n(M; R) is R in the orientable case and R[2] otherwise.

@[reducible, inline]

abbrev LocalCoefficientSystems.LocalCoefficientSystem (B : Type u_1) [TopologicalSpace B] (R : Type u_2) [CommRing R] : Type (max u_1 1 u_2)

A local coefficient system of R-modules over B: a functor from the fundamental groupoid of B to R-modules.

def LocalCoefficientSystems.fiberRepresentation {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] (b : B) (F : LocalCoefficientSystem B R) : Representation R (FundamentalGroup B b) ↑(F.obj { as := b })

The representation of π₁(B, b) on the fiber F(b) of a local coefficient system F.

def LocalCoefficientSystems.fiberIntertwiningMap {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] (b : B) {F G : LocalCoefficientSystem B R} (η : F ⟶ G) : (fiberRepresentation R b F).IntertwiningMap (fiberRepresentation R b G)

A natural transformation η : F → G of local coefficient systems restricts on fibers to an intertwining map between the corresponding π₁(B, b)-representations.

def LocalCoefficientSystems.fiberToRep {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] (b : B) : CategoryTheory.Functor (LocalCoefficientSystem B R) (Rep R (FundamentalGroup B b))

The functor sending a local coefficient system to its fiber at b as an object of Rep R (π₁(B, b)).

noncomputable def LocalCoefficientSystems.fiberFunctor {B : Type u_1} [TopologicalSpace B] (R : Type u_2) [CommRing R] (b : B) : CategoryTheory.Functor (LocalCoefficientSystem B R) (ModuleCat (MonoidAlgebra R (FundamentalGroup B b)))

The composite "fiber" functor from local coefficient systems on B to modules over the group algebra R[π₁(B, b)].

noncomputable def LocalCoefficientSystems.fiberEquivalence (B : Type u_1) [TopologicalSpace B] [PathConnectedSpace B] [CoveringSpaces.IsSemiLocallySimplyConnected B] (R : Type u_2) [CommRing R] (b : B) : LocalCoefficientSystem B R ≌ ModuleCat (MonoidAlgebra R (FundamentalGroup B b))

(Theorem 31.7) For B path connected and semi-locally simply connected, the fiber functor gives an equivalence between local coefficient systems of R-modules on B and modules over the group algebra R[π₁(B, b)].