Fibres of a map over a base

For p : E → X, the fibre of p over x is the set p ⁻¹' {x}. This file collects the two elementary constructions on such fibres that the covering-space development uses, each stated at the level where it is actually true: a bare function for the first, a bare equivalence for the second.

• Function.fiberMap: a map f : E → F commuting with the projections to X restricts to the fibres over each point. It is Set.MapsTo.restrict for the fibre inclusion, so its application, identity and composition laws are the generic Subtype.map ones.
• Equiv.compFiberEquiv: relabelling the base along h : X ≃ Y identifies the fibre of h ∘ p over y with the fibre of p over h.symm y.

Together they cover the two ways the fibres of a map vary: Function.fiberMap moves along a map over a fixed base and carries the identity and composition laws it inherits from Subtype.map, while Equiv.compFiberEquiv transports fibres along a change of base and is pinned down on points by its coercion lemmas. Neither uses a topology, so both are stated for a bare function and a bare equivalence; a ContinuousMap or a Homeomorph is applied through its underlying function or equivalence.

Main declarations

• Function.mapsTo_fiber: a map over X sends each fibre into the corresponding fibre.
• Function.fiberMap: the restriction of a map over X to the fibre over x.
• Equiv.compFiberEquiv: the relabelling of fibres under an equivalence of bases.

theorem Function.mapsTo_fiber {E : Type u_1} {F : Type u_2} {X : Type u_4} {p : E → X} {q : F → X} (f : E → F) (hf : q ∘ f = p) (x : X) : Set.MapsTo f (p ⁻¹' {x}) (q ⁻¹' {x})

A map over X sends the fibre over x into the fibre over x.

def Function.fiberMap {E : Type u_1} {F : Type u_2} {X : Type u_4} {p : E → X} {q : F → X} (f : E → F) (hf : q ∘ f = p) (x : X) : ↑(p ⁻¹' {x}) → ↑(q ⁻¹' {x})

The restriction of a map over X to the fibre over x.

Equations

• Function.fiberMap f hf x = Set.MapsTo.restrict f (p ⁻¹' {x}) (q ⁻¹' {x}) ⋯

@[simp]

theorem Function.fiberMap_apply_coe {E : Type u_1} {F : Type u_2} {X : Type u_4} {p : E → X} {q : F → X} (f : E → F) (hf : q ∘ f = p) (x : X) (e : ↑(p ⁻¹' {x})) : ↑(fiberMap f hf x e) = f ↑e

On underlying points, restriction to a fibre applies the original map.

@[simp]

theorem Function.fiberMap_id_apply {E : Type u_1} {X : Type u_4} {p : E → X} (x : X) (e : ↑(p ⁻¹' {x})) : fiberMap id ⋯ x e = e

Restricting the identity map to a fibre gives the identity.

theorem Function.fiberMap_comp_apply {E : Type u_1} {F : Type u_2} {G : Type u_3} {X : Type u_4} {p : E → X} {q : F → X} {r : G → X} (f : E → F) (g : F → G) (hf : q ∘ f = p) (hg : r ∘ g = q) (x : X) (e : ↑(p ⁻¹' {x})) : fiberMap (g ∘ f) ⋯ x e = fiberMap g hg x (fiberMap f hf x e)

Restriction to a fibre respects composition of maps over the base.

def Equiv.compFiberEquiv {E : Type u_1} {X : Type u_2} {Y : Type u_3} {p : E → X} (h : X ≃ Y) (y : Y) : ↑(⇑h ∘ p ⁻¹' {y}) ≃ ↑(p ⁻¹' {h.symm y})

Postcomposing a map with an equivalence of the base relabels its fibres: the fibre of h ∘ p over y is the fibre of p over h.symm y.

Equations

• h.compFiberEquiv y = Set.equivOfEq ⋯

@[simp]

theorem Equiv.compFiberEquiv_apply_coe {E : Type u_1} {X : Type u_2} {Y : Type u_3} {p : E → X} (h : X ≃ Y) (y : Y) (e : ↑(⇑h ∘ p ⁻¹' {y})) : ↑((h.compFiberEquiv y) e) = ↑e

On underlying points, the fibre equivalence for an equivalence of bases is the identity.

@[simp]

theorem Equiv.compFiberEquiv_symm_apply_coe {E : Type u_1} {X : Type u_2} {Y : Type u_3} {p : E → X} (h : X ≃ Y) (y : Y) (e : ↑(p ⁻¹' {h.symm y})) : ↑((h.compFiberEquiv y).symm e) = ↑e

On underlying points, the inverse fibre equivalence for an equivalence of bases is the identity.