Covering maps of a disjoint union

A family of covering maps f i : E i → X i assembles into a single map Sigma.map id f : (Σ i, E i) → Σ i, X i, and this file proves that the assembled map is again a covering map, identifies its fibres, and computes its monodromy.

Everything is local: the summand Set.range (Sigma.mk i) is open in Σ i, X i, the assembled map restricts over it to f i up to the two open embeddings, and IsCoveringMap is a pointwise condition, so the summandwise statements glue with no compatibility to check.

The classification of covering spaces by functors out of the fundamental groupoid, TauCeti.CoveringSpace.monodromyEquivalence, is available only over a path-connected base, which a disjoint union need not be; the statements here are proved summandwise instead and assume no connectivity.

Main declarations

• TauCeti.isCoveringMap_sigmaMap: a disjoint union of covering maps is a covering map.
• TauCeti.sigmaMapFiberEquiv: the fibre of Sigma.map id f over ⟨i, x⟩ is the fibre of f i over x.
• TauCeti.monodromy_sigmaMap: that identification intertwines the monodromy of f i along a path with the monodromy of Sigma.map id f along its image in Σ i, X i.

theorem TauCeti.isCoveringMap_sigmaMap {ι : Type u_1} {E : ι → Type u_2} {X : ι → Type u_3} [(i : ι) → TopologicalSpace (E i)] [(i : ι) → TopologicalSpace (X i)] (f : (i : ι) → E i → X i) (hf : ∀ (i : ι), IsCoveringMap (f i)) : IsCoveringMap (Sigma.map id f)

A disjoint union of covering maps is a covering map.

noncomputable def TauCeti.sigmaMapFiberEquiv {ι : Type u_1} {E : ι → Type u_2} {X : ι → Type u_3} (f : (i : ι) → E i → X i) (i : ι) (x : X i) : ↑(f i ⁻¹' {x}) ≃ ↑(Sigma.map id f ⁻¹' {⟨i, x⟩})

The fibre of a disjoint union of maps over ⟨i, x⟩ is the fibre of the i-th map over x, through the inclusion of the i-th summand.

Equations

• TauCeti.sigmaMapFiberEquiv f i x = (Equiv.Set.image (Sigma.mk i) (f i ⁻¹' {x}) ⋯).trans (Set.equivOfEq ⋯)

@[simp]

theorem TauCeti.sigmaMapFiberEquiv_apply_coe {ι : Type u_1} {E : ι → Type u_2} {X : ι → Type u_3} (f : (i : ι) → E i → X i) (i : ι) (x : X i) (e : ↑(f i ⁻¹' {x})) : ↑((sigmaMapFiberEquiv f i x) e) = ⟨i, ↑e⟩

@[simp]

theorem TauCeti.sigmaMapFiberEquiv_symm_apply_mk {ι : Type u_1} {E : ι → Type u_2} {X : ι → Type u_3} (f : (i : ι) → E i → X i) (i : ι) (x : X i) (e : E i) (he : e ∈ f i ⁻¹' {x}) : (sigmaMapFiberEquiv f i x).symm ⟨⟨i, e⟩, ⋯⟩ = ⟨e, he⟩

The inverse fibre equivalence sends an element in the i-th summand back to that element.

@[simp]

theorem TauCeti.monodromy_sigmaMap {ι : Type u_1} {E : ι → Type u_2} {X : ι → Type u_3} [(i : ι) → TopologicalSpace (E i)] [(i : ι) → TopologicalSpace (X i)] (f : (i : ι) → E i → X i) (hf : ∀ (i : ι), IsCoveringMap (f i)) {i : ι} {x y : X i} (γ : Path.Homotopic.Quotient x y) (e : ↑(f i ⁻¹' {x})) : ⋯.monodromy (γ.map { toFun := Sigma.mk i, continuous_toFun := ⋯ }) ((sigmaMapFiberEquiv f i x) e) = (sigmaMapFiberEquiv f i y) (⋯.monodromy γ e)

Monodromy commutes with the inclusion of a summand. Transporting a point of the fibre of f i over x into the disjoint union and letting the assembled cover transport it along the image of γ gives the same result as transporting along γ first.