The transfer of a finite covering on singular chains

Let p : E ⟶ B be a covering map whose fibres are finite. Topological simplices are simply connected and locally path connected, so a singular simplex σ of B lifts uniquely through p once the lift of one point is prescribed: evaluating at any point x of the simplex is a bijection from the lifts of σ onto the fibre of p over σ x. In particular σ has finitely many lifts, and restricting a lift to a face is a bijection onto the lifts of that face.

The transfer hp.singularTransfer hfin R : C(B; R) ⟶ C(E; R) sends a singular simplex to the sum of its lifts. Since faces of lifts are exactly the lifts of faces, this is a chain map. Composing with p_* counts the lifts: on a simplex σ it is multiplication by the cardinality of a fibre over a point of σ, so p_* ∘ transfer = d • id when every fibre has d points. A bijective self-map f of E over B, such as a deck transformation, permutes the lifts of each simplex, so f_* ∘ transfer = transfer. When p is the quotient covering of a free action of a finite group G, the lifts of p ∘ τ are the translates g • τ, so transfer ∘ p_* = ∑_{g ∈ G} g_*.

The variable-degree and constant-degree transfer formulas on chains and homology are in TauCeti.AlgebraicTopology.Singular.Transfer.Degree.

Main declarations

• IsCoveringMap.bijOn_simplexMap_apply: evaluation at a point of the simplex identifies the lifts of a singular simplex with a fibre of p.
• IsCoveringMap.bijOn_toSSet_obj_map: restricting lifts along a simplicial operator is a bijection onto the lifts of the restricted simplex.
• IsCoveringMap.bijOn_toSSet_map_app_of_comp_eq: a bijective self-map of E over B permutes the lifts of each singular simplex.
• IsCoveringMap.singularTransfer: the transfer chain map C(B; R) ⟶ C(E; R), with IsCoveringMap.ιChainComplex_singularTransfer_f its value on a singular simplex.
• IsCoveringMap.singularTransfer_comp_chainComplexMap_of_comp_eq: f_* ∘ transfer = transfer on singular chains for a bijective self-map f of E over B, and IsCoveringMap.homologyMap_singularTransfer_comp_homologyMap_of_comp_eq the same on singular homology.
• IsQuotientCoveringMap.chainComplexMap_comp_singularTransfer: for the quotient covering of a finite group G, transfer ∘ p_* = ∑_{g ∈ G} g_* on singular chains.

References

• A. Hatcher, Algebraic Topology, Section 3.G, for the transfer of a finite covering.

theorem IsCoveringMap.bijOn_simplexMap_apply {E B : TopCat} {p : E ⟶ B} (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj B).obj n) (x : ↑(SimplexCategory.toTop.{w}.obj (Opposite.unop n))) : Set.BijOn (fun (τ : (TopCat.toSSet.obj E).obj n) => (TauCeti.TopCat.simplexMap τ) x) (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) ⁻¹' {σ}) (⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {(TauCeti.TopCat.simplexMap σ) x})

Evaluation at a point x of the topological simplex is a bijection from the lifts of a singular simplex σ of B through the covering map p onto the fibre of p over σ x.

theorem IsCoveringMap.finite_preimage_singleton_toSSet_map_app {E B : TopCat} {p : E ⟶ B} (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj B).obj n) : (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) ⁻¹' {σ}).Finite

A singular simplex has only finitely many lifts through a covering map with finite fibres.

theorem IsCoveringMap.bijOn_toSSet_obj_map {E B : TopCat} {p : E ⟶ B} (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) {m n : SimplexCategoryᵒᵖ} (α : m ⟶ n) (σ : (TopCat.toSSet.obj B).obj m) : Set.BijOn (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj E).map α))) (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app m)) ⁻¹' {σ}) (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) ⁻¹' {(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj B).map α)) σ})

A simplicial operator α restricts the lifts of a singular simplex σ bijectively onto the lifts of the restricted simplex α^* σ.

