Normalizer-quotient actions on subgroup fibre quotients

For a subgroup H ≤ deck p, the normalizer of H acts on the quotient of a fibre by H-orbits: a normalizer representative sends the class of e to the class of its deck translate. Elements of H act trivially on this quotient, so the action descends to the normalizer quotient N(H) / H.

This is the fibre-level action used to identify the deck group of the cover attached to H with N(H) / H.

Main declarations

• TauCeti.Deck.normalizerSubgroupFiberOrbitEquiv: the permutation of the H-fibre quotient induced by one normalizer representative.
• TauCeti.Deck.normalizerSubgroupFiberOrbitPermHom: the homomorphism from the normalizer to permutations of the H-fibre quotient.
• TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitPermHom: the descended homomorphism from N(H) / H.
• TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitMulAction: the resulting action of N(H) / H on SubgroupFiberOrbitQuotient H b.
• TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitIsPretransitive: transitivity of this descended action when the normalizer action on the fibre is transitive.
• TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitIsPretransitiveOfNormal: the normal-subgroup instance for this descended action.
• TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitIsCancelSMul: freeness of this descended action when the deck action on the fibre is free.

References

In the regular case that deck group specializes to π₁(X, x₀)/H.

def TauCeti.Deck.normalizerSubgroupFiberOrbitMap {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) : SubgroupFiberOrbitQuotient H b → SubgroupFiberOrbitQuotient H b

A normalizer representative acts on the quotient of one fibre by H-orbits.

Equations

