Transfer for coverings of variable degree

For a covering with finite fibres, projection after transfer multiplies a singular simplex by the number of sheets over any point of that simplex. On a disconnected base this is not in general a single scalar: it is the action of the locally constant function IsCoveringMap.degree. This file proves the formula on chains and homology, then restricts it to any preconnected subspace. In particular each connected component has its own degree. The constant-degree formulas follow by specializing the degree to a constant function. There is no connectedness, surjectivity, or uniform bound on the fibre cardinalities.

We reuse IsCoveringMap.singularTransfer and its summand formula. The mathematical reference is Hatcher, Algebraic Topology, Section 3.G.

theorem IsCoveringMap.singularTransfer_comp_chainComplexMap_eq_locallyConstantNsmul {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) : CategoryTheory.CategoryStruct.comp (hp.singularTransfer hfin R) (SSet.chainComplexMap (TopCat.toSSet.map p) R) = TauCeti.singularChainLocallyConstantNsmul R hp.degree

Variable-degree transfer formula on chains. Projection after transfer is multiplication by the locally constant fibre cardinality, rather than a single global degree.

theorem IsCoveringMap.homologyMap_singularTransfer_comp_homologyMap_eq_locallyConstantNsmul {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (SSet.homologyMap (TopCat.toSSet.map p) R n) = HomologicalComplex.homologyMap (TauCeti.singularChainLocallyConstantNsmul R hp.degree) n

Variable-degree transfer formula on homology. Projection after transfer is the map induced by multiplication of chains by the locally constant fibre cardinality.

theorem IsCoveringMap.singularTransfer_comp_chainComplexMap {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) {d : ℕ} (hd : ∀ (b : ↑B), Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b}) = d) : CategoryTheory.CategoryStruct.comp (hp.singularTransfer hfin R) (SSet.chainComplexMap (TopCat.toSSet.map p) R) = d • CategoryTheory.CategoryStruct.id ((TopCat.toSSet.obj B).chainComplex R)

The transfer formula p_* ∘ transfer = d • id on singular chains, for a covering map whose fibres all have d points.

theorem IsCoveringMap.homologyMap_singularTransfer_comp_homologyMap {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) {d : ℕ} (hd : ∀ (b : ↑B), Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b}) = d) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (SSet.homologyMap (TopCat.toSSet.map p) R n) = d • CategoryTheory.CategoryStruct.id (HomologicalComplex.homology ((TopCat.toSSet.obj B).chainComplex R) n)

The transfer formula p_* ∘ transfer = d • id on singular homology, for a covering map whose fibres all have d points.

theorem IsCoveringMap.chainComplexMap_comp_singularTransfer_comp_chainComplexMap {E B Y : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [PreconnectedSpace ↑Y] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) (f : Y ⟶ B) (y : ↑Y) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (CategoryTheory.CategoryStruct.comp (hp.singularTransfer hfin R) (SSet.chainComplexMap (TopCat.toSSet.map p) R)) = Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {(CategoryTheory.ConcreteCategory.hom f) y}) • SSet.chainComplexMap (TopCat.toSSet.map f) R

On chains from a preconnected space mapping into the base, projection after transfer multiplies by the fibre cardinality over the image of any chosen point of that space.

theorem IsCoveringMap.chainComplexMap_comp_singularTransfer_comp_chainComplexMap_assoc {E B Y : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [PreconnectedSpace ↑Y] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) (f : Y ⟶ B) (y : ↑Y) {Z : ChainComplex C ℕ} (h : (TopCat.toSSet.obj B).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (CategoryTheory.CategoryStruct.comp (hp.singularTransfer hfin R) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map p) R) h)) = CategoryTheory.CategoryStruct.comp (Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {(CategoryTheory.ConcreteCategory.hom f) y}) • SSet.chainComplexMap (TopCat.toSSet.map f) R) h

On chains from a preconnected space mapping into the base, projection after transfer multiplies by the fibre cardinality over the image of any chosen point of that space.

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

On homology classes coming from a preconnected space, projection after transfer is multiplication by the number of sheets over that component. This includes degree zero.

theorem IsCoveringMap.homologyMap_comp_singularTransfer_comp_homologyMap_assoc {E B Y : TopCat} {p : E ⟶ B} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.CategoryWithHomology C] [PreconnectedSpace ↑Y] (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hfin : ∀ (b : ↑B), Finite ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b})) (R : C) (f : Y ⟶ B) (y : ↑Y) (n : ℕ) {Z : C} (h : (TopCat.toSSet.obj B).homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map f) R n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map p) R n) h)) = CategoryTheory.CategoryStruct.comp (Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {(CategoryTheory.ConcreteCategory.hom f) y}) • SSet.homologyMap (TopCat.toSSet.map f) R n) h

On homology classes coming from a preconnected space, projection after transfer is multiplication by the number of sheets over that component. This includes degree zero.

theorem IsCoveringMap.homologyMap_connectedComponent_comp_singularTransfer_comp_homologyMap {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) (b : ↑B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })) R n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (SSet.homologyMap (TopCat.toSSet.map p) R n)) = Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b}) • SSet.homologyMap (TopCat.toSSet.map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })) R n

Componentwise transfer formula. The restriction to the homology coming from a connected component of the base uses the degree of that component, with no global degree hypothesis.

theorem IsCoveringMap.homologyMap_connectedComponent_comp_singularTransfer_comp_homologyMap_assoc {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) (b : ↑B) (n : ℕ) {Z : C} (h : (TopCat.toSSet.obj B).homology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })) R n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hp.singularTransfer hfin R) n) (CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map p) R n) h)) = CategoryTheory.CategoryStruct.comp (Nat.card ↑(⇑(CategoryTheory.ConcreteCategory.hom p) ⁻¹' {b}) • SSet.homologyMap (TopCat.toSSet.map (TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })) R n) h

Componentwise transfer formula. The restriction to the homology coming from a connected component of the base uses the degree of that component, with no global degree hypothesis.