theorem IsCoveringMap.bijOn_toSSet_map_app_of_comp_eq {E B : TopCat} {p : E ⟶ B} (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) {f : E ⟶ E} (hf : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfp : CategoryTheory.CategoryStruct.comp f p = p) {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj B).obj n) : Set.BijOn (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n))) (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) ⁻¹' {σ}) (⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) ⁻¹' {σ})

A bijective self-map f of E over B, such as a deck transformation of p, permutes the lifts of every singular simplex of B through p.

noncomputable def IsCoveringMap.singularTransfer {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) : (TopCat.toSSet.obj B).chainComplex R ⟶ (TopCat.toSSet.obj E).chainComplex R

The transfer C(B; R) ⟶ C(E; R) of a covering map p : E ⟶ B with finite fibres: the chain map sending a singular simplex of B to the sum of its lifts to E.

@[simp]

theorem IsCoveringMap.ιChainComplex_singularTransfer_f {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) ((hp.singularTransfer hfin R).f n) = ∑ τ ∈ ⋯.toFinset, (TopCat.toSSet.obj E).ιChainComplex τ

The transfer sends the summand of a singular simplex σ to the sum of the summands of the lifts of σ.

@[simp]

theorem IsCoveringMap.ιChainComplex_singularTransfer_f_assoc {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) {Z : C} (h : ((TopCat.toSSet.obj E).chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((hp.singularTransfer hfin R).f n) h) = CategoryTheory.CategoryStruct.comp (∑ τ ∈ ⋯.toFinset, (TopCat.toSSet.obj E).ιChainComplex τ) h

The transfer sends the summand of a singular simplex σ to the sum of the summands of the lifts of σ.

theorem IsCoveringMap.ιChainComplex_singularTransfer_f_comp_chainComplexMap_f {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) (x : ↑(SimplexCategory.toTop.{w}.obj { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((hp.singularTransfer hfin R).f n) ((SSet.chainComplexMap (TopCat.toSSet.map p) R).f n)) = Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {(TauCeti.TopCat.simplexMap σ) x}) • (TopCat.toSSet.obj B).ιChainComplex σ

Projecting the transfer of a singular simplex σ back down to B multiplies σ by the number of points of the fibre over any point σ x of σ.

theorem IsCoveringMap.singularTransfer_comp_chainComplexMap_of_comp_eq {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) {f : E ⟶ E} (hf : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfp : CategoryTheory.CategoryStruct.comp f p = p) : CategoryTheory.CategoryStruct.comp (hp.singularTransfer hfin R) (SSet.chainComplexMap (TopCat.toSSet.map f) R) = hp.singularTransfer hfin R

The transfer is invariant under deck transformations: f_* ∘ transfer = transfer on singular chains for every bijective self-map f of E over B, since f permutes the lifts of each singular simplex.

theorem IsCoveringMap.homologyMap_singularTransfer_comp_homologyMap_of_comp_eq {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.CategoryWithHomology C] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) {f : E ⟶ E} (hf : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfp : CategoryTheory.CategoryStruct.comp f p = p) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (SSet.homologyMap (TopCat.toSSet.map f) R n) = HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n

The transfer is invariant under deck transformations: f_* ∘ transfer = transfer on singular homology for every bijective self-map f of E over B.

theorem IsQuotientCoveringMap.chainComplexMap_comp_singularTransfer {E B : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {G : Type u_1} [Group G] [Fintype G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (R : C) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map p) R) (⋯.singularTransfer ⋯ R) = ∑ g : G, SSet.chainComplexMap (TopCat.toSSet.map (TopCat.ofHom { toFun := fun (x : ↑E) => g • x, continuous_toFun := ⋯ })) R

The deck-transformation formula transfer ∘ p_* = ∑_{g ∈ G} g_* on singular chains, for the quotient covering map p of an action of a finite group G.