• TauCeti.Deck.normalizerSubgroupFiberOrbitMap H φ = TauCeti.MulAction.normalizerOrbitRelQuotientMap H φ

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitMap_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (e : ↑(p ⁻¹' {b})) : normalizerSubgroupFiberOrbitMap H φ (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass H (↑φ • e)

The normalizer action on fibre quotients sends the class of a point to the class of its deck translate.

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitMap_one {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : normalizerSubgroupFiberOrbitMap H ⟨1, ⋯⟩ = id

The normalizer representative 1 acts trivially on the subgroup fibre quotient.

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitMap_mul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ ψ : ↥(Subgroup.normalizer ↑H)) : normalizerSubgroupFiberOrbitMap H (φ * ψ) = normalizerSubgroupFiberOrbitMap H φ ∘ normalizerSubgroupFiberOrbitMap H ψ

Normalizer representatives act by composition on the subgroup fibre quotient.

def TauCeti.Deck.normalizerSubgroupFiberOrbitEquiv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) : Equiv.Perm (SubgroupFiberOrbitQuotient H b)

A normalizer representative acts on the subgroup fibre quotient by a permutation.

Equations

• TauCeti.Deck.normalizerSubgroupFiberOrbitEquiv H φ = TauCeti.MulAction.normalizerOrbitRelQuotientEquiv H φ

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitEquiv_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (e : ↑(p ⁻¹' {b})) : (normalizerSubgroupFiberOrbitEquiv H φ) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass H (↑φ • e)

A normalizer representative permutes the subgroup fibre quotient by translating representatives.

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitEquiv_symm_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (e : ↑(p ⁻¹' {b})) : (Equiv.symm (normalizerSubgroupFiberOrbitEquiv H φ)) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass H ((↑φ)⁻¹ • e)

The inverse normalizer permutation translates fibre-orbit representatives by the inverse deck transformation.

noncomputable def TauCeti.Deck.normalizerSubgroupFiberOrbitPermHom {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : ↥(Subgroup.normalizer ↑H) →* Equiv.Perm (SubgroupFiberOrbitQuotient H b)

The normalizer action on the subgroup fibre quotient as a permutation representation.

Equations

• TauCeti.Deck.normalizerSubgroupFiberOrbitPermHom H = TauCeti.MulAction.normalizerOrbitRelQuotientPermHom H

@[simp]

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitPermHom_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (e : ↑(p ⁻¹' {b})) : ((normalizerSubgroupFiberOrbitPermHom H) φ) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass H (↑φ • e)

The normalizer permutation homomorphism sends representatives to the expected deck translate on fibre-orbit classes.

theorem TauCeti.Deck.normalizerSubgroupFiberOrbitPermHom_eq_one_of_mem {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (hφ : ↑φ ∈ H) : (normalizerSubgroupFiberOrbitPermHom H) φ = 1

Any normalizer representative whose underlying deck transformation lies in H maps to the identity permutation on the quotient of each fibre by H-orbits.

noncomputable def TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitPermHom {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : H.normalizerQuotient →* Equiv.Perm (SubgroupFiberOrbitQuotient H b)

The action of the normalizer on subgroup fibre quotients descends to N(H) / H.

Equations

• TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitPermHom H = TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom H

@[simp]

theorem TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitPermHom_mk_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(Subgroup.normalizer ↑H)) (e : ↑(p ⁻¹' {b})) : ((normalizerQuotientSubgroupFiberOrbitPermHom H) ↑φ) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass H (↑φ • e)

The descended normalizer-quotient action sends a normalizer representative to the corresponding deck translate on fibre-orbit classes.

@[instance_reducible]

noncomputable instance TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitMulAction {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : MulAction H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

The normalizer quotient N(H) / H acts on the quotient of a fibre by H-orbits.

Equations

• TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitMulAction H = TauCeti.MulAction.normalizerQuotientOrbitRelQuotientMulAction H

@[simp]

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

Representative formula for the action of N(H) / H on subgroup fibre quotients.

theorem TauCeti.Deck.normalizerQuotient_one_smul_subgroupFiberOrbitClass {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : 1 • subgroupFiberOrbitClass H e = subgroupFiberOrbitClass H e

The identity class in N(H) / H fixes every subgroup fibre-orbit class.

theorem TauCeti.Deck.normalizerQuotient_mk_of_mem_smul_subgroupFiberOrbitClass {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (φ : ↥(deck p)) (hφ : φ ∈ H) (e : ↑(p ⁻¹' {b})) : ↑⟨φ, ⋯⟩ • subgroupFiberOrbitClass H e = subgroupFiberOrbitClass H e

A representative from H acts trivially through the normalizer quotient.

theorem TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitIsPretransitive {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) [MulAction.IsPretransitive ↥(Subgroup.normalizer ↑H) ↑(p ⁻¹' {b})] : MulAction.IsPretransitive H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

If the normalizer of H acts transitively on the chosen fibre, then the descended N(H) / H action on the quotient of that fibre by H-orbits is transitive.

theorem TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitIsPretransitiveOfNormal {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) [H.Normal] : MulAction.IsPretransitive H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

If H is normal and the deck action on the chosen fibre is transitive, then the descended N(H) / H action on the quotient of that fibre by H-orbits is transitive.

instance TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitIsPretransitiveOfNormal {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) [H.Normal] : MulAction.IsPretransitive H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

The normalizer quotient acts transitively on a normal subgroup fibre quotient whenever the deck action on the fibre is transitive.

theorem TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitIsPretransitiveOfNormal_of_isRegular {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} (hreg : IsRegular p) (H : Subgroup ↥(deck p)) [H.Normal] : MulAction.IsPretransitive H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

For a regular map and a normal deck subgroup, the descended N(H) / H action on each subgroup fibre quotient is transitive. This is the fibre-action half of the regular-cover specialization from the normalizer quotient to an ordinary quotient by a normal subgroup.

theorem TauCeti.Deck.normalizerQuotient_smul_subgroupFiberOrbit_eq_smul_iff {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [IsCancelSMul ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) (a c : H.normalizerQuotient) (x : SubgroupFiberOrbitQuotient H b) : a • x = c • x ↔ a = c

Equality after the N(H) / H action on an H-fibre quotient is equality of normalizer-quotient elements, provided the deck action on that fibre is free.

instance TauCeti.Deck.instNormalizerQuotientSubgroupFiberOrbitIsCancelSMul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [IsCancelSMul ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) : IsCancelSMul H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

If the deck action on a fibre is free, then the descended N(H) / H action on the quotient of that fibre by H-orbits is free.

theorem TauCeti.Deck.normalizerQuotientSubgroupFiberOrbitIsCancelSMulOfIsCoveringMap {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [TopologicalSpace B] [PreconnectedSpace E] (hp : IsCoveringMap p) (H : Subgroup ↥(deck p)) : IsCancelSMul H.normalizerQuotient (SubgroupFiberOrbitQuotient H b)

For a preconnected covering map, the descended N(H) / H action on every H-fibre quotient is free.