Fibre orbits for subgroups of the deck group

This file packages the orbit quotient of a single fibre by a chosen subgroup H ≤ deck p. When the cover attached to a subgroup is compared with a pointed cover, changing the chosen lift in one fibre is controlled by subgroup orbits, and regular-cover statements compare these orbits with normalizers and deck groups.

Mathlib already supplies the generic orbit quotient MulAction.orbitRel.Quotient; the declarations here only specialize it to the deck action on a fibre and record the maps that the classification of covers reuses.

Main declarations

• TauCeti.Deck.SubgroupFiberOrbitQuotient: the quotient of one fibre by a subgroup of the deck group.
• TauCeti.Deck.subgroupFiberOrbitClass: the quotient class of a fibre point.
• TauCeti.Deck.subgroupFiberOrbitMapOfLE: the map induced by an inclusion H ≤ K.
• TauCeti.Deck.subgroupFiberOrbitQuotientEquiv: transport of subgroup fibre-orbit quotients along an over-base homeomorphism.
• TauCeti.Deck.subgroupFiberOrbitQuotientBotEquiv: the quotient for ⊥ ≤ deck p is the original fibre.
• TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv: the quotient for ⊤ ≤ deck p is the existing full deck-orbit quotient.
• TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit: the map from an H-fibre quotient to the full deck-orbit quotient induced by H ≤ ⊤.

References

It is the subgroup-level analogue of TauCeti.AlgebraicTopology.UniversalCover.Deck.Fiber.Orbit, adapting that file's fiberOrbitClass, fiberOrbitQuotientEquiv, and fibre transport/conjugation lemmas from the full deck group to arbitrary subgroups.

@[reducible, inline]

abbrev TauCeti.Deck.SubgroupFiberOrbitQuotient {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} (H : Subgroup ↥(deck p)) (b : B) : Type u_1

The quotient of the fibre over b by the restricted action of a subgroup of the deck group.

Equations

