Topological isomorphisms between type tags

The multiplicative type tag of a product of additive topological groups is topologically isomorphic to the product of the multiplicative type tags, both for binary products and for dependent products, and when T has a unique element, Multiplicative (M × T) is topologically isomorphic to Multiplicative M. These are MulEquiv.prodMultiplicative, MulEquiv.piMultiplicative and AddEquiv.prodUnique between the multiplicative type tags, upgraded to ContinuousMulEquivs: the first two transport properties of topological groups, such as being pro-p, between the two shapes of a product, and the last collapses a product decomposition of a topological group whose second factor turns out to be trivial. The universe lift ULift M of a topological monoid is topologically isomorphic to M, which is MulEquiv.ulift upgraded to a ContinuousMulEquiv; it lets a universal property whose target must live in a fixed universe be applied to a group in a smaller one.

Main definitions

• TauCeti.ContinuousMulEquiv.prodMultiplicative: the topological isomorphism Multiplicative (M × N) ≃ₜ* Multiplicative M × Multiplicative N, with its evaluation lemmas prodMultiplicative_apply and prodMultiplicative_symm_apply.
• TauCeti.ContinuousMulEquiv.piMultiplicative: the topological isomorphism Multiplicative (∀ i, K i) ≃ₜ* ∀ i, Multiplicative (K i), with its evaluation lemmas piMultiplicative_apply and piMultiplicative_symm_apply.
• TauCeti.ContinuousMulEquiv.multiplicativeProdUnique: the topological isomorphism Multiplicative (M × T) ≃ₜ* Multiplicative M for [Unique T], with its evaluation lemmas multiplicativeProdUnique_apply and multiplicativeProdUnique_symm_apply.
• ContinuousAddEquiv.toMultiplicative: a topological isomorphism M ≃ₜ+ N of additive groups as a topological isomorphism Multiplicative M ≃ₜ* Multiplicative N, with its evaluation lemmas toMultiplicative_apply and toMultiplicative_symm_apply.
• TauCeti.ContinuousMulEquiv.ulift: the topological isomorphism ULift M ≃ₜ* M, with its evaluation lemmas ulift_apply and ulift_symm_apply.

def TauCeti.ContinuousMulEquiv.prodMultiplicative (M : Type u_1) (N : Type u_2) [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] : Multiplicative (M × N) ≃ₜ* Multiplicative M × Multiplicative N

The multiplicative type tag of a product is the product of the multiplicative type tags, as a topological isomorphism. This is MulEquiv.prodMultiplicative as a ContinuousMulEquiv.

Equations

