Deck transformations of a map

For a map p : E → B, its deck transformations are the homeomorphisms of E over B. Mathlib collects them as the subgroup deck p of the homeomorphism group E ≃ₜ E; for a covering projection p this subgroup is the classical deck transformation group.

This file adds the fibre API that the rest of the deck-transformation development uses. In particular, deck.fiberHomeomorph restricts a deck transformation to each fibre of p.

The action of deck p on the total space is inherited, by subgroup transfer, from the tautological action of the ambient homeomorphism group E ≃ₜ E on E (Homeomorph.applyMulAction). Each deck transformation preserves p, hence preserves every fibre of p.

The deck group only sees p through the equalities p (φ e) = p e, so postcomposition by an injective map leaves it unchanged (TauCeti.deck_comp_of_injective).

References

The deck construction is due to Kim Morrison in mathlib4#40135.

def deck.fiberHomeomorph {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} (φ : ↥(deck p)) (b : B) : ↑(p ⁻¹' {b}) ≃ₜ ↑(p ⁻¹' {b})

A deck transformation restricts to a homeomorphism of every fibre of the projection, the restriction of its underlying homeomorphism along Homeomorph.subtype.

Equations

• deck.fiberHomeomorph φ b = (↑φ).subtype ⋯

@[simp]

theorem deck.fiberHomeomorph_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} (φ : ↥(deck p)) (b : B) (e : ↑(p ⁻¹' {b})) : ↑((fiberHomeomorph φ b) e) = ↑φ ↑e

On points, the fibre homeomorphism induced by a deck transformation is just evaluation of that transformation.

@[simp]

theorem deck.fiberHomeomorph_symm_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} (φ : ↥(deck p)) (b : B) (e : ↑(p ⁻¹' {b})) : ↑((fiberHomeomorph φ b).symm e) = (↑φ).symm ↑e

On points, the inverse fibre homeomorphism induced by a deck transformation is evaluation of the inverse homeomorphism.

@[simp]

theorem deck.smul_eq_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} (φ : ↥(deck p)) (e : E) : φ • e = ↑φ e

On points, the action of a deck transformation is evaluation of its underlying homeomorphism. The action itself is inherited, by subgroup transfer, from the tautological action of E ≃ₜ E on E.

@[simp]

theorem deck.inv_smul_eq_symm_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} (φ : ↥(deck p)) (e : E) : φ⁻¹ • e = (↑φ).symm e

Applying the inverse deck transformation is evaluation of the inverse homeomorphism.

theorem TauCeti.deck_comp_of_injective {E : Type u_3} {B : Type u_4} {B' : Type u_5} [TopologicalSpace E] {f : B → B'} (hf : Function.Injective f) (p : E → B) : deck (f ∘ p) = deck p

Postcomposing a map with an injection does not change its deck group.