• TauCeti.Deck.SubgroupFiberOrbitQuotient H b = MulAction.orbitRel.Quotient ↥H ↑(p ⁻¹' {b})

def TauCeti.Deck.subgroupFiberOrbitClass {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : SubgroupFiberOrbitQuotient H b

The H-orbit class of a point in one fibre.

Equations

• TauCeti.Deck.subgroupFiberOrbitClass H e = Quotient.mk'' e

theorem TauCeti.Deck.subgroupFiberOrbitClass_eq_mk {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitClass H e = Quotient.mk'' e

The subgroup fibre-orbit quotient map sends a fibre point to its own class.

theorem TauCeti.Deck.subgroupFiberOrbitClass_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitClass H e = subgroupFiberOrbitClass H e' ↔ e ∈ MulAction.orbit (↥H) e'

Two fibre points have the same H-orbit class exactly when they lie in the same H-orbit. The orientation follows MulAction.orbitRel_apply: the left point is in the orbit of the right point.

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

A deck translate of the chosen fibre point has the same subgroup orbit class as the chosen point exactly when the translating deck transformation lies in the subgroup.

theorem TauCeti.Deck.subgroupFiberOrbitClass_smul_eq_base_iff_of_isCoveringMap {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} [TopologicalSpace B] [PreconnectedSpace E] (hp : IsCoveringMap p) (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : subgroupFiberOrbitClass H (φ • e) = subgroupFiberOrbitClass H e ↔ φ ∈ H

For a preconnected covering, a deck translate of the chosen fibre point has the same subgroup orbit class as the chosen point exactly when the translating deck transformation lies in the subgroup.

def TauCeti.Deck.subgroupFiberOrbitMapOfLE {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K : Subgroup ↥(deck p)} (hHK : H ≤ K) : SubgroupFiberOrbitQuotient H b → SubgroupFiberOrbitQuotient K b

If H ≤ K, the quotient of a fibre by H maps naturally to the quotient by K.

Equations

• TauCeti.Deck.subgroupFiberOrbitMapOfLE hHK = Setoid.map_of_le ⋯

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K : Subgroup ↥(deck p)} (hHK : H ≤ K) (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitMapOfLE hHK (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass K e

The map induced by H ≤ K sends the H-class of a point to its K-class.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : subgroupFiberOrbitMapOfLE ⋯ = id

The map induced by the identity inclusion is the identity on the subgroup fibre-orbit quotient.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_comp {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K L : Subgroup ↥(deck p)} (hHK : H ≤ K) (hKL : K ≤ L) : subgroupFiberOrbitMapOfLE hKL ∘ subgroupFiberOrbitMapOfLE hHK = subgroupFiberOrbitMapOfLE ⋯

The maps induced by subgroup inclusions compose as expected.

theorem TauCeti.Deck.subgroupFiberOrbitQuotient_subsingleton_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : Subsingleton (SubgroupFiberOrbitQuotient H b) ↔ MulAction.IsPretransitive ↥H ↑(p ⁻¹' {b})

A subgroup fibre-orbit quotient is subsingleton exactly when that subgroup acts transitively on the fibre.

theorem TauCeti.Deck.subsingleton_subgroupFiberOrbitQuotient_top {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] : Subsingleton (SubgroupFiberOrbitQuotient ⊤ b)

If the full deck group acts transitively on a fibre, then the quotient of that fibre by the full deck subgroup is a subsingleton.

theorem TauCeti.Deck.subsingleton_regularSubgroupFiberOrbitQuotient_top {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (hreg : IsRegular p) : Subsingleton (SubgroupFiberOrbitQuotient ⊤ b)

For a regular cover, the quotient of a fibre by the full deck subgroup is a subsingleton.

theorem TauCeti.Deck.fiberMap_mem_orbit_subgroup_map {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (H : Subgroup ↥(deck p)) {e e' : ↑(p ⁻¹' {b})} (hee' : e ∈ MulAction.orbit (↥H) e') : (fiberMap h hpq b) e ∈ MulAction.orbit (↥(Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((fiberMap h hpq b) e')

Transporting a point in an H-orbit along an over-base homeomorphism puts the transported point in the orbit for the conjugated subgroup.

theorem TauCeti.Deck.mem_orbit_fiberMap_subgroup_map_iff {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (H : Subgroup ↥(deck p)) (e e' : ↑(p ⁻¹' {b})) : (fiberMap h hpq b) e ∈ MulAction.orbit (↥(Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((fiberMap h hpq b) e') ↔ e ∈ MulAction.orbit (↥H) e'

Membership in a subgroup fibre-orbit is preserved by an over-base homeomorphism, with the subgroup conjugated along the induced deck-group isomorphism.

def TauCeti.Deck.subgroupFiberOrbitQuotientEquiv {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (H : Subgroup ↥(deck p)) (b : B) : SubgroupFiberOrbitQuotient H b ≃ SubgroupFiberOrbitQuotient (Subgroup.map (↑(conjMulEquiv h hpq)) H) b

An over-base homeomorphism identifies subgroup fibre-orbit quotients, conjugating the subgroup of deck transformations along the induced deck-group isomorphism.

Equations

• TauCeti.Deck.subgroupFiberOrbitQuotientEquiv h hpq H b = Quotient.congr (TauCeti.Deck.fiberMap h hpq b).toEquiv ⋯

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquiv_apply {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : (subgroupFiberOrbitQuotientEquiv h hpq H b) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass (Subgroup.map (↑(conjMulEquiv h hpq)) H) ((fiberMap h hpq b) e)

The transported equivalence on subgroup fibre-orbit quotients sends a class to the class of the transported fibre point.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquiv_symm_apply {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (H : Subgroup ↥(deck p)) (f : ↑(q ⁻¹' {b})) : (subgroupFiberOrbitQuotientEquiv h hpq H b).symm (subgroupFiberOrbitClass (Subgroup.map (↑(conjMulEquiv h hpq)) H) f) = subgroupFiberOrbitClass H ((fiberMap h hpq b).symm f)

The inverse transported equivalence sends a target class to the class of its inverse transport.

theorem TauCeti.Deck.cast_subgroupFiberOrbitClass {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K : Subgroup ↥(deck p)} (hHK : H = K) (e : ↑(p ⁻¹' {b})) : (Equiv.cast ⋯) (subgroupFiberOrbitClass H e) = subgroupFiberOrbitClass K e

Casting subgroup fibre-orbit quotients along an equality of subgroups carries the class of a point to the corresponding class for the target subgroup.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquiv_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (x : SubgroupFiberOrbitQuotient H b) : cast ⋯ ((subgroupFiberOrbitQuotientEquiv (Homeomorph.refl E) ⋯ H b) x) = x

The identity over-base homeomorphism induces the identity on subgroup fibre-orbit quotients, up to the canonical rewrite identifying the image of a subgroup under the identity conjugation with the original subgroup.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquiv_trans {E : Type u_1} {F : Type u_2} {G : Type u_3} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] {p : E → B} {q : F → B} {r : G → B} {b : B} (h : E ≃ₜ F) (k : F ≃ₜ G) (hpq : ∀ (e : E), q (h e) = p e) (hqr : ∀ (f : F), r (k f) = q f) (H : Subgroup ↥(deck p)) (x : SubgroupFiberOrbitQuotient H b) : (subgroupFiberOrbitQuotientEquiv (h.trans k) ⋯ H b) x = (Equiv.cast ⋯) ((subgroupFiberOrbitQuotientEquiv k hqr (Subgroup.map (↑(conjMulEquiv h hpq)) H) b) ((subgroupFiberOrbitQuotientEquiv h hpq H b) x))

Subgroup fibre-orbit quotient equivalences compose as the underlying over-base homeomorphisms compose, with subgroup maps rewritten along conjugation composition.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientEquiv_mapOfLE {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) {H K : Subgroup ↥(deck p)} (hHK : H ≤ K) : ⇑(subgroupFiberOrbitQuotientEquiv h hpq K b) ∘ subgroupFiberOrbitMapOfLE hHK = subgroupFiberOrbitMapOfLE ⋯ ∘ ⇑(subgroupFiberOrbitQuotientEquiv h hpq H b)

Transport of subgroup fibre-orbit quotients is natural with respect to maps induced by subgroup inclusions.

noncomputable def TauCeti.Deck.subgroupFiberOrbitQuotientBotEquiv {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} : SubgroupFiberOrbitQuotient ⊥ b ≃ ↑(p ⁻¹' {b})

Quotienting a fibre by the trivial deck subgroup gives the fibre itself.

Equations

• TauCeti.Deck.subgroupFiberOrbitQuotientBotEquiv = TauCeti.MulAction.orbitRelQuotientBotEquiv

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientBotEquiv_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitQuotientBotEquiv (subgroupFiberOrbitClass ⊥ e) = e

The bottom-subgroup quotient equivalence sends a class to its representative fibre point.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientBotEquiv_symm_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitQuotientBotEquiv.symm e = subgroupFiberOrbitClass ⊥ e

The inverse bottom-subgroup quotient equivalence sends a fibre point to its quotient class.

theorem TauCeti.Deck.subgroupFiberOrbitClass_bot_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitClass ⊥ e = subgroupFiberOrbitClass ⊥ e' ↔ e = e'

Equality of bottom-subgroup fibre-orbit classes is equality of fibre points.

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_bot_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitMapOfLE ⋯ (subgroupFiberOrbitQuotientBotEquiv.symm e) = subgroupFiberOrbitClass H e

The quotient map induced by ⊥ ≤ H, after identifying the bottom quotient with the fibre, is the H-orbit class map.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_bot_eq {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : subgroupFiberOrbitMapOfLE ⋯ = (fun (e : ↑(p ⁻¹' {b})) => subgroupFiberOrbitClass H e) ∘ ⇑subgroupFiberOrbitQuotientBotEquiv

The map from the bottom-subgroup quotient to the H-quotient is the H-orbit class map under the bottom quotient equivalence.

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_bot_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (x y : SubgroupFiberOrbitQuotient ⊥ b) : subgroupFiberOrbitMapOfLE ⋯ x = subgroupFiberOrbitMapOfLE ⋯ y ↔ subgroupFiberOrbitQuotientBotEquiv x ∈ MulAction.orbit (↥H) (subgroupFiberOrbitQuotientBotEquiv y)

Equality in an H-fibre quotient can be checked after choosing representatives through the bottom quotient.

def TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} : SubgroupFiberOrbitQuotient ⊤ b ≃ FiberOrbitQuotient p b

The quotient by the full deck group is the previously defined deck fibre-orbit quotient.

Equations

• TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv = Quotient.congr (Equiv.refl ↑(p ⁻¹' {b})) ⋯

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitQuotientTopEquiv (subgroupFiberOrbitClass ⊤ e) = fiberOrbitClass e

The top-subgroup quotient equivalence sends a class to the full deck-orbit class of the same fibre point.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv_symm_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitQuotientTopEquiv.symm (fiberOrbitClass e) = subgroupFiberOrbitClass ⊤ e

The inverse top-subgroup quotient equivalence sends a full deck-orbit class to the class for the top subgroup.

def TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : SubgroupFiberOrbitQuotient H b → FiberOrbitQuotient p b

The map from the quotient of one fibre by H to the full deck-orbit quotient, induced by the subgroup inclusion H ≤ ⊤.

Equations

• TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit H = ⇑TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv ∘ TauCeti.Deck.subgroupFiberOrbitMapOfLE ⋯

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_apply {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) : subgroupFiberOrbitMapToFiberOrbit H (subgroupFiberOrbitClass H e) = fiberOrbitClass e

Forgetting from H-orbits to full deck orbits sends a class to the full orbit class of the same fibre point.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_top {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} : subgroupFiberOrbitMapToFiberOrbit ⊤ = ⇑subgroupFiberOrbitQuotientTopEquiv

For H = ⊤, forgetting from H-orbits to full deck orbits is the top-subgroup identification already supplied by subgroupFiberOrbitQuotientTopEquiv.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitClass_top_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitClass ⊤ e = subgroupFiberOrbitClass ⊤ e' ↔ fiberOrbitClass e = fiberOrbitClass e'

The top-subgroup equivalence identifies equality of top-subgroup classes with equality of the corresponding full deck-orbit classes.

theorem TauCeti.Deck.subgroupFiberOrbitClass_top_eq_iff_mem_orbit {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitClass ⊤ e = subgroupFiberOrbitClass ⊤ e' ↔ e ∈ MulAction.orbit (↥(deck p)) e'

Equality of top-subgroup fibre-orbit classes is membership in a full deck orbit.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitQuotientTopEquiv_mapOfLE {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H : Subgroup ↥(deck p)) : ⇑subgroupFiberOrbitQuotientTopEquiv ∘ subgroupFiberOrbitMapOfLE ⋯ = subgroupFiberOrbitMapToFiberOrbit H

The map induced by H ≤ ⊤, after identifying the top quotient with the full deck-orbit quotient, is subgroupFiberOrbitMapToFiberOrbit.

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_apply_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K L : Subgroup ↥(deck p)} (hHL : H ≤ L) (hKL : K ≤ L) (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitMapOfLE hHL (subgroupFiberOrbitClass H e) = subgroupFiberOrbitMapOfLE hKL (subgroupFiberOrbitClass K e') ↔ e ∈ MulAction.orbit (↥L) e'

Equality after mapping two subgroup fibre-orbit representatives into a common supergroup quotient is exactly membership in the common supergroup orbit.

theorem TauCeti.Deck.subgroupFiberOrbitMapOfLE_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K L : Subgroup ↥(deck p)} (hHL : H ≤ L) (hKL : K ≤ L) (x : SubgroupFiberOrbitQuotient H b) (y : SubgroupFiberOrbitQuotient K b) : subgroupFiberOrbitMapOfLE hHL x = subgroupFiberOrbitMapOfLE hKL y ↔ ∃ (e : ↑(p ⁻¹' {b})) (e' : ↑(p ⁻¹' {b})), x = subgroupFiberOrbitClass H e ∧ y = subgroupFiberOrbitClass K e' ∧ e ∈ MulAction.orbit (↥L) e'

Equality after mapping two subgroup fibre quotients into a common supergroup quotient can be checked on representatives from the common supergroup orbit.

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_apply_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H K : Subgroup ↥(deck p)) (e e' : ↑(p ⁻¹' {b})) : subgroupFiberOrbitMapToFiberOrbit H (subgroupFiberOrbitClass H e) = subgroupFiberOrbitMapToFiberOrbit K (subgroupFiberOrbitClass K e') ↔ e ∈ MulAction.orbit (↥(deck p)) e'

Equality after forgetting from H-orbits to full deck orbits is exactly membership of representatives in the same full deck orbit.

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (H K : Subgroup ↥(deck p)) (x : SubgroupFiberOrbitQuotient H b) (y : SubgroupFiberOrbitQuotient K b) : subgroupFiberOrbitMapToFiberOrbit H x = subgroupFiberOrbitMapToFiberOrbit K y ↔ ∃ (e : ↑(p ⁻¹' {b})) (e' : ↑(p ⁻¹' {b})), x = subgroupFiberOrbitClass H e ∧ y = subgroupFiberOrbitClass K e' ∧ e ∈ MulAction.orbit (↥(deck p)) e'

Equality after forgetting from subgroup fibre quotients to full deck orbits can be checked on representatives, even when the two subgroup quotients come from different subgroups.

@[simp]

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_mapOfLE {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} {H K : Subgroup ↥(deck p)} (hHK : H ≤ K) (x : SubgroupFiberOrbitQuotient H b) : subgroupFiberOrbitMapToFiberOrbit K (subgroupFiberOrbitMapOfLE hHK x) = subgroupFiberOrbitMapToFiberOrbit H x

If H ≤ K, forgetting H-orbits to full deck orbits factors through the K-orbit quotient.

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_eq {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} [Subsingleton (FiberOrbitQuotient p b)] (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) (x : SubgroupFiberOrbitQuotient H b) : subgroupFiberOrbitMapToFiberOrbit H x = fiberOrbitClass e

If the full deck-orbit quotient of a fibre is a subsingleton, every H-fibre orbit maps to the same full deck-orbit class as any chosen point of the fibre.

theorem TauCeti.Deck.subgroupFiberOrbitMapToFiberOrbit_eq_subgroupFiberOrbitMapToFiberOrbit {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} [Subsingleton (FiberOrbitQuotient p b)] (H K : Subgroup ↥(deck p)) (x : SubgroupFiberOrbitQuotient H b) (y : SubgroupFiberOrbitQuotient K b) : subgroupFiberOrbitMapToFiberOrbit H x = subgroupFiberOrbitMapToFiberOrbit K y

If the full deck-orbit quotient of a fibre is a subsingleton, forgetting any two subgroup fibre-orbit classes to full deck orbits gives the same result.

theorem TauCeti.Deck.IsRegular.subgroupFiberOrbitMapToFiberOrbit_eq {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (hreg : IsRegular p) (H : Subgroup ↥(deck p)) (e : ↑(p ⁻¹' {b})) (x : SubgroupFiberOrbitQuotient H b) : subgroupFiberOrbitMapToFiberOrbit H x = fiberOrbitClass e

For a regular deck action, every H-fibre orbit maps to the same full deck-orbit class as any chosen point of the fibre.

theorem TauCeti.Deck.IsRegular.subgroupFiberOrbitMapToFiberOrbit_eq_subgroupFiberOrbitMapToFiberOrbit {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (hreg : IsRegular p) (H K : Subgroup ↥(deck p)) (x : SubgroupFiberOrbitQuotient H b) (y : SubgroupFiberOrbitQuotient K b) : subgroupFiberOrbitMapToFiberOrbit H x = subgroupFiberOrbitMapToFiberOrbit K y

For a regular deck action, forgetting any two subgroup fibre-orbit classes to full deck orbits gives the same result.