The deck group of an intermediate quotient is a normalizer quotient #
Let p : E → X be a quotient covering map for a group Γ acting on E, let H ≤ Γ, and let
q : E → F present F as the quotient of E by H, so that p factors as r ∘ q for a
covering map r : F → X. This file computes the deck transformation group of the intermediate
covering r:
deck r ≃* N(H) ⧸ H,
where N(H) is the normalizer of H in Γ. Taking H = ⊥ recovers
TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv, which identifies deck p with Γ itself.
Only a normalizer element descends to the quotient as a deck transformation: translation by
γ respects the H-orbit relation, so descends as a map, exactly when γ H γ⁻¹ ⊆ H, while
the descended map is invertible, hence a homeomorphism, exactly when γ H γ⁻¹ = H, that is,
when γ normalizes H.
Conversely every deck transformation of r arises this way, by uniqueness of lifts. A deck
transformation φ of r, precomposed with q, and translation by a suitable γ followed by
q, are two lifts of p through r which agree at one point of the preconnected space E,
hence agree everywhere; comparing the translates of a single point then forces γ to
normalize H.
Main declarations #
TauCeti.Deck.IsQuotientCoveringMap.normalizerMap: translation by a normalizer element, descended to the orbit quotient.TauCeti.Deck.IsQuotientCoveringMap.normalizerDeckHom: the resulting homomorphism from the normalizer todeck r.TauCeti.Deck.IsQuotientCoveringMap.ker_normalizerDeckHom: its kernel isH.TauCeti.Deck.IsQuotientCoveringMap.normalizerDeckHom_surjective: it is surjective whenEis preconnected andris a covering map.TauCeti.Deck.IsQuotientCoveringMap.normalizerQuotientDeckMulEquiv: the deck group ofrisN(H) ⧸ H.TauCeti.Deck.IsQuotientCoveringMap.quotientDeckMulEquivOfNormal: for normalHthis readsdeck r ≃* Γ ⧸ H.
References #
The cover attached to H ≤ π₁(X, x₀) has deck group N(H)/H, and π₁(X, x₀)/H when H is
normal. The quotient-covering-map interface it
consumes (Mathlib/Topology/Covering/Quotient.lean) is due to Junyan Xu, and uniqueness of
lifts, IsCoveringMap.eq_of_comp_eq in Mathlib/Topology/Covering/Basic.lean, is due to
Thomas Browning after Hatcher, Algebraic Topology, Proposition 1.34.
Translation by an element of the normalizer of H, descended to the quotient of E by the
H-action. It is well defined because γ H γ⁻¹ = H.
Equations
- TauCeti.Deck.IsQuotientCoveringMap.normalizerMap hq γ y = q (↑γ • Function.surjInv ⋯ y)
Instances For
The descended translation sends the class of e to the class of γ • e.
The identity of the normalizer descends to the identity.
Descending translations is multiplicative, the right factor acting first.
The descended translation is continuous, because q is a quotient map.
Translation by a normalizer element, as a homeomorphism of the orbit quotient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of the descended translation is translation by the inverse.
Translation by an element normalizing H, as a homomorphism from the normalizer to the
deck transformation group of the intermediate covering r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On points, the deck transformation attached to a normalizer element is the descent of translation by that element.
The inverse of the deck transformation attached to a normalizer element is the descent of translation by the inverse element.
The kernel of the normalizer-to-deck homomorphism is H: a translation descends to the
identity exactly when it is an H-translation, because the Γ-action is free.
Every deck transformation of the intermediate covering is the descent of a translation by a normalizer element.
The deck group of an intermediate covering is the normalizer quotient. For a quotient
covering map p : E → X with preconnected nonempty total space, a subgroup H of the acting
group, and the induced covering r : E / H → X, translation identifies N(H) ⧸ H with
deck r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The normalizer-quotient isomorphism sends the class of γ to the descent of translation
by γ.
For a normal subgroup every group element descends, giving a homomorphism from the whole acting group to the deck group of the intermediate covering.
Equations
Instances For
The inverse of the deck transformation attached to γ is the descent of translation by
γ⁻¹.
For a normal subgroup, the deck group of the intermediate covering is Γ ⧸ H. This is
the general normalizer-quotient identification, read through the algebraic comparison
Subgroup.normalizerQuotientEquivQuotientOfNormal between N(H) ⧸ H and Γ ⧸ H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The isomorphism Γ ⧸ H ≃* deck r sends the class of γ to the descent of translation
by γ.