The action of deck transformations on a fibre

A deck transformation preserves every fibre of the projection, so each fibre of p is a deck p-stable subset of the total space. This file records that fibre as a SubMulAction, so that the action of deck p on it is the restriction of the tautological action on the total space and the two agree on underlying points by definition, and packages the same restriction as a multiplicative homomorphism to the homeomorphism group of the fibre.

The 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.fiberSubMulAction: the fibre over b as a deck p-stable subset of the total space, and TauCeti.Deck.instFiberMulAction: the action of deck p it carries.
• deck.fiber_stabilizer_eq_stabilizer_coe: the stabilizer of a fibre point is the stabilizer of the underlying point of the total space, and deck.mem_fiber_stabilizer_iff_coe: membership in a fibre stabilizer is equality on the underlying point.

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 (φ : ↥(deck p)) => deck.fiberHomeomorph φ b, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem deck.fiberHomeomorphHom_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (φ : ↥(deck p)) (e : ↑(p ⁻¹' {b})) : ((TauCeti.Deck.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 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 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 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 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 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.

def TauCeti.Deck.fiberSubMulAction {E : Type u_1} {B : Type u_2} [TopologicalSpace E] (p : E → B) (b : B) : SubMulAction (↥(deck p)) E

The fibre of p over b, as a deck p-stable subset of the total space: a deck transformation fixes the value of p, hence maps the fibre over b to itself.

The body is exposed because the subtype it denotes has to be recognised as the fibre p ⁻¹' {b} itself, which is what lets the generic SubMulAction API apply to the fibre action.

Equations

• TauCeti.Deck.fiberSubMulAction p b = { carrier := p ⁻¹' {b}, smul_mem' := ⋯ }

@[instance_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 = (TauCeti.Deck.fiberSubMulAction p b).mulAction

@[simp]

theorem 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 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.

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

The stabilizer of a point of the fibre is the stabilizer of the underlying point of the total space.

theorem 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.