Subgroup fibre orbits of a regular cover as deck-group quotients #
For a regular preconnected covering map, evaluation at any point of a fibre identifies the
deck group with that fibre. This file records the corresponding quotient-level statement:
orbits of a subgroup H ≤ deck p on the fibre are equivalent to the coset quotient
deck p ⧸ H.
The classification of connected covers uses fibre quotients by subgroups, while the regular-cover
computation of the deck group of the cover attached to H is expressed algebraically as a
normalizer quotient. The bridge here lets arguments move between those fibre-orbit quotients and
subgroup quotients without unfolding either construction.
Main declarations #
TauCeti.Deck.subgroupFiberOrbitQuotientEquivQuotientGroup: identifiesSubgroupFiberOrbitQuotient H bwithdeck p ⧸ H.TauCeti.Deck.regularSubgroupFiberOrbitQuotientEquivQuotientGroup: the regular-cover specialization that installs the free-transitive deck action on the fibre.TauCeti.Deck.subgroupFiberOrbitQuotientEquivQuotientGroup_mapOfLE: compatibility with the maps induced by subgroup inclusions.TauCeti.Deck.subgroupFiberOrbitQuotientBotEquivDeck: forH = ⊥, the quotient is the deck group, with the inverse orientation coming from Mathlib's quotient convention.- Endpoint collapse lemmas for
H = ⊤.
References #
It is a deck-specific specialization of Mathlib's
MulAction.equivSubgroupOrbitsQuotientGroup, the orbit-quotient form of the
orbit-stabilizer theorem for free transitive actions.
The subgroup-fibre orbit quotient is equivalent to the quotient of the deck group by the subgroup, once the deck action on the chosen fibre is free and transitive.
Equations
Instances For
For a regular preconnected covering map, the subgroup-fibre orbit quotient is equivalent to the quotient of the deck group by the subgroup.
Equations
Instances For
The inverse quotient equivalence sends the coset of a deck transformation φ to the
H-orbit class of the point φ⁻¹ • e.
For a regular cover, the inverse quotient equivalence sends the coset of a deck
transformation φ to the H-orbit class of φ⁻¹ • e.
On underlying points, the inverse quotient equivalence sends the coset of φ to the
class of the value of φ⁻¹ on the chosen fibre point.
The inverse quotient equivalence sends the identity coset to the orbit class of the chosen fibre point.
The quotient equivalence sends the orbit class of φ⁻¹ • e to the coset of φ.
For a regular cover, the quotient equivalence sends the orbit class of φ⁻¹ • e to the
coset of φ.
The quotient equivalence sends the chosen fibre point to the identity coset.
The quotient equivalence sends the orbit class of φ • e to the coset of φ⁻¹.
For a regular cover, the quotient equivalence sends the orbit class of φ • e to the
coset of φ⁻¹.
For a free transitive deck action on a fibre, quotienting the fibre by the trivial
subgroup identifies that quotient with the deck group. The representative convention is the
same as subgroupFiberOrbitQuotientEquivQuotientGroup: the class of φ • e corresponds to
φ⁻¹.
Equations
Instances For
For a regular preconnected covering map, the quotient of a fibre by the trivial deck subgroup is the deck group.
Equations
Instances For
The bottom-subgroup quotient-to-deck equivalence sends the class of φ • e to φ⁻¹.
For a regular cover, the bottom-subgroup quotient-to-deck equivalence sends the class of
φ • e to φ⁻¹.
The chosen fibre point maps to the identity deck transformation under the bottom-subgroup quotient-to-deck equivalence.
For a regular cover, the chosen fibre point maps to the identity deck transformation under the bottom-subgroup quotient-to-deck equivalence.
The inverse bottom-subgroup quotient-to-deck equivalence sends a deck transformation to the class of its inverse acting on the chosen fibre point.
For a regular cover, the inverse bottom-subgroup quotient-to-deck equivalence sends a deck transformation to the class of its inverse acting on the chosen fibre point.
Under the quotient-group equivalence, the full-subgroup fibre quotient lands in the
unique coset of deck p ⧸ ⊤.
For a regular cover, the full-subgroup fibre quotient lands in the unique coset of
deck p ⧸ ⊤.
The subgroup-fibre quotient equivalence is natural in subgroup inclusions.
For a regular cover, the subgroup-fibre quotient equivalence is natural in subgroup inclusions.
Equality of subgroup fibre-orbit classes is equality of the corresponding deck cosets under the quotient equivalence, with the inverse orientation coming from Mathlib's quotient convention.