The action of deck transformations on a fibre

A deck transformation preserves every fibre of the projection. This file packages that restriction as a multiplicative homomorphism from the deck transformation group to the homeomorphism group of a chosen fibre, and records the induced action on that fibre.

This is bookkeeping for the universal-covers roadmap: the later comparison between deck transformations and the fundamental group, and the regular-cover statements, use the action of deck transformations on individual fibres rather than only on the total space.

Main definitions

• TauCeti.Deck.fiberHomeomorphHom: the homomorphism Deck p →* (p ⁻¹' {b} ≃ₜ p ⁻¹' {b}).
• TauCeti.Deck.instFiberMulAction: the induced action of Deck p on the fibre over b.
• TauCeti.Deck.mem_fiber_stabilizer_iff_coe: membership in a fibre stabilizer is equality on the underlying point.

References

This supplies a prerequisite for the Tau Ceti universal-covers roadmap, Stage 0.4 (Deck p as the deck transformation group), and the later deck-group action on fibres in Stages 1 and 2.

def TauCeti.Deck.fiberHomeomorphHom {E : Type u_1} {B : Type u_2} [TopologicalSpace E] (p : E → B) (b : B) : ↥(Deck p) →* ↑(p ⁻¹' {b}) ≃ₜ ↑(p ⁻¹' {b})

The homomorphism from deck transformations to homeomorphisms of the fibre over b.

It sends a deck transformation to its restriction to the subtype p ⁻¹' {b}.

Equations

• TauCeti.Deck.fiberHomeomorphHom p b = { toFun := fun (φ : ↥(TauCeti.Deck p)) => TauCeti.Deck.fiberHomeomorph φ b, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

The fibre homomorphism evaluates by applying the deck transformation to the underlying point of the fibre.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_apply_coe {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : ↑(((fiberHomeomorphHom p b) φ) e) = ↑φ ↑e

On underlying points, the fibre homomorphism is evaluation of the underlying homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_one {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} : (fiberHomeomorphHom p b) 1 = 1

The fibre homomorphism sends the identity deck transformation to the identity homeomorphism of the fibre.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_mul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ ψ : ↥(Deck p)) : (fiberHomeomorphHom p b) (φ * ψ) = (fiberHomeomorphHom p b) φ * (fiberHomeomorphHom p b) ψ

The fibre homomorphism sends products of deck transformations to products of fibre homeomorphisms.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) : (fiberHomeomorphHom p b) φ⁻¹ = ((fiberHomeomorphHom p b) φ)⁻¹

The fibre homomorphism sends inverses of deck transformations to inverses of fibre homeomorphisms.

@[simp]

theorem TauCeti.Deck.fiberHomeomorph_one {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} : fiberHomeomorph 1 b = 1

The fibre homeomorphism associated to the identity deck transformation is the identity.

@[simp]

theorem TauCeti.Deck.fiberHomeomorph_mul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ ψ : ↥(Deck p)) : fiberHomeomorph (φ * ψ) b = fiberHomeomorph φ b * fiberHomeomorph ψ b

The fibre homeomorphism associated to a product is the product of the associated fibre homeomorphisms.

@[simp]

theorem TauCeti.Deck.fiberHomeomorph_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) : fiberHomeomorph φ⁻¹ b = (fiberHomeomorph φ b)⁻¹

The fibre homeomorphism associated to an inverse is the inverse of the associated fibre homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberHomeomorph_pow {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (n : ℕ) : fiberHomeomorph (φ ^ n) b = fiberHomeomorph φ b ^ n

The fibre homeomorphism associated to a natural-number power is the corresponding power of the associated fibre homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberHomeomorph_zpow {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (n : ℤ) : fiberHomeomorph (φ ^ n) b = fiberHomeomorph φ b ^ n

The fibre homeomorphism associated to an integer power is the corresponding power of the associated fibre homeomorphism.

@[implicit_reducible]

instance TauCeti.Deck.instFiberMulAction {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} : MulAction ↥(Deck p) ↑(p ⁻¹' {b})

Deck transformations act on each fibre by restricting their action on the total space.

Equations

• TauCeti.Deck.instFiberMulAction = MulAction.compHom (↑(p ⁻¹' {b})) (TauCeti.Deck.fiberHomeomorphHom p b)

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

The fibre action is evaluation of the fibre homeomorphism.

@[simp]

theorem TauCeti.Deck.fiber_smul_coe {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : ↑(φ • e) = ↑φ ↑e

On underlying points, the fibre action is evaluation of the underlying deck transformation.

theorem TauCeti.Deck.map_fiber_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : p (φ • ↑e) = b

The projection value of a point in the fibre is unchanged after the restricted deck action.

theorem TauCeti.Deck.fiber_smul_mem {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : φ • ↑e ∈ p ⁻¹' {b}

The restricted deck action keeps points in the fibre over b.

theorem TauCeti.Deck.fiber_smul_coe_eq_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : ↑(φ • e) = φ • ↑e

The restricted fibre action agrees with the ambient action on the total space after coercing out of the fibre subtype.

theorem TauCeti.Deck.mem_fiber_stabilizer_iff_coe {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(Deck p)) (e : ↑(p ⁻¹' {b})) : φ ∈ MulAction.stabilizer (↥(Deck p)) e ↔ ↑φ ↑e = ↑e

Membership in the stabilizer of a fibre point is equality on the underlying point.