Documentation

TauCeti.AlgebraicTopology.ThricePuncturedSphere.RestrictOver

Restricting a map to the Riemann sphere over the thrice-punctured sphere #

A map f : Z → OnePoint ℂ, such as a Belyi map or the projection of a topological branched cover, restricts to the points of Z lying over the thrice-punctured sphere: the complement of the fibres over 0, 1 and ∞. Read through the open embedding toOnePoint, this restriction is a map to ThricePuncturedSphere. It is a covering map whenever f is one away from the marked points, and its fibres are the fibres of f.

Main declarations #

source
noncomputable def TauCeti.ThricePuncturedSphere.restrictOver {Z : Type u_1} (f : Z → OnePoint ℂ) :
↑(f ⁻¹' Set.range toOnePoint) → ThricePuncturedSphere

The map f restricted to the complement of the fibres over 0, 1 and ∞, viewed as a map to ThricePuncturedSphere through toOnePoint.

Instances For
    source
    @[simp]
    theorem TauCeti.ThricePuncturedSphere.coe_restrictOver_apply {Z : Type u_1} (f : Z → OnePoint ℂ) (x : ↑(f ⁻¹' Set.range toOnePoint)) :
    ↑↑(restrictOver f x) = f ↑x

    The restriction of f agrees with f, read in the Riemann sphere.

    source
    theorem TauCeti.ThricePuncturedSphere.isCoveringMap_restrictOver {Z : Type u_1} [TopologicalSpace Z] {f : Z → OnePoint ℂ} (hf : IsCoveringMapOn f markedᶜ) :
    IsCoveringMap (restrictOver f)

    If f is a covering map away from 0, 1 and ∞, its restriction over the thrice-punctured sphere is a covering map.

    source
    theorem TauCeti.ThricePuncturedSphere.image_val_restrictOver_preimage_singleton {Z : Type u_1} (f : Z → OnePoint ℂ) (z : ThricePuncturedSphere) :
    Subtype.val '' restrictOver f ⁻¹' {z} = f ⁻¹' {z.toOnePoint}

    The points over z of the restriction of f are the points of the fibre of f over z.

    source
    theorem TauCeti.ThricePuncturedSphere.finite_restrictOver_preimage_singleton {Z : Type u_1} (f : Z → OnePoint ℂ) {z : ThricePuncturedSphere} (h : (f ⁻¹' {z.toOnePoint}).Finite) :
    (restrictOver f ⁻¹' {z}).Finite

    The fibre of the restriction of f over z is finite when the fibre of f over z is.

    source
    theorem TauCeti.ThricePuncturedSphere.ncard_restrictOver_preimage_singleton {Z : Type u_1} (f : Z → OnePoint ℂ) (z : ThricePuncturedSphere) :
    (restrictOver f ⁻¹' {z}).ncard = (f ⁻¹' {z.toOnePoint}).ncard

    The fibre of the restriction of f over z has as many points as the fibre of f.