Equivariance for normal deck-subgroup fibre quotients

For a normal subgroup H ≤ deck p, the existing free-transitive fibre-action equivalence identifies the quotient of a fibre by H with the normalizer quotient N(H) / H. This file records how that identification, and its regular preconnected-cover specialization, interacts with the descended N(H) / H action on the fibre quotient.

The orientation is important: the existing fibre-quotient equivalence sends the orbit class of φ • e to the normalizer-quotient class of φ⁻¹. Consequently, acting on the fibre quotient by a normalizer-quotient element a corresponds, under this equivalence, to right multiplication by a⁻¹.

Main declarations

• TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_map_smul_eq_mul_inv: the N(H) / H action becomes right multiplication by the inverse.
• the regular ..._map_smul_eq_mul_inv wrapper: the same statement for a regular preconnected covering map.
• Inverse-form lemmas for applying the inverse equivalence after right multiplication.

References

These results feed the identification of the deck group of the cover attached to H with N(H) / H, whose normal case is a quotient by H.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_map_smul_eq_mul_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] [IsCancelSMul ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) [H.Normal] (e : ↑(p ⁻¹' {b})) (a : H.normalizerQuotient) (x : SubgroupFiberOrbitQuotient H b) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) (a • x) = (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) x * a⁻¹

Under the normal-subgroup fibre quotient equivalence, the descended normalizer-quotient action is right multiplication by the inverse. This is the representative-free form of the convention that φ • e maps to the class of φ⁻¹.

@[simp]

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_map_smul_eq_mul_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [TopologicalSpace B] [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (H : Subgroup ↥(deck p)) [H.Normal] (e : ↑(p ⁻¹' {b})) (a : H.normalizerQuotient) (x : SubgroupFiberOrbitQuotient H b) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) (a • x) = (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) x * a⁻¹

For a regular preconnected covering map, the normal-subgroup fibre quotient equivalence turns the descended normalizer-quotient action into right multiplication by the inverse.

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_mul_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] [IsCancelSMul ↥(deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(deck p)) [H.Normal] (e : ↑(p ⁻¹' {b})) (a y : H.normalizerQuotient) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e).symm (y * a⁻¹) = a • (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e).symm y

Applying the inverse normal-subgroup fibre quotient equivalence after right multiplication by a⁻¹ is the same as acting by a on the fibre quotient.

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_mul_inv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [TopologicalSpace B] [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (H : Subgroup ↥(deck p)) [H.Normal] (e : ↑(p ⁻¹' {b})) (a y : H.normalizerQuotient) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e).symm (y * a⁻¹) = a • (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e).symm y

For a regular preconnected covering map, applying the inverse normal-subgroup fibre quotient equivalence after right multiplication by a⁻¹ is the same as acting by a on the fibre quotient.