Coordinate topology on permutation wreath products

The base has the product topology and the permutation group has the topology of pointwise convergence. Relabeling the index type by a continuous equivalence is continuous. When the base is a topological group and the index type is discrete, this topology makes the wreath product a topological group.

This is the topology used to prove continuity of Subgroup.monomialHom and Subgroup.monomialFinHom for an open subgroup. Pointwise convergence on the permutation factor reduces that part of continuity to the orbit maps of individual cosets. TauCeti.WreathProduct.continuous_iff gives the coordinate criterion for maps into the wreath product, and TauCeti.WreathProduct.isEmbedding_left_right identifies it with its image in the product of the two function spaces.

@[instance_reducible]

instance TauCeti.WreathProduct.instTopologicalSpace (D : Type u) (ι : Type v) [Group D] [TopologicalSpace D] [TopologicalSpace ι] : TopologicalSpace (WreathProduct D ι)

The coordinate topology on a permutation wreath product. The base coordinates have the product topology, while the permutation has the topology of pointwise convergence.

Equations

• TauCeti.WreathProduct.instTopologicalSpace D ι = TopologicalSpace.induced (fun (w : TauCeti.WreathProduct D ι) => (w.left, ⇑w.right)) inferInstance

theorem TauCeti.WreathProduct.isInducing_left_right {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] : Topology.IsInducing fun (w : WreathProduct D ι) => (w.left, ⇑w.right)

The coordinate map induces the topology on the permutation wreath product.

theorem TauCeti.WreathProduct.isEmbedding_left_right {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] : Topology.IsEmbedding fun (w : WreathProduct D ι) => (w.left, ⇑w.right)

The coordinate map embeds the permutation wreath product into the product of function spaces.

theorem TauCeti.WreathProduct.continuous_iff {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] {α : Type u_2} [TopologicalSpace α] {f : α → WreathProduct D ι} : Continuous f ↔ (∀ (i : ι), Continuous fun (a : α) => (f a).left i) ∧ ∀ (i : ι), Continuous fun (a : α) => (f a).right i

A map into a permutation wreath product is continuous exactly when each base and permutation coordinate is continuous.

theorem TauCeti.WreathProduct.continuous_left {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] (i : ι) : Continuous fun (w : WreathProduct D ι) => w.left i

Evaluation of a base coordinate is continuous.

theorem TauCeti.WreathProduct.continuous_right {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] (i : ι) : Continuous fun (w : WreathProduct D ι) => w.right i

Evaluation of a permutation coordinate is continuous.

theorem TauCeti.WreathProduct.continuous_right_inv {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [DiscreteTopology ι] (i : ι) : Continuous fun (w : WreathProduct D ι) => w.right⁻¹ i

Evaluation of the inverse permutation coordinate is continuous when the index is discrete.

theorem TauCeti.WreathProduct.continuous_left_eval {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [DiscreteTopology ι] : Continuous fun (p : WreathProduct D ι × ι) => p.1.left p.2

Joint evaluation of a base coordinate is continuous for a discrete index type.

theorem TauCeti.WreathProduct.continuous_right_eval {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [DiscreteTopology ι] : Continuous fun (p : WreathProduct D ι × ι) => p.1.right p.2

Joint evaluation of a permutation coordinate is continuous for a discrete index type.

instance TauCeti.WreathProduct.instContinuousMul {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [ContinuousMul D] [DiscreteTopology ι] : ContinuousMul (WreathProduct D ι)

Multiplication is continuous when the base has continuous multiplication and the index is discrete.

instance TauCeti.WreathProduct.instContinuousInv {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [ContinuousInv D] [DiscreteTopology ι] : ContinuousInv (WreathProduct D ι)

Inversion is continuous when the base has continuous inversion and the index is discrete.

instance TauCeti.WreathProduct.instIsTopologicalGroup {D : Type u} {ι : Type v} [Group D] [TopologicalSpace D] [TopologicalSpace ι] [IsTopologicalGroup D] [DiscreteTopology ι] : IsTopologicalGroup (WreathProduct D ι)

The coordinate topology makes a wreath product a topological group when the base is one and the index type is discrete.

theorem TauCeti.WreathProduct.continuous_congr {D : Type u} {ι : Type v} [Group D] {κ : Type u_1} [TopologicalSpace D] [TopologicalSpace ι] [TopologicalSpace κ] (e : ι ≃ κ) (he : Continuous ⇑e) : Continuous ⇑(congr e)

Relabeling a wreath product is continuous when the relabeling of its index type is continuous.