Fibres of maps between orbit spaces

If H has finite index in K, every fibre of the map from H-orbits to K-orbits is finite. The cosets of H in K cover each fibre by translating a representative of the larger orbit. This applies even when the ambient action has nontrivial stabilizers.

When the stabilizer of the representative acts trivially on the coset space, distinct cosets give distinct H-orbits. The resulting equivalence counts the fibre by the subgroup index, with no finite-index assumption. For an infinite index, both Nat.card and the index are zero.

In general, the stabilizer of the representative acts on the coset space, and its orbit space is exactly the fibre of the map between orbit spaces. Thus two cosets give the same point of the fibre precisely when they lie in the same stabilizer orbit. In geometric applications satisfying the relevant hypotheses, these identifications can describe ramification.

noncomputable def TauCeti.cosetToOrbitRelMapFiber {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) : ↥K ⧸ H.subgroupOf K → { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = Quotient.mk'' x }

A coset determines a point in the fibre over the orbit of x.

Equations

• TauCeti.cosetToOrbitRelMapFiber h x c = ⟨TauCeti.orbitOfCosetTranslate x c, ⋯⟩

@[simp]

theorem TauCeti.cosetToOrbitRelMapFiber_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) (q : ↥K ⧸ H.subgroupOf K) : ↑(cosetToOrbitRelMapFiber h x q) = orbitOfCosetTranslate x q

The coset-to-fibre map sends a coset to the orbit of its inverse translate.

theorem TauCeti.cosetToOrbitRelMapFiber_surjective {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) : Function.Surjective (cosetToOrbitRelMapFiber h x)

Every orbit in the fibre is represented by a coset.

theorem TauCeti.finite_fiber_orbitRel_map_of_isFiniteRelIndex {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) [H.IsFiniteRelIndex K] (p : MulAction.orbitRel.Quotient (↥K) X) : Finite { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = p }

Every fibre of the orbit map for a finite-index subgroup inclusion is finite.

noncomputable def TauCeti.stabilizerOrbitRelQuotientEquivOrbitRelMapFiber {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (↥K) x)) (↥K ⧸ H.subgroupOf K) ≃ { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = Quotient.mk'' x }

The fibre over the orbit of x is the orbit space for the action of the stabilizer of x on the cosets of the smaller subgroup.

The stabilizer acts by left translation. Two cosets determine the same smaller-subgroup orbit precisely when they lie in the same stabilizer orbit.

Equations

• TauCeti.stabilizerOrbitRelQuotientEquivOrbitRelMapFiber h x = (Quotient.congrRight ⋯).trans (Setoid.quotientKerEquivOfSurjective (TauCeti.cosetToOrbitRelMapFiber h x) ⋯)

@[simp]

theorem TauCeti.stabilizerOrbitRelQuotientEquivOrbitRelMapFiber_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) (q : ↥K ⧸ H.subgroupOf K) : ↑((stabilizerOrbitRelQuotientEquivOrbitRelMapFiber h x) (Quotient.mk'' q)) = orbitOfCosetTranslate x q

The stabilizer-orbit equivalence sends the orbit of a coset to the smaller-subgroup orbit of the corresponding inverse translate.

theorem TauCeti.card_fiber_orbitRel_map_eq_card_stabilizerOrbitRelQuotient {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) : Nat.card { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = Quotient.mk'' x } = Nat.card (MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (↥K) x)) (↥K ⧸ H.subgroupOf K))

The cardinality of an orbit-map fibre is the number of stabilizer-orbits on the subgroup coset space. Several cosets can lie in one stabilizer orbit and hence determine the same point of the fibre. In geometric applications satisfying the relevant hypotheses, these identifications can describe ramification.

noncomputable def TauCeti.cosetsEquivOrbitRelMapFiber {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) (hx : MulAction.stabilizer (↥K) x ≤ (H.subgroupOf K).normalCore) : ↥K ⧸ H.subgroupOf K ≃ { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = Quotient.mk'' x }

If the stabilizer acts trivially on the coset space, the fibre of an orbit map is indexed exactly by the cosets of the smaller subgroup in the larger one.

Equations

• TauCeti.cosetsEquivOrbitRelMapFiber h x hx = Equiv.ofBijective (TauCeti.cosetToOrbitRelMapFiber h x) ⋯

@[simp]

theorem TauCeti.cosetsEquivOrbitRelMapFiber_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) (hx : MulAction.stabilizer (↥K) x ≤ (H.subgroupOf K).normalCore) (q : ↥K ⧸ H.subgroupOf K) : ↑((cosetsEquivOrbitRelMapFiber h x hx) q) = orbitOfCosetTranslate x q

A coset maps to the smaller-subgroup orbit of the inverse translate.

theorem TauCeti.card_fiber_orbitRel_map_of_stabilizer_le_normalCore {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) (x : X) (hx : MulAction.stabilizer (↥K) x ≤ (H.subgroupOf K).normalCore) : Nat.card { q : MulAction.orbitRel.Quotient (↥H) X // Setoid.map_of_le ⋯ q = Quotient.mk'' x } = (H.subgroupOf K).index

The fibre cardinality equals the subgroup index when the stabilizer acts trivially on the coset space.