The balanced product of a quotient covering map with a discrete set

Let a group G act on a space E so that q : E → X presents X as the quotient E / G in the strong sense of Mathlib's IsQuotientCoveringMap: the fibres of q are the orbits, and every point of E has a neighbourhood whose G-translates are pairwise disjoint. For a discrete G-set A, the balanced product BalancedProduct G E A is the quotient of E × A by the diagonal action of G. Since q is invariant along the first factor it descends to

BalancedProduct.proj A : BalancedProduct G E A → X,

and the theorem of this file is that this projection is a covering map, with fibre A.

Neither space is assumed connected, and no local connectedness of X is needed. Over the base set q '' U cut out by a set U whose G-translates are pairwise disjoint, the sheets of the projection are the images of U ×ˢ {a}, one for each a : A, and each defining property of a sheet comes straight from the disjointness of those translates: two points of U with the same class differ by a group element carrying U into itself, hence by the identity.

The intended reading is the cover of X attached to a set acted on by the deck group of a regular cover. For E the universal cover of X and G its fundamental group, this is the covering space attached to an arbitrary π₁(X, x₀)-set; no transitivity, and hence no connectedness of the resulting cover, is assumed. The transitive case A = G ⧸ H, where the balanced product is E / H, is IsQuotientCoveringMap.isCoveringMap_of_comp, proved there for an abstract presentation of E / H rather than for a fixed model.

Main declarations

• TauCeti.BalancedProduct: the quotient of E × A by the diagonal action of G.
• TauCeti.isQuotientCoveringMap_quotientMk_of_smul_disjoint: an action with locally pairwise disjoint translates presents its orbit space as a quotient covering map.
• TauCeti.BalancedProduct.isQuotientCoveringMap_mk: the class map E × A → E ×_G A is one such.
• TauCeti.BalancedProduct.isCoveringMap_proj: the balanced product of a quotient covering map with a discrete set is a covering map.
• TauCeti.BalancedProduct.fiberEquiv: its fibre over q e is A, through a ↦ ⟦(e, a)⟧. This last bijection is purely algebraic: it uses no topology, only that the action on E is free and that the fibres of q are its orbits.

References

The IsQuotientCoveringMap interface used here — the predicate itself, its disjoint and apply_eq_iff_mem_orbit fields, IsQuotientCoveringMap.isOpenQuotientMap, and IsOpen.trivializationDiscrete — is Junyan Xu's, in Mathlib/Topology/Covering/Quotient.lean and Mathlib/Topology/Covering/Basic.lean. The sheet bookkeeping follows the subgroup case in TauCeti/Topology/Covering/Quotient.lean.

theorem TauCeti.isQuotientCoveringMap_quotientMk_of_smul_disjoint {E : Type u_1} [TopologicalSpace E] {G : Type u_2} [Group G] [MulAction G E] [ContinuousConstSMul G E] (hdisj : ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun (x : E) => g • x) '' U ∩ U).Nonempty → g = 1) : IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G E)) G

An action whose translates are locally pairwise disjoint presents its orbit space as a quotient covering map. This is the free, not necessarily properly discontinuous, form of Mathlib's isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul: no local compactness or separation of E is assumed.

@[reducible, inline]

abbrev TauCeti.BalancedProduct (G : Type u_5) (E : Type u_6) (A : Type u_7) [Group G] [MulAction G E] [MulAction G A] : Type (max u_6 u_7)

The balanced product E ×_G A of a G-space E and a G-set A: the quotient of E × A by the diagonal action of G.

Equations

• TauCeti.BalancedProduct G E A = Quotient (MulAction.orbitRel G (E × A))

@[reducible, inline]

abbrev TauCeti.BalancedProduct.mk {E : Type u_1} {A : Type u_3} (G : Type u_5) [Group G] [MulAction G E] [MulAction G A] (e : E) (a : A) : BalancedProduct G E A

The class of a pair in the balanced product.

Equations

• TauCeti.BalancedProduct.mk G e a = ⟦(e, a)⟧

@[simp]

theorem TauCeti.BalancedProduct.mk_smul_left {E : Type u_1} {A : Type u_3} {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] (g : G) (e : E) (a : A) : mk G (g • e) a = mk G e (g⁻¹ • a)

Moving a point of E × A by g in the first coordinate is the same as moving it by g⁻¹ in the second.

def TauCeti.BalancedProduct.proj {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) : BalancedProduct G E A → X

A G-invariant map q : E → X descends to the balanced product.

Equations

• TauCeti.BalancedProduct.proj A hq = Quotient.lift (fun (p : E × A) => q p.1) ⋯

@[simp]

theorem TauCeti.BalancedProduct.proj_mk {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) (e : E) (a : A) : proj A hq (mk G e a) = q e

theorem TauCeti.BalancedProduct.continuous_proj {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] (hqc : Continuous q) : Continuous (proj A hq)

The descended projection is continuous when q is.

theorem TauCeti.BalancedProduct.isQuotientCoveringMap_mk {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] [ContinuousConstSMul G A] (hqc : IsQuotientCoveringMap q G) : IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G (E × A))) G

The class map onto the balanced product is a quotient covering map for the diagonal action, as soon as the action on E is one and the action on A is continuous: a neighbourhood U of e with pairwise disjoint translates gives the neighbourhood U ×ˢ univ of (e, a), whose translates are again pairwise disjoint.

theorem TauCeti.BalancedProduct.isCoveringMap_proj {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] [DiscreteTopology A] (hqc : IsQuotientCoveringMap q G) : IsCoveringMap (proj A hq)

The balanced product of a quotient covering map with a discrete set is a covering map.

If q : E → X presents X as the quotient of E by a group G in the sense of IsQuotientCoveringMap, and A is a discrete G-set, then the descended projection of the balanced product E ×_G A to X is a covering map.

noncomputable def TauCeti.BalancedProduct.fiberEquiv {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) [IsCancelSMul G E] (hfiber : ∀ {e₁ e₂ : E}, q e₁ = q e₂ → e₁ ∈ MulAction.orbit G e₂) {x : X} (e : ↑(q ⁻¹' {x})) : A ≃ ↑(proj A hq ⁻¹' {x})

The fibre of the balanced product over x is A. The bijection sends a to the class of (e, a); it depends on the chosen point e of the fibre of q.

Only two consequences of q being a quotient covering map are used, and neither involves a topology: the action on E is free, and points of E with the same image lie in one orbit.

Equations

• TauCeti.BalancedProduct.fiberEquiv A hq hfiber e = Equiv.ofBijective (fun (a : A) => ⟨TauCeti.BalancedProduct.mk G (↑e) a, ⋯⟩) ⋯

@[simp]

theorem TauCeti.BalancedProduct.fiberEquiv_apply_coe {E : Type u_1} {X : Type u_2} (A : Type u_3) {G : Type u_4} [Group G] [MulAction G E] [MulAction G A] {q : E → X} (hq : ∀ (g : G) (e : E), q (g • e) = q e) [IsCancelSMul G E] (hfiber : ∀ {e₁ e₂ : E}, q e₁ = q e₂ → e₁ ∈ MulAction.orbit G e₂) {x : X} (e : ↑(q ⁻¹' {x})) (a : A) : ↑((fiberEquiv A hq ⋯ e) a) = mk G (↑e) a

The fibre bijection of the balanced product sends a to the class of (e, a).