Continuous Monoid Hom

Material destined for Mathlib.

def ContinuousAddEquiv.toIntContinuousLinearEquiv {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) : M ≃L[ℤ] M₂

Reinterpret a continuous additive equivalence between additive groups as a continuous ℤ-linear equivalence.

Equations

• e.toIntContinuousLinearEquiv = { toLinearEquiv := e.toIntLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAddEquiv.toIntContinuousLinearEquiv_apply {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) (a✝ : M) : e.toIntContinuousLinearEquiv a✝ = ↑e a✝

@[simp]

theorem ContinuousAddEquiv.toIntContinuousLinearEquiv_symm_apply {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) (a✝ : M₂) : e.toIntContinuousLinearEquiv.symm a✝ = (↑e).symm a✝

def ContinuousAddEquiv.quotientPi {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddCommGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] : ((i : ι) → G i) ⧸ AddSubgroup.pi Set.univ p ≃ₜ+ ((i : ι) → G i ⧸ p i)

For a finite family of topological additive groups G i and subgroups p i ≤ G i, the canonical continuous additive isomorphism (∏ i, G i) ⧸ (∏ i, p i) ≃ₜ+ ∏ i, (G i ⧸ p i).

Equations

• ContinuousAddEquiv.quotientPi p = (Submodule.quotientPiContinuousLinearEquiv fun (i : ι) => AddSubgroup.toIntSubmodule (p i)).toContinuousAddEquiv

def ContinuousMulEquiv.piUnique {ι : Type u_1} (M : ι → Type u_2) [(j : ι) → Mul (M j)] [(j : ι) → TopologicalSpace (M j)] [Unique ι] : ((j : ι) → M j) ≃ₜ* M default

A family indexed by a type with a unique element is ContinuousMulEquiv to the element at the single index.

Equations

• ContinuousMulEquiv.piUnique M = { toMulEquiv := MulEquiv.piUnique M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piUnique {ι : Type u_1} (M : ι → Type u_2) [(j : ι) → Add (M j)] [(j : ι) → TopologicalSpace (M j)] [Unique ι] : ((j : ι) → M j) ≃ₜ+ M default

A family indexed by a type with a unique element is ContinuousAddEquiv to the element at the single index.

Equations

• ContinuousAddEquiv.piUnique M = { toAddEquiv := AddEquiv.piUnique M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousMulEquiv.piEquivPiSubtypeProd {ι : Type u_1} (p : ι → Prop) (Y : ι → Type u_2) [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Mul (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ* ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

Splits the indices of ∀ (i : ι), Y i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a ContinuousMulEquiv.

Equations

• ContinuousMulEquiv.piEquivPiSubtypeProd p Y = { toEquiv := (Homeomorph.piEquivPiSubtypeProd p Y).toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piEquivPiSubtypeProd {ι : Type u_1} (p : ι → Prop) (Y : ι → Type u_2) [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Add (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ+ ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

Splits the indices of ∀ (i : ι), Y i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a ContinuousAddEquiv.

Equations

• ContinuousAddEquiv.piEquivPiSubtypeProd p Y = { toEquiv := (Homeomorph.piEquivPiSubtypeProd p Y).toEquiv, map_add' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousMulEquiv.mapUnits {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) : Mˣ ≃ₜ* Nˣ

Any ContinuousMulEquiv induces a ContinuousMulEquiv on units.

Equations

• f.mapUnits = { toMulEquiv := Units.mapEquiv ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.val_mapUnits_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) (a✝ : Mˣ) : ↑(f.mapUnits a✝) = ↑f ↑a✝

@[simp]

theorem ContinuousMulEquiv.val_inv_mapUnits_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) (a : Nˣ) : ↑(f.mapUnits.symm a)⁻¹ = (↑f).symm ↑a⁻¹

@[simp]

theorem ContinuousMulEquiv.val_mapUnits_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) (a : Nˣ) : ↑(f.mapUnits.symm a) = (↑f).symm ↑a

@[simp]

theorem ContinuousMulEquiv.val_inv_mapUnits_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Monoid M] [Monoid N] (f : M ≃ₜ* N) (a✝ : Mˣ) : ↑(f.mapUnits a✝)⁻¹ = ↑f ↑a✝⁻¹

theorem ContinuousMulEquiv.coe_toHomeomorph {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [CommMonoid M] [CommMonoid N] (f : M ≃ₜ* N) : ⇑f.toHomeomorph = ⇑f

theorem ContinuousAddEquiv.coe_toHomeomorph {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [AddCommMonoid M] [AddCommMonoid N] (f : M ≃ₜ+ N) : ⇑f.toHomeomorph = ⇑f