• TauCeti.ContinuousMulEquiv.prodMultiplicative M N = { toMulEquiv := MulEquiv.prodMultiplicative M N, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMulEquiv.prodMultiplicative_apply (M : Type u_1) (N : Type u_2) [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] (x : Multiplicative (M × N)) : (prodMultiplicative M N) x = (Multiplicative.ofAdd (Multiplicative.toAdd x).1, Multiplicative.ofAdd (Multiplicative.toAdd x).2)

@[simp]

theorem TauCeti.ContinuousMulEquiv.prodMultiplicative_symm_apply (M : Type u_1) (N : Type u_2) [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] (x : Multiplicative M × Multiplicative N) : (prodMultiplicative M N).symm x = Multiplicative.ofAdd (Multiplicative.toAdd x.1, Multiplicative.toAdd x.2)

def TauCeti.ContinuousMulEquiv.piMultiplicative {ι : Type u_1} (K : ι → Type u_2) [(i : ι) → Add (K i)] [(i : ι) → TopologicalSpace (K i)] : Multiplicative ((i : ι) → K i) ≃ₜ* ((i : ι) → Multiplicative (K i))

The multiplicative type tag of a dependent product is the product of the multiplicative type tags, as a topological isomorphism. This is MulEquiv.piMultiplicative as a ContinuousMulEquiv.

Equations

• TauCeti.ContinuousMulEquiv.piMultiplicative K = { toMulEquiv := MulEquiv.piMultiplicative K, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMulEquiv.piMultiplicative_apply {ι : Type u_1} (K : ι → Type u_2) [(i : ι) → Add (K i)] [(i : ι) → TopologicalSpace (K i)] (x : Multiplicative ((i : ι) → K i)) (i : ι) : (piMultiplicative K) x i = Multiplicative.ofAdd (Multiplicative.toAdd x i)

@[simp]

theorem TauCeti.ContinuousMulEquiv.piMultiplicative_symm_apply {ι : Type u_1} (K : ι → Type u_2) [(i : ι) → Add (K i)] [(i : ι) → TopologicalSpace (K i)] (x : (i : ι) → Multiplicative (K i)) : (piMultiplicative K).symm x = Multiplicative.ofAdd fun (i : ι) => Multiplicative.toAdd (x i)

def TauCeti.ContinuousMulEquiv.multiplicativeProdUnique (M : Type u_1) (T : Type u_2) [AddZeroClass M] [AddZeroClass T] [TopologicalSpace M] [TopologicalSpace T] [Unique T] : Multiplicative (M × T) ≃ₜ* Multiplicative M

Dropping a trivial factor: when T has a unique element, Multiplicative (M × T) is topologically isomorphic to Multiplicative M. This is AddEquiv.prodUnique as a ContinuousMulEquiv between the multiplicative type tags.

Equations

• TauCeti.ContinuousMulEquiv.multiplicativeProdUnique M T = { toMulEquiv := AddEquiv.toMultiplicative AddEquiv.prodUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMulEquiv.multiplicativeProdUnique_apply {M : Type u_1} {T : Type u_2} [AddZeroClass M] [AddZeroClass T] [TopologicalSpace M] [TopologicalSpace T] [Unique T] (x : Multiplicative (M × T)) : (multiplicativeProdUnique M T) x = Multiplicative.ofAdd (Multiplicative.toAdd x).1

@[simp]

theorem TauCeti.ContinuousMulEquiv.multiplicativeProdUnique_symm_apply {M : Type u_1} {T : Type u_2} [AddZeroClass M] [AddZeroClass T] [TopologicalSpace M] [TopologicalSpace T] [Unique T] (v : Multiplicative M) : (multiplicativeProdUnique M T).symm v = Multiplicative.ofAdd (Multiplicative.toAdd v, default)

def ContinuousAddEquiv.toMultiplicative {M : Type u_1} {N : Type u_2} [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] (e : M ≃ₜ+ N) : Multiplicative M ≃ₜ* Multiplicative N

A topological isomorphism M ≃ₜ+ N of additive topological groups, as a topological isomorphism Multiplicative M ≃ₜ* Multiplicative N of the multiplicative type tags. This is AddEquiv.toMultiplicative as a ContinuousMulEquiv.

Equations

• e.toMultiplicative = { toMulEquiv := AddEquiv.toMultiplicative e.toAddEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAddEquiv.toMultiplicative_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] (e : M ≃ₜ+ N) (x : Multiplicative M) : e.toMultiplicative x = Multiplicative.ofAdd (e (Multiplicative.toAdd x))

@[simp]

theorem ContinuousAddEquiv.toMultiplicative_symm_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] (e : M ≃ₜ+ N) (y : Multiplicative N) : e.toMultiplicative.symm y = Multiplicative.ofAdd (e.symm (Multiplicative.toAdd y))

def TauCeti.ContinuousMulEquiv.ulift {M : Type u} [Mul M] [TopologicalSpace M] : ULift.{v, u} M ≃ₜ* M

The universe lift of a topological monoid is topologically isomorphic to it. This is MulEquiv.ulift as a ContinuousMulEquiv.

Equations

• TauCeti.ContinuousMulEquiv.ulift = { toMulEquiv := MulEquiv.ulift, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.ContinuousMulEquiv.ulift_apply {M : Type u} [Mul M] [TopologicalSpace M] (x : ULift.{v, u} M) : ulift x = x.down

@[simp]

theorem TauCeti.ContinuousMulEquiv.ulift_symm_apply {M : Type u} [Mul M] [TopologicalSpace M] (x : M) : ulift.symm x = { down := x }