Normal deck-subgroup fibre quotients

For a regular preconnected covering map, the quotient of one fibre by a subgroup H ≤ Deck p is already identified with the coset quotient Deck p ⧸ H. When H is normal, the universal-covers roadmap uses this quotient as the regular-cover specialization of the normalizer quotient N(H) / H. This file records that specialization directly, so later deck-group computations for quotient covers can move between fibre quotients and normalizer quotients without redoing the algebraic comparison.

Main declarations

• TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal: for a normal subgroup H ≤ Deck p, identifies the subgroup fibre-orbit quotient with N(H) / H when the deck action on the chosen fibre is free and transitive.
• TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal: the regular-cover specialization.
• Simp lemmas for the image of the chosen fibre point, its deck translates, and representatives of the inverse map.

References

This is a small prerequisite for TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8: in the regular case H ◁ π₁(X, x₀), the deck group of the cover attached to H is π₁(X, x₀) / H. The file combines the existing Tau Ceti regular fibre-quotient equivalence with the algebraic normalizer-quotient comparison; no Mathlib infrastructure is vendored.

noncomputable def TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal {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})) : SubgroupFiberOrbitQuotient H b ≃ Subgroup.normalizerQuotient H

For a normal subgroup H ≤ Deck p, the quotient of a fibre by the restricted H-action is the normalizer quotient N(H) / H, once the deck action on the fibre is free and transitive.

Under normality, N(H) = Deck p, so this is the fibre-level version of the regular-cover specialization from N(H) / H to Deck p / H.

Equations

• TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e = TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal H e

noncomputable def TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal {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})) : SubgroupFiberOrbitQuotient H b ≃ Subgroup.normalizerQuotient H

For a regular preconnected covering and a normal subgroup H ≤ Deck p, the quotient of a fibre by the restricted H-action is the normalizer quotient N(H) / H.

Equations

• TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e = TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e

@[simp]

theorem TauCeti.Deck.normalizerQuotientEquivQuotientOfNormal_subgroupFiberOrbitQuotientEquiv {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})) (x : SubgroupFiberOrbitQuotient H b) : (Subgroup.normalizerQuotientEquivQuotientOfNormal H) ((subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) x) = (subgroupFiberOrbitQuotientEquivQuotientGroup H e) x

The normal-subgroup fibre quotient equivalence, followed by the normalizer quotient's normal-case comparison, is the existing equivalence to Deck p ⧸ H.

@[simp]

theorem TauCeti.Deck.normalizerQuotientEquivQuotientOfNormal_regularSubgroupFiberOrbitQuotientEquiv {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})) (x : SubgroupFiberOrbitQuotient H b) : (Subgroup.normalizerQuotientEquivQuotientOfNormal H) ((regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) x) = (regularSubgroupFiberOrbitQuotientEquivQuotientGroup hp hreg H e) x

For a regular cover, the normal-subgroup fibre quotient equivalence, followed by the normalizer quotient's normal-case comparison, is the existing equivalence to Deck p ⧸ H.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_base {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})) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) (subgroupFiberOrbitClass H e) = (Subgroup.normalizerQuotientMk H) ⟨1, ⋯⟩

The chosen fibre point maps to the identity class in the normalizer quotient.

@[simp]

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_base {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})) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) (subgroupFiberOrbitClass H e) = (Subgroup.normalizerQuotientMk H) ⟨1, ⋯⟩

For a regular cover, the chosen fibre point maps to the identity class in the normalizer quotient.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_smul {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})) (φ : ↥(Deck p)) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) (subgroupFiberOrbitClass H (φ • e)) = (Subgroup.normalizerQuotientMk H) ⟨φ⁻¹, ⋯⟩

The normal-subgroup fibre quotient equivalence sends the class of φ • e to the normalizer-quotient class of φ⁻¹.

@[simp]

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_smul {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})) (φ : ↥(Deck p)) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) (subgroupFiberOrbitClass H (φ • e)) = (Subgroup.normalizerQuotientMk H) ⟨φ⁻¹, ⋯⟩

For a regular cover, the normal-subgroup fibre quotient equivalence sends the class of φ • e to the normalizer-quotient class of φ⁻¹.

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_inv_smul {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})) (φ : ↥(Deck p)) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e) (subgroupFiberOrbitClass H (φ⁻¹ • e)) = (Subgroup.normalizerQuotientMk H) ⟨φ, ⋯⟩

The normal-subgroup fibre quotient equivalence sends the class of φ⁻¹ • e to the normalizer-quotient class of φ.

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_apply_inv_smul {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})) (φ : ↥(Deck p)) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e) (subgroupFiberOrbitClass H (φ⁻¹ • e)) = (Subgroup.normalizerQuotientMk H) ⟨φ, ⋯⟩

For a regular cover, the normal-subgroup fibre quotient equivalence sends the class of φ⁻¹ • e to the normalizer-quotient class of φ.

theorem TauCeti.Deck.subgroupFiberOrbitClass_eq_iff_normalizerQuotientMk_inv_eq {E : Type u_1} {B : Type u_2} [TopologicalSpace E] {p : E → B} {b : B} [IsCancelSMul ↥(Deck p) ↑(p ⁻¹' {b})] (H : Subgroup ↥(Deck p)) [H.Normal] (e : ↑(p ⁻¹' {b})) (φ ψ : ↥(Deck p)) : subgroupFiberOrbitClass H (φ • e) = subgroupFiberOrbitClass H (ψ • e) ↔ (Subgroup.normalizerQuotientMk H) ⟨φ⁻¹, ⋯⟩ = (Subgroup.normalizerQuotientMk H) ⟨ψ⁻¹, ⋯⟩

Equality of subgroup fibre-orbit classes of two deck translates is equality of the corresponding inverse representatives in the normalizer quotient.

theorem TauCeti.Deck.subgroupFiberOrbitClass_eq_iff_normalizerQuotientMk_inv_eq_of_isCoveringMap {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)) [H.Normal] (e : ↑(p ⁻¹' {b})) (φ ψ : ↥(Deck p)) : subgroupFiberOrbitClass H (φ • e) = subgroupFiberOrbitClass H (ψ • e) ↔ (Subgroup.normalizerQuotientMk H) ⟨φ⁻¹, ⋯⟩ = (Subgroup.normalizerQuotientMk H) ⟨ψ⁻¹, ⋯⟩

For a preconnected cover, equality of subgroup fibre-orbit classes of two deck translates is equality of the corresponding inverse representatives in the normalizer quotient.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_mk {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})) (φ : ↥(Subgroup.normalizer ↑H)) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e).symm ↑φ = subgroupFiberOrbitClass H ((↑φ)⁻¹ • e)

The inverse equivalence sends a normalizer representative to the fibre-orbit class of its inverse acting on the chosen fibre point.

@[simp]

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_mk {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})) (φ : ↥(Subgroup.normalizer ↑H)) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e).symm ↑φ = subgroupFiberOrbitClass H ((↑φ)⁻¹ • e)

For a regular cover, the inverse equivalence sends a normalizer representative to the fibre-orbit class of its inverse acting on the chosen fibre point.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_one {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})) : (subgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal H e).symm 1 = subgroupFiberOrbitClass H e

In particular, the inverse equivalence sends the identity normalizer quotient class to the chosen fibre-orbit class.

@[simp]

theorem TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal_symm_one {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})) : (regularSubgroupFiberOrbitQuotientEquivNormalizerQuotientOfNormal hp hreg H e).symm 1 = subgroupFiberOrbitClass H e

For a regular cover, the inverse equivalence sends the identity normalizer quotient class to the chosen fibre-orbit class.