The topological group extension built from a continuous factor set

A factor set α : FactorSet G M builds the group extension 1 → M → E_α → G → 1 whose underlying set is M × G and whose multiplication is twisted by α. When G and M are topological groups, the action of G on M is continuous and α is continuous, the product topology on M × G makes E_α a topological group. The projection to G is an open quotient map, and — as soon as G is T1, so that the range of the inclusion, the preimage of {1}, is closed — the inclusion of M is a closed embedding. For G a profinite group and M a finite discrete module this exhibits E_α as a profinite group, which is the extension attached to a continuous 2-cocycle.

The topology is put on TauCeti.FactorSet.Extension unconditionally, as the product topology transported along the coordinate equivalence TauCeti.FactorSet.Extension.equivProd. The group structure itself needs no continuity at all; what needs α and the action of G on M to be continuous is the compatibility of the group operations with the topology. The separation, compactness and disconnectedness instances below hold for every factor set.

Continuity of a factor set is membership of the explicit complex of continuous cochains: TauCeti.FactorSet.ofMul_mem_Z2_iff says that α is continuous exactly when it is a continuous 2-cocycle in the sense of TauCeti.ContCohomology.Z2, once read additively through Additive.ofMul. Conversely TauCeti.FactorSet.ofMemZ2 names the factor set of a normalized continuous 2-cocycle, so the two descriptions of the data are interchangeable.

Main definitions

• TauCeti.FactorSet.Extension.equivProd: the twisted product is M × G as a type, and TauCeti.FactorSet.Extension.instTopologicalSpace transports the product topology along it.
• TauCeti.FactorSet.Extension.homeomorphProd: the twisted product is M × G as a space.
• TauCeti.FactorSet.ofMemZ2: the factor set named by a normalized continuous 2-cocycle.

Main results

• TauCeti.FactorSet.Extension.isTopologicalGroup: over a continuous action of G on M, a continuous factor set builds a topological group.
• TauCeti.FactorSet.isClosedEmbedding_inl and TauCeti.FactorSet.isQuotientMap_rightHom: for G a T1 space the copy of M is a closed subgroup, and the projection to G is an open quotient map, so 1 → M → E_α → G → 1 is an extension of topological groups.
• TauCeti.FactorSet.continuous_canonicalSection: the canonical section is continuous, so the extension built from a continuous factor set carries a continuous normalized section.
• TauCeti.FactorSet.continuous_map and TauCeti.FactorSet.continuous_mapExtension: the pushforward of a continuous factor set along a continuous equivariant homomorphism of coefficient modules is continuous, and so is the induced homomorphism of twisted products.
• TauCeti.FactorSet.ofMul_mem_Z2_iff: continuity of a factor set is membership of the explicit complex of continuous cochains.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2, for the description of an extension of profinite groups by a continuous 2-cocycle.
• L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., Ch. 6, §8.

@[instance_reducible]

instance TauCeti.FactorSet.Extension.instTopologicalSpace {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : TopologicalSpace α.Extension

The twisted product carries the product topology of M × G, transported along TauCeti.FactorSet.Extension.equivProd; see TauCeti.FactorSet.Extension.homeomorphProd.

Equations

• TauCeti.FactorSet.Extension.instTopologicalSpace α = (TauCeti.FactorSet.Extension.equivProd α).topologicalSpace

def TauCeti.FactorSet.Extension.homeomorphProd {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : α.Extension ≃ₜ M × G

The twisted product is M × G as a topological space. The multiplication is twisted by the factor set, the topology is not.

Equations

• TauCeti.FactorSet.Extension.homeomorphProd α = (TauCeti.FactorSet.Extension.equivProd α).homeomorph

@[simp]

theorem TauCeti.FactorSet.Extension.homeomorphProd_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} (x : α.Extension) : (homeomorphProd α) x = (x.left, x.right)

@[simp]

theorem TauCeti.FactorSet.Extension.homeomorphProd_symm_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} (p : M × G) : (homeomorphProd α).symm p = { left := p.1, right := p.2 }

theorem TauCeti.FactorSet.Extension.isInducing_leftRight {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} : Topology.IsInducing fun (x : α.Extension) => (x.left, x.right)

The defining property of the topology on the twisted product: it is induced from M × G. This is the lemma every continuity argument about the twisted product goes through.

theorem TauCeti.FactorSet.Extension.continuous_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} : Continuous left

theorem TauCeti.FactorSet.Extension.continuous_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} : Continuous right

instance TauCeti.FactorSet.Extension.instT2Space {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} [T2Space M] [T2Space G] : T2Space α.Extension

instance TauCeti.FactorSet.Extension.instCompactSpace {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} [CompactSpace M] [CompactSpace G] : CompactSpace α.Extension

instance TauCeti.FactorSet.Extension.instTotallyDisconnectedSpace {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} [TotallyDisconnectedSpace M] [TotallyDisconnectedSpace G] : TotallyDisconnectedSpace α.Extension

instance TauCeti.FactorSet.Extension.instDiscreteTopology {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} [DiscreteTopology M] [DiscreteTopology G] : DiscreteTopology α.Extension

The topological group structure

theorem TauCeti.FactorSet.Extension.isTopologicalGroup {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α : FactorSet G M} [ContinuousSMul G M] (hα : Continuous ⇑α) [IsTopologicalGroup G] [IsTopologicalGroup M] : IsTopologicalGroup α.Extension

Over a continuous action of G on M, a continuous factor set builds a topological group. The twisted multiplication of TauCeti.FactorSet.Extension is ⟨a, g⟩ * ⟨b, h⟩ = ⟨a * g • b * α (g, h), g * h⟩, so it is continuous for the product topology exactly because the two things appearing in it beyond the group operations — the action and the factor set — are.

The maps of the extension

theorem TauCeti.FactorSet.continuous_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : Continuous ⇑α.inl

theorem TauCeti.FactorSet.continuous_rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : Continuous ⇑α.rightHom

theorem TauCeti.FactorSet.isEmbedding_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : Topology.IsEmbedding ⇑α.inl

The coefficient inclusion carries the topology of M, without any separation assumption on the quotient group.

theorem TauCeti.FactorSet.continuous_trivial {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] : Continuous ⇑(trivial G M)

The trivial factor set is continuous, being constant.

theorem TauCeti.FactorSet.continuous_canonicalSection {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : Continuous ⇑α.canonicalSection

The canonical section g ↦ ⟨1, g⟩ of the projection is continuous: the extension built from a continuous factor set comes with a continuous normalized section, and TauCeti.GroupExtension.factorSet_canonicalSection reads the factor set back off it.

theorem TauCeti.FactorSet.isClosedEmbedding_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) [T1Space G] : Topology.IsClosedEmbedding ⇑α.inl

The copy of M inside the twisted product is a closed subgroup, and carries the topology of M. Only G needs a separation assumption: under TauCeti.FactorSet.Extension.homeomorphProd the inclusion is a ↦ (a, 1), whose range is the preimage of {1} under the projection to G.

theorem TauCeti.FactorSet.isOpenMap_rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : IsOpenMap ⇑α.rightHom

The projection of the twisted product onto G is open: under TauCeti.FactorSet.Extension.homeomorphProd it is the projection M × G → G.

theorem TauCeti.FactorSet.isQuotientMap_rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] (α : FactorSet G M) : Topology.IsQuotientMap ⇑α.rightHom

The projection of the twisted product onto G is a quotient map, so G carries the quotient topology of the extension by the copy of M.

Continuity of the pushforward along a coefficient map

theorem TauCeti.FactorSet.continuous_map {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {N : Type u_1} [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) (hf : Continuous ⇑f) (hα : Continuous ⇑α) : Continuous ⇑(α.map f)

The pushforward of a continuous factor set along a continuous equivariant homomorphism of coefficient modules is continuous.

theorem TauCeti.FactorSet.continuous_mapExtension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {N : Type u_1} [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) (hf : Continuous ⇑f) : Continuous ⇑(α.mapExtension f)

The homomorphism of twisted products induced by a continuous equivariant coefficient homomorphism is continuous: it is f on the M-coordinate and the identity on the G-coordinate.

Continuity of the rescaling equivalence

theorem TauCeti.FactorSet.continuous_rescaleEquiv {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α β : FactorSet G M} {x : G → M} (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) (hxc : Continuous x) [ContinuousMul M] : Continuous ⇑(α.rescaleEquiv β x hx)

The rescaling equivalence between the twisted products of α and β is continuous when the rescaling function x is: under TauCeti.FactorSet.Extension.homeomorphProd it is (a, g) ↦ (a * x g, g).

theorem TauCeti.FactorSet.continuous_rescaleEquiv_symm {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] {α β : FactorSet G M} {x : G → M} (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) (hxc : Continuous x) [ContinuousMul M] [ContinuousInv M] : Continuous ⇑(α.rescaleEquiv β x hx).symm

The inverse of the rescaling equivalence is continuous as well: it is the rescaling by x⁻¹.

Continuity as membership of the explicit complex of continuous cochains

theorem TauCeti.FactorSet.ofMul_mem_Z2_iff {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] [IsTopologicalGroup M] (α : FactorSet G M) : (fun (p : G × G) => Additive.ofMul (α p)) ∈ ContCohomology.Z2 G (Additive M) ↔ Continuous ⇑α

Continuity of a factor set is membership of the explicit complex of continuous cochains. Read additively, a factor set is a continuous 2-cocycle in the sense of TauCeti.ContCohomology.Z2 exactly when it is continuous as a function.

def TauCeti.FactorSet.ofMemZ2 {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] [IsTopologicalGroup M] {z : G × G → Additive M} (hz : z ∈ ContCohomology.Z2 G (Additive M)) (hz₁ : z (1, 1) = 0) : FactorSet G M

The factor set named by a normalized continuous 2-cocycle of the explicit complex of continuous cochains. Normalization is a hypothesis rather than a consequence: the cochains of that complex are not normalized, and TauCeti.ContCohomology.map_one_fst_of_mem_Z2 only says that the value at (1, g) is the value at (1, 1).

Equations

• TauCeti.FactorSet.ofMemZ2 hz hz₁ = { toFun := fun (p : G × G) => Additive.toMul (z p), isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.ofMemZ2_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] [IsTopologicalGroup M] {z : G × G → Additive M} (hz : z ∈ ContCohomology.Z2 G (Additive M)) (hz₁ : z (1, 1) = 0) (p : G × G) : (ofMemZ2 hz hz₁) p = Additive.toMul (z p)

theorem TauCeti.FactorSet.continuous_ofMemZ2 {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [TopologicalSpace G] [TopologicalSpace M] [IsTopologicalGroup M] {z : G × G → Additive M} (hz : z ∈ ContCohomology.Z2 G (Additive M)) (hz₁ : z (1, 1) = 0) : Continuous ⇑(ofMemZ2 hz hz₁)

The factor set named by a normalized continuous 2-cocycle is continuous. Continuity is one half of membership of TauCeti.ContCohomology.Z2, and TauCeti.FactorSet.ofMemZ2 changes only the notation, so the hypothesis of TauCeti.FactorSet.Extension.isTopologicalGroup is available for the extension built from a cocycle of the explicit complex of continuous cochains.