Mathlib.Topology.Algebra.ContinuousMonoidHom

ContinuousAddMonoidHom structure

(A B : Type*) [AddMonoid A] [AddMonoid B] [TopologicalSpace A]
  [TopologicalSpace B] extends A →+ B, C(A, B)

Full source

/-- The type of continuous additive monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousAddMonoidHom A B)`,
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F)`.

When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `AddMonoidHomClass`, if needed. -/
structure ContinuousAddMonoidHom (A B : Type*) [AddMonoid A] [AddMonoid B] [TopologicalSpace A]
  [TopologicalSpace B] extends A →+ B, C(A, B)

Continuous additive monoid homomorphism

Informal description

The structure representing continuous additive monoid homomorphisms from a topological additive monoid $ A $ to another topological additive monoid $ B $. It consists of an additive monoid homomorphism $ A \to B $ that is also continuous.

ContinuousMonoidHom structure

extends A →* B, C(A, B)

Full source

/-- The type of continuous monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousMonoidHom A B)`,
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F)`.

When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `MonoidHomClass`, if needed. -/
@[to_additive "The type of continuous additive monoid homomorphisms from `A` to `B`."]
structure ContinuousMonoidHom extends A →* B, C(A, B)

Continuous monoid homomorphism

Informal description

The structure representing continuous monoid homomorphisms from a topological monoid $ A $ to another topological monoid $ B $. It consists of a monoid homomorphism $ A \to B $ that is also continuous.

ContinuousMonoidHom.term_→ₜ+_ definition

: Lean.TrailingParserDescr✝

Full source

/-- The type of continuous monoid homomorphisms from `A` to `B`.-/
infixr:25 " →ₜ+ " => ContinuousAddMonoidHom

Continuous additive monoid homomorphism notation

Informal description

The notation `A →ₜ+ B` denotes the type of continuous additive monoid homomorphisms from a topological additive monoid `A` to another topological additive monoid `B`. These are additive monoid homomorphisms that are also continuous maps between the underlying topological spaces.

ContinuousMonoidHom.term_→ₜ*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- The type of continuous monoid homomorphisms from `A` to `B`.-/
infixr:25 " →ₜ* " => ContinuousMonoidHom

Continuous monoid homomorphism notation

Informal description

The notation `A →ₜ* B` denotes the type of continuous monoid homomorphisms from a topological monoid `A` to a topological monoid `B`.

ContinuousMonoidHom.instFunLike instance

: FunLike (A →ₜ* B) A B

Full source

@[to_additive]
instance instFunLike : FunLike (A →ₜ* B) A B where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := g
    congr

Function-Like Structure of Continuous Monoid Homomorphisms

Informal description

For topological monoids $A$ and $B$, the type of continuous monoid homomorphisms $A \to_{t*} B$ can be treated as a function-like type, where each homomorphism can be coerced to a function from $A$ to $B$ in an injective way.

ContinuousMonoidHom.instMonoidHomClass instance

: MonoidHomClass (A →ₜ* B) A B

Full source

@[to_additive]
instance instMonoidHomClass : MonoidHomClass (A →ₜ* B) A B where
  map_mul f := f.map_mul'
  map_one f := f.map_one'

Continuous Monoid Homomorphisms as Monoid Homomorphism Class

Informal description

For topological monoids $A$ and $B$, the type of continuous monoid homomorphisms $A \to_{t*} B$ forms a `MonoidHomClass`, meaning it inherits all the properties of monoid homomorphisms (preserving multiplication and identity) while also maintaining continuity.

ContinuousMonoidHom.instContinuousMapClass instance

: ContinuousMapClass (A →ₜ* B) A B

Full source

@[to_additive]
instance instContinuousMapClass : ContinuousMapClass (A →ₜ* B) A B where
  map_continuous f := f.continuous_toFun

Continuous Monoid Homomorphisms as Continuous Map Class

Informal description

For topological monoids $A$ and $B$, the type of continuous monoid homomorphisms $A \to_{t*} B$ forms a `ContinuousMapClass`, meaning it inherits all the properties of continuous maps (preserving continuity) while also maintaining the structure of monoid homomorphisms.

ContinuousMonoidHom.coe_toMonoidHom theorem

(f : A →ₜ* B) : f.toMonoidHom = f

Full source

@[to_additive (attr := simp)]
lemma coe_toMonoidHom (f : A →ₜ* B) : f.toMonoidHom = f := rfl

Underlying Monoid Homomorphism of Continuous Monoid Homomorphism

Informal description

For any continuous monoid homomorphism $f \colon A \to_{t*} B$, the underlying monoid homomorphism $f.toMonoidHom$ is equal to $f$ itself.

ContinuousMonoidHom.coe_toContinuousMap theorem

(f : A →ₜ* B) : f.toContinuousMap = f

Full source

@[to_additive (attr := simp)]
lemma coe_toContinuousMap (f : A →ₜ* B) : f.toContinuousMap = f := rfl

Underlying Continuous Map of Continuous Monoid Homomorphism

Informal description

For any continuous monoid homomorphism $f \colon A \to_{t*} B$, the underlying continuous map $f.toContinuousMap$ is equal to $f$ itself.

ContinuousMonoidHom.toContinuousMonoidHom definition

[MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : A →ₜ* B

Full source

/-- Turn an element of a type `F` satisfying `MonoidHomClass F A B` and `ContinuousMapClass F A B`
into a`ContinuousMonoidHom`. This is declared as the default coercion from `F` to
`(A →ₜ* B)`. -/
@[to_additive (attr := coe) "Turn an element of a type `F` satisfying
`AddMonoidHomClass F A B` and `ContinuousMapClass F A B` into a`ContinuousAddMonoidHom`.
This is declared as the default coercion from `F` to `ContinuousAddMonoidHom A B`."]
def toContinuousMonoidHom [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : A →ₜ* B :=
  { MonoidHomClass.toMonoidHom f with }

Conversion to continuous monoid homomorphism

Informal description

Given a type `F` satisfying both `MonoidHomClass F A B` (meaning elements of `F` are monoid homomorphisms from `A` to `B`) and `ContinuousMapClass F A B` (meaning elements of `F` are continuous maps from `A` to `B`), this definition converts an element `f : F` into a `ContinuousMonoidHom A B`. The resulting continuous monoid homomorphism has the same underlying function as `f` and inherits both the homomorphism properties and continuity from `f`.

ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass instance

[MonoidHomClass F A B] [ContinuousMapClass F A B] : CoeOut F (A →ₜ* B)

Full source

/-- Any type satisfying `MonoidHomClass` and `ContinuousMapClass` can be cast into
`ContinuousMonoidHom` via `ContinuousMonoidHom.toContinuousMonoidHom`. -/
@[to_additive "Any type satisfying `AddMonoidHomClass` and `ContinuousMapClass` can be cast into
`ContinuousAddMonoidHom` via `ContinuousAddMonoidHom.toContinuousAddMonoidHom`."]
instance [MonoidHomClass F A B] [ContinuousMapClass F A B] : CoeOut F (A →ₜ* B) :=
  ⟨ContinuousMonoidHom.toContinuousMonoidHom⟩

Canonical View of Monoid Homomorphism Classes as Continuous Monoid Homomorphisms

Informal description

For any type $F$ that satisfies both `MonoidHomClass F A B` (meaning elements of $F$ are monoid homomorphisms from $A$ to $B$) and `ContinuousMapClass F A B` (meaning elements of $F$ are continuous maps from $A$ to $B$), there is a canonical way to view elements of $F$ as continuous monoid homomorphisms from $A$ to $B$.

ContinuousMonoidHom.coe_coe theorem

[MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ⇑(f : A →ₜ* B) = f

Full source

@[to_additive (attr := simp)]
lemma coe_coe [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
    ⇑(f : A →ₜ* B) = f := rfl

Coercion of Continuous Monoid Homomorphism Preserves Underlying Function

Informal description

For any type $F$ that satisfies both `MonoidHomClass F A B` (meaning elements of $F$ are monoid homomorphisms from $A$ to $B$) and `ContinuousMapClass F A B` (meaning elements of $F$ are continuous maps from $A$ to $B$), the underlying function of the continuous monoid homomorphism obtained by coercing $f : F$ to $A \to_{t*} B$ is equal to $f$ itself. In other words, $\text{toFun}(f : A \to_{t*} B) = f$.

ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom theorem

[MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ((f : A →ₜ* B) : A →* B) = f

Full source

@[to_additive (attr := simp, norm_cast)]
lemma toMonoidHom_toContinuousMonoidHom [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
    ((f : A →ₜ* B) : A →* B) = f := rfl

Coercion of Continuous Monoid Homomorphism to Monoid Homomorphism Preserves Identity

Informal description

For any type $F$ that is both a `MonoidHomClass` from $A$ to $B$ and a `ContinuousMapClass` from $A$ to $B$, and for any element $f \in F$, the monoid homomorphism obtained by coercing the continuous monoid homomorphism $f : A \to_{t*} B$ to a monoid homomorphism $A \to* B$ is equal to $f$ itself. In other words, $(f : A \to_{t*} B) = f$ as monoid homomorphisms.

ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom theorem

[MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ((f : A →ₜ* B) : C(A, B)) = f

Full source

@[to_additive (attr := simp, norm_cast)]
lemma toContinuousMap_toContinuousMonoidHom [MonoidHomClass F A B] [ContinuousMapClass F A B]
    (f : F) : ((f : A →ₜ* B) : C(A, B)) = f := rfl

Coercion of Continuous Monoid Homomorphism to Continuous Map Preserves Identity

Informal description

For any type $F$ that is both a `MonoidHomClass` from $A$ to $B$ and a `ContinuousMapClass` from $A$ to $B$, and for any element $f \in F$, the continuous map obtained by coercing the continuous monoid homomorphism $f : A \to_{t*} B$ to a continuous map $C(A, B)$ is equal to $f$ itself. In other words, $(f : A \to_{t*} B) = f$ as continuous maps.

ContinuousMonoidHom.ext theorem

{f g : A →ₜ* B} (h : ∀ x, f x = g x) : f = g

Full source

@[to_additive (attr := ext)]
theorem ext {f g : A →ₜ* B} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Continuous Monoid Homomorphisms

Informal description

For any two continuous monoid homomorphisms $f, g \colon A \to B$ between topological monoids, if $f(x) = g(x)$ for all $x \in A$, then $f = g$.

ContinuousMonoidHom.toContinuousMap_injective theorem

: Injective (toContinuousMap : _ → C(A, B))

Full source

@[to_additive]
theorem toContinuousMap_injective : Injective (toContinuousMap : _ → C(A, B)) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h

Injectivity of Continuous Monoid Homomorphism to Continuous Map

Informal description

The map from continuous monoid homomorphisms $A \to_{t*} B$ to continuous maps $C(A, B)$, given by forgetting the monoid homomorphism structure, is injective. In other words, if two continuous monoid homomorphisms induce the same continuous map, then they are equal.

ContinuousMonoidHom.comp definition

(g : B →ₜ* C) (f : A →ₜ* B) : A →ₜ* C

Full source

/-- Composition of two continuous homomorphisms. -/
@[to_additive (attr := simps!) "Composition of two continuous homomorphisms."]
def comp (g : B →ₜ* C) (f : A →ₜ* B) : A →ₜ* C :=
  ⟨g.toMonoidHom.comp f.toMonoidHom, (map_continuous g).comp (map_continuous f)⟩

Composition of continuous monoid homomorphisms

Informal description

Given continuous monoid homomorphisms $ g \colon B \to C $ and $ f \colon A \to B $, the composition $ g \circ f $ is a continuous monoid homomorphism from $ A $ to $ C $.

ContinuousMonoidHom.coe_comp theorem

(g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ⇑(g.comp f) = ⇑g ∘ ⇑f

Full source

@[to_additive (attr := simp)]
lemma coe_comp (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) :
    ⇑(g.comp f) = ⇑g ∘ ⇑f := rfl

Composition of Continuous Monoid Homomorphisms Preserves Underlying Functions

Informal description

For any continuous monoid homomorphisms $g \colon B \to C$ and $f \colon A \to B$, the underlying function of their composition $g \circ f$ is equal to the composition of their underlying functions, i.e., $(g \circ f)(a) = g(f(a))$ for all $a \in A$.

ContinuousMonoidHom.prod definition

(f : A →ₜ* B) (g : A →ₜ* C) : A →ₜ* (B × C)

Full source

/-- Product of two continuous homomorphisms on the same space. -/
@[to_additive (attr := simps!) prod "Product of two continuous homomorphisms on the same space."]
def prod (f : A →ₜ* B) (g : A →ₜ* C) : A →ₜ* (B × C) :=
  ⟨f.toMonoidHom.prod g.toMonoidHom, f.continuous_toFun.prodMk g.continuous_toFun⟩

Product of continuous monoid homomorphisms

Informal description

Given continuous monoid homomorphisms $ f \colon A \to B $ and $ g \colon A \to C $, the function `ContinuousMonoidHom.prod` constructs the continuous monoid homomorphism $ A \to B \times C $ defined by $ a \mapsto (f(a), g(a)) $.

ContinuousMonoidHom.prodMap definition

(f : A →ₜ* C) (g : B →ₜ* D) : (A × B) →ₜ* (C × D)

Full source

/-- Product of two continuous homomorphisms on different spaces. -/
@[to_additive (attr := simps!) prodMap
  "Product of two continuous homomorphisms on different spaces."]
def prodMap (f : A →ₜ* C) (g : B →ₜ* D) :
    (A × B) →ₜ* (C × D) :=
  ⟨f.toMonoidHom.prodMap g.toMonoidHom, f.continuous_toFun.prodMap g.continuous_toFun⟩

Product map of continuous monoid homomorphisms

Informal description

Given continuous monoid homomorphisms $ f \colon A \to C $ and $ g \colon B \to D $, the function `ContinuousMonoidHom.prodMap` constructs the continuous monoid homomorphism $ A \times B \to C \times D $ defined by $(a, b) \mapsto (f(a), g(b))$.

ContinuousMonoidHom.instOne instance

: One (A →ₜ* B)

Full source

/-- The trivial continuous homomorphism. -/
@[to_additive (attr := simps!) "The trivial continuous homomorphism."]
instance : One (A →ₜ* B) where
  one := ⟨1, continuous_const⟩

Trivial Continuous Monoid Homomorphism

Informal description

The space of continuous monoid homomorphisms from a topological monoid $A$ to another topological monoid $B$ has a trivial homomorphism, which maps every element of $A$ to the identity element of $B$.

ContinuousMonoidHom.coe_one theorem

: ⇑(1 : A →ₜ* B) = 1

Full source

@[to_additive (attr := simp)]
lemma coe_one : ⇑(1 : A →ₜ* B) = 1 :=
  rfl

Trivial Continuous Homomorphism Coincides with Constant One Function

Informal description

The trivial continuous monoid homomorphism $1 \colon A \to_{t*} B$ (which maps every element to the identity) coincides with the constant function $1$ when viewed as a function from $A$ to $B$.

ContinuousMonoidHom.instInhabited instance

: Inhabited (A →ₜ* B)

Full source

@[to_additive]
instance : Inhabited (A →ₜ* B) := ⟨1⟩

Inhabited Space of Continuous Monoid Homomorphisms

Informal description

The space of continuous monoid homomorphisms from a topological monoid $A$ to another topological monoid $B$ is inhabited.

ContinuousMonoidHom.id definition

: A →ₜ* A

Full source

/-- The identity continuous homomorphism. -/
@[to_additive (attr := simps!) "The identity continuous homomorphism."]
def id : A →ₜ* A := ⟨.id A, continuous_id⟩

Identity continuous monoid homomorphism

Informal description

The identity continuous monoid homomorphism from a topological monoid $ A $ to itself, which is the identity map on $ A $ equipped with the continuous structure.

ContinuousMonoidHom.coe_id theorem

: ⇑(ContinuousMonoidHom.id A) = _root_.id

Full source

@[to_additive (attr := simp)]
lemma coe_id : ⇑(ContinuousMonoidHom.id A) = _root_.id :=
  rfl

Identity Continuous Monoid Homomorphism as Identity Function

Informal description

The underlying function of the identity continuous monoid homomorphism from a topological monoid $A$ to itself is equal to the identity function on $A$.

ContinuousMonoidHom.fst definition

: (A × B) →ₜ* A

Full source

/-- The continuous homomorphism given by projection onto the first factor. -/
@[to_additive (attr := simps!)
  "The continuous homomorphism given by projection onto the first factor."]
def fst : (A × B) →ₜ* A := ⟨MonoidHom.fst A B, continuous_fst⟩

Projection onto first factor as a continuous monoid homomorphism

Informal description

The continuous homomorphism from the product topological monoid $ A \times B $ to $ A $ given by projection onto the first factor.

ContinuousMonoidHom.snd definition

: (A × B) →ₜ* B

Full source

/-- The continuous homomorphism given by projection onto the second factor. -/
@[to_additive (attr := simps!)
  "The continuous homomorphism given by projection onto the second factor."]
def snd : (A × B) →ₜ* B :=
  ⟨MonoidHom.snd A B, continuous_snd⟩

Projection onto second factor as a continuous monoid homomorphism

Informal description

The continuous homomorphism from the product topological monoid $ A \times B $ to $ B $ given by projection onto the second factor.

ContinuousMonoidHom.inl definition

: A →ₜ* (A × B)

Full source

/-- The continuous homomorphism given by inclusion of the first factor. -/
@[to_additive (attr := simps!)
  "The continuous homomorphism given by inclusion of the first factor."]
def inl : A →ₜ* (A × B) :=
  prod (id A) 1

Inclusion into first factor as a continuous monoid homomorphism

Informal description

The continuous monoid homomorphism from a topological monoid $ A $ to the product topological monoid $ A \times B $ that maps each element $ a \in A $ to $ (a, 1) $, where $ 1 $ is the identity element of $ B $.

ContinuousMonoidHom.inr definition

: B →ₜ* (A × B)

Full source

/-- The continuous homomorphism given by inclusion of the second factor. -/
@[to_additive (attr := simps!)
  "The continuous homomorphism given by inclusion of the second factor."]
def inr : B →ₜ* (A × B) :=
  prod 1 (id B)

Inclusion into second factor as a continuous monoid homomorphism

Informal description

The continuous monoid homomorphism from a topological monoid $ B $ to the product topological monoid $ A \times B $ that maps each element $ b \in B $ to $ (1, b) $, where $ 1 $ is the identity element of $ A $.

ContinuousMonoidHom.diag definition

: A →ₜ* (A × A)

Full source

/-- The continuous homomorphism given by the diagonal embedding. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by the diagonal embedding."]
def diag : A →ₜ* (A × A) := prod (id A) (id A)

Diagonal continuous monoid homomorphism

Informal description

The continuous monoid homomorphism that maps an element $ a $ of a topological monoid $ A $ to the pair $ (a, a) $ in the product topological monoid $ A \times A $. This is constructed as the product of the identity continuous monoid homomorphism on $ A $ with itself.

ContinuousMonoidHom.swap definition

: (A × B) →ₜ* (B × A)

Full source

/-- The continuous homomorphism given by swapping components. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by swapping components."]
def swap : (A × B) →ₜ* (B × A) := prod (snd A B) (fst A B)

Component-swapping continuous monoid homomorphism

Informal description

The continuous monoid homomorphism that swaps the components of a pair in the product topological monoid $ A \times B $, mapping $ (a, b) $ to $ (b, a) $.

ContinuousMonoidHom.mul definition

: (E × E) →ₜ* E

Full source

/-- The continuous homomorphism given by multiplication. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by addition."]
def mul : (E × E) →ₜ* E := ⟨mulMonoidHom, continuous_mul⟩

Continuous multiplication homomorphism

Informal description

The continuous monoid homomorphism given by the multiplication operation, mapping a pair of elements $(x, y)$ in the topological monoid $E \times E$ to their product $x \cdot y$ in $E$. This homomorphism is continuous with respect to the product topology on $E \times E$ and the topology on $E$.

ContinuousMonoidHom.instCommMonoid instance

: CommMonoid (A →ₜ* E)

Full source

@[to_additive]
instance : CommMonoid (A →ₜ* E) where
  mul f g := (mul E).comp (f.prod g)
  mul_comm f g := ext fun x => mul_comm (f x) (g x)
  mul_assoc f g h := ext fun x => mul_assoc (f x) (g x) (h x)
  one_mul f := ext fun x => one_mul (f x)
  mul_one f := ext fun x => mul_one (f x)

Commutative Monoid Structure on Continuous Monoid Homomorphisms

Informal description

For any topological monoids $A$ and $E$, the space of continuous monoid homomorphisms from $A$ to $E$ forms a commutative monoid under pointwise multiplication.

ContinuousMonoidHom.coprod definition

(f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) : ContinuousMonoidHom (A × B) E

Full source

/-- Coproduct of two continuous homomorphisms to the same space. -/
@[to_additive (attr := simps!) "Coproduct of two continuous homomorphisms to the same space."]
def coprod (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) :
    ContinuousMonoidHom (A × B) E :=
  (mul E).comp (f.prodMap g)

Coproduct of continuous monoid homomorphisms

Informal description

Given continuous monoid homomorphisms $ f \colon A \to E $ and $ g \colon B \to E $, the coproduct $ f \coprod g $ is the continuous monoid homomorphism $ A \times B \to E $ defined by $(a, b) \mapsto f(a) \cdot g(b)$, where the multiplication is taken in $ E $.

ContinuousMonoidHom.inv definition

: ContinuousMonoidHom E E

Full source

/-- The continuous homomorphism given by inversion. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by negation."]
def inv : ContinuousMonoidHom E E :=
  ⟨invMonoidHom, continuous_inv⟩

Inversion as a continuous monoid homomorphism

Informal description

The continuous homomorphism from a topological group $ E $ to itself given by the inversion map $ x \mapsto x^{-1} $.

ContinuousMonoidHom.instCommGroup instance

: CommGroup (ContinuousMonoidHom A E)

Full source

@[to_additive]
instance : CommGroup (ContinuousMonoidHom A E) where
  __ : CommMonoid (ContinuousMonoidHom A E) := inferInstance
  inv f := (inv E).comp f
  inv_mul_cancel f := ext fun x => inv_mul_cancel (f x)
  div f g := .comp ⟨divMonoidHom, continuous_div'⟩ (f.prod g)
  div_eq_mul_inv f g := ext fun x => div_eq_mul_inv (f x) (g x)

Commutative Group Structure on Continuous Monoid Homomorphisms

Informal description

For any topological monoid $A$ and topological commutative group $E$, the space of continuous monoid homomorphisms from $A$ to $E$ forms a commutative group under pointwise multiplication.

ContinuousMonoidHom.ofClass definition

(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F) : (ContinuousMonoidHom A B)

Full source

/-- For `f : F` where `F` is a class of continuous monoid hom, this yields an element
`ContinuousMonoidHom A B`. -/
@[to_additive "For `f : F` where `F` is a class of continuous additive monoid hom, this yields
an element `ContinuousAddMonoidHom A B`."]
def ofClass (F : Type*) [FunLike F A B] [ContinuousMapClass F A B]
    [MonoidHomClass F A B] (f : F) : (ContinuousMonoidHom A B) := toContinuousMonoidHom f

Conversion to continuous monoid homomorphism

Informal description

Given a type `F` that is a class of continuous monoid homomorphisms from `A` to `B` (i.e., elements of `F` are both monoid homomorphisms and continuous maps), this definition converts an element `f : F` into a bundled continuous monoid homomorphism `A →ₜ* B`.

ContinuousAddEquiv structure

[Add G] [Add H] extends G ≃+ H , G ≃ₜ H

Full source

/-- The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous. -/
structure ContinuousAddEquiv [Add G] [Add H] extends G ≃+ H , G ≃ₜ H

Continuous additive group isomorphism

Informal description

The structure representing continuous additive isomorphisms between two topological additive groups. It consists of a bijective additive homomorphism $ f \colon G \to H $ between the groups $ G $ and $ H $, where both $ f $ and its inverse $ f^{-1} $ are continuous.

ContinuousMulEquiv structure

[Mul G] [Mul H] extends G ≃* H , G ≃ₜ H

Full source

/-- The structure of two-sided continuous isomorphisms between groups.
Note that both the map and its inverse have to be continuous. -/
@[to_additive "The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous."]
structure ContinuousMulEquiv [Mul G] [Mul H] extends G ≃* H , G ≃ₜ H

Continuous multiplicative isomorphism

Informal description

The structure representing continuous multiplicative isomorphisms between two topological groups $G$ and $H$ with multiplication operations. It consists of a bijective multiplicative homomorphism $G \to H$ (i.e., a group isomorphism) that is continuous, and whose inverse is also continuous.

term_≃ₜ*_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " ≃ₜ* " => ContinuousMulEquiv

Continuous multiplicative equivalence

Informal description

The notation `≃ₜ*` represents a continuous multiplicative equivalence between two topological groups. Specifically, for topological groups `G` and `H` with multiplicative structures, `G ≃ₜ* H` denotes a bijective map that is both a group isomorphism and a homeomorphism (i.e., it preserves the group operation and is continuous with a continuous inverse).

term_≃ₜ+_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " ≃ₜ+ " => ContinuousAddEquiv

Continuous additive equivalence

Informal description

The notation `A ≃ₜ+ B` represents the type of continuous additive equivalences between two topological additive groups `A` and `B`, i.e., continuous additive homomorphisms that are bijective with continuous inverses.

ContinuousMulEquiv.instEquivLike instance

: EquivLike (M ≃ₜ* N) M N

Full source

@[to_additive]
instance : EquivLike (M ≃ₜ* N) M N where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by
    cases f
    cases g
    congr
    exact MulEquiv.ext_iff.mpr (congrFun h₁)

Equivalence-like Structure for Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphisms $M \simeq^* N$ between topological groups $M$ and $N$, there is an equivalence-like structure that allows terms of this type to be treated as bijections between $M$ and $N$.

ContinuousMulEquiv.instMulEquivClass instance

: MulEquivClass (M ≃ₜ* N) M N

Full source

@[to_additive]
instance : MulEquivClass (M ≃ₜ* N) M N where
  map_mul f := f.map_mul'

Continuous Multiplicative Isomorphisms as Group Isomorphisms

Informal description

For any topological groups $M$ and $N$ with multiplication operations, the continuous multiplicative isomorphisms $M \simeq^* N$ form a class of multiplicative group isomorphisms between $M$ and $N$.

ContinuousMulEquiv.instHomeomorphClass instance

: HomeomorphClass (M ≃ₜ* N) M N

Full source

@[to_additive]
instance : HomeomorphClass (M ≃ₜ* N) M N where
  map_continuous f := f.continuous_toFun
  inv_continuous f := f.continuous_invFun

Continuous Multiplicative Isomorphisms as Homeomorphisms

Informal description

For any topological groups $M$ and $N$ with multiplication operations, the continuous multiplicative isomorphisms $M \simeq^* N$ form a class of homeomorphisms between $M$ and $N$.

ContinuousMulEquiv.ext theorem

{f g : M ≃ₜ* N} (h : ∀ x, f x = g x) : f = g

Full source

/-- Two continuous multiplicative isomorphisms agree if they are defined by the
same underlying function. -/
@[to_additive (attr := ext)
  "Two continuous additive isomorphisms agree if they are defined by the same underlying function."]
theorem ext {f g : M ≃ₜ* N} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Continuous Multiplicative Isomorphisms

Informal description

Let $M$ and $N$ be topological groups, and let $f, g: M \simeq^* N$ be continuous multiplicative isomorphisms. If $f(x) = g(x)$ for all $x \in M$, then $f = g$.

ContinuousMulEquiv.coe_mk theorem

(f : M ≃* N) (hf1 hf2) : ⇑(mk f hf1 hf2) = f

Full source

@[to_additive (attr := simp)]
theorem coe_mk (f : M ≃* N) (hf1 hf2) : ⇑(mk f hf1 hf2) = f := rfl

Underlying Function of Continuous Multiplicative Isomorphism Construction Equals Original Isomorphism

Informal description

Let $M$ and $N$ be topological groups, and let $f : M \simeq^* N$ be a multiplicative isomorphism. If $f$ is continuous (condition $hf1$) and its inverse is continuous (condition $hf2$), then the underlying function of the constructed continuous multiplicative isomorphism $\text{mk}(f, hf1, hf2)$ equals $f$.

ContinuousMulEquiv.toEquiv_eq_coe theorem

(f : M ≃ₜ* N) : f.toEquiv = f

Full source

@[to_additive]
theorem toEquiv_eq_coe (f : M ≃ₜ* N) : f.toEquiv = f :=
  rfl

Equality of Underlying Equivalence and Continuous Multiplicative Isomorphism

Informal description

For any continuous multiplicative isomorphism $f : M \simeq^* N$ between topological groups $M$ and $N$, the underlying equivalence (bijection) of $f$ is equal to $f$ itself when viewed as a function.

ContinuousMulEquiv.toMulEquiv_eq_coe theorem

(f : M ≃ₜ* N) : f.toMulEquiv = f

Full source

@[to_additive (attr := simp)]
theorem toMulEquiv_eq_coe (f : M ≃ₜ* N) : f.toMulEquiv = f :=
  rfl

Underlying multiplicative isomorphism equals continuous multiplicative isomorphism

Informal description

For any continuous multiplicative isomorphism $f \colon M \simeq^* N$ between topological groups $M$ and $N$, the underlying multiplicative isomorphism $f.toMulEquiv$ is equal to $f$ when viewed as a function.

ContinuousMulEquiv.toHomeomorph_eq_coe theorem

(f : M ≃ₜ* N) : f.toHomeomorph = f

Full source

@[to_additive]
theorem toHomeomorph_eq_coe (f : M ≃ₜ* N) : f.toHomeomorph = f :=
  rfl

Underlying homeomorphism equals continuous multiplicative isomorphism

Informal description

For any continuous multiplicative isomorphism $f \colon M \simeq^* N$ between topological groups $M$ and $N$, the underlying homeomorphism $f.toHomeomorph$ is equal to $f$ when viewed as a function.

ContinuousMulEquiv.mk' definition

(f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃ₜ* N

Full source

/-- Makes a continuous multiplicative isomorphism from
a homeomorphism which preserves multiplication. -/
@[to_additive "Makes an continuous additive isomorphism from
a homeomorphism which preserves addition."]
def mk' (f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃ₜ* N :=
  ⟨⟨f.toEquiv,h⟩, f.continuous_toFun, f.continuous_invFun⟩

Continuous multiplicative isomorphism from a multiplication-preserving homeomorphism

Informal description

Given a homeomorphism $f \colon M \to N$ between topological groups that preserves multiplication (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), this constructs a continuous multiplicative isomorphism from $M$ to $N$.

ContinuousMulEquiv.coe_mk' theorem

(f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : ⇑(mk' f h) = f

Full source

@[simp]
lemma coe_mk' (f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y)  : ⇑(mk' f h) = f := rfl

Underlying Function of Continuous Multiplicative Isomorphism Construction Equals Original Homeomorphism

Informal description

Given a homeomorphism $f \colon M \to N$ between topological groups that preserves multiplication (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the underlying function of the continuous multiplicative isomorphism constructed via `mk'` is equal to $f$.

ContinuousMulEquiv.bijective theorem

(e : M ≃ₜ* N) : Function.Bijective e

Full source

@[to_additive]
protected theorem bijective (e : M ≃ₜ* N) : Function.Bijective e :=
  EquivLike.bijective e

Bijectivity of Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \to N$ between topological groups, the map $e$ is bijective, meaning it is both injective and surjective.

ContinuousMulEquiv.injective theorem

(e : M ≃ₜ* N) : Function.Injective e

Full source

@[to_additive]
protected theorem injective (e : M ≃ₜ* N) : Function.Injective e :=
  EquivLike.injective e

Injectivity of Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \to N$ between topological groups, the map $e$ is injective.

ContinuousMulEquiv.surjective theorem

(e : M ≃ₜ* N) : Function.Surjective e

Full source

@[to_additive]
protected theorem surjective (e : M ≃ₜ* N) : Function.Surjective e :=
  EquivLike.surjective e

Surjectivity of Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \to N$ between topological groups, the map $e$ is surjective.

ContinuousMulEquiv.apply_eq_iff_eq theorem

(e : M ≃ₜ* N) {x y : M} : e x = e y ↔ x = y

Full source

@[to_additive]
theorem apply_eq_iff_eq (e : M ≃ₜ* N) {x y : M} : e x = e y ↔ x = y :=
  e.injective.eq_iff

Continuous Multiplicative Isomorphism Preserves Equality

Informal description

For any continuous multiplicative isomorphism $e \colon M \to N$ between topological groups and any elements $x, y \in M$, we have $e(x) = e(y)$ if and only if $x = y$.

ContinuousMulEquiv.refl definition

: M ≃ₜ* M

Full source

/-- The identity map is a continuous multiplicative isomorphism. -/
@[to_additive (attr := refl) "The identity map is a continuous additive isomorphism."]
def refl : M ≃ₜ* M :=
  { MulEquiv.refl _ with }

Identity continuous multiplicative isomorphism

Informal description

The identity map on a topological group $M$ is a continuous multiplicative isomorphism from $M$ to itself.

ContinuousMulEquiv.instInhabited instance

: Inhabited (M ≃ₜ* M)

Full source

@[to_additive]
instance : Inhabited (M ≃ₜ* M) := ⟨ContinuousMulEquiv.refl M⟩

Inhabited Type of Continuous Multiplicative Automorphisms

Informal description

For any topological group $M$, the type of continuous multiplicative isomorphisms from $M$ to itself is inhabited.

ContinuousMulEquiv.coe_refl theorem

: ↑(refl M) = id

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_refl : ↑(refl M) = id := rfl

Identity Continuous Multiplicative Isomorphism as Identity Function

Informal description

The underlying function of the identity continuous multiplicative isomorphism $\text{refl}_M$ from a topological group $M$ to itself is equal to the identity function $\text{id}$ on $M$.

ContinuousMulEquiv.refl_apply theorem

(m : M) : refl M m = m

Full source

@[to_additive (attr := simp)]
theorem refl_apply (m : M) : refl M m = m := rfl

Identity Continuous Multiplicative Isomorphism Acts as Identity

Informal description

For any element $m$ of a topological group $M$, the identity continuous multiplicative isomorphism evaluated at $m$ is equal to $m$, i.e., $\text{refl}_M(m) = m$.

ContinuousMulEquiv.symm definition

(cme : M ≃ₜ* N) : N ≃ₜ* M

Full source

/-- The inverse of a ContinuousMulEquiv. -/
@[to_additive (attr := symm) "The inverse of a ContinuousAddEquiv."]
def symm (cme : M ≃ₜ* N) : N ≃ₜ* M :=
  { cme.toMulEquiv.symm with
  continuous_toFun := cme.continuous_invFun
  continuous_invFun := cme.continuous_toFun }

Inverse of a continuous multiplicative isomorphism

Informal description

Given a continuous multiplicative isomorphism $f : M \simeq_{\text{top}}^* N$ between two topological groups $M$ and $N$, the inverse $f^{-1} : N \simeq_{\text{top}}^* M$ is also a continuous multiplicative isomorphism, where the continuous function of $f^{-1}$ is the inverse function of $f$, and vice versa.

ContinuousMulEquiv.invFun_eq_symm theorem

{f : M ≃ₜ* N} : f.invFun = f.symm

Full source

@[to_additive]
theorem invFun_eq_symm {f : M ≃ₜ* N} : f.invFun = f.symm := rfl

Inverse Function Equals Symmetric Isomorphism for Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $f \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the inverse function of $f$ is equal to its symmetric counterpart $f^{-1} \colon N \simeq_{\text{top}}^* M$.

ContinuousMulEquiv.coe_toHomeomorph_symm theorem

(f : M ≃ₜ* N) : (f : M ≃ₜ N).symm = (f.symm : N ≃ₜ M)

Full source

@[to_additive (attr := simp)]
theorem coe_toHomeomorph_symm (f : M ≃ₜ* N) : (f : M ≃ₜ N).symm = (f.symm : N ≃ₜ M) := rfl

Inverse of Underlying Homeomorphism Equals Homeomorphism of Inverse

Informal description

For any continuous multiplicative isomorphism $f \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the inverse of the underlying homeomorphism $f \colon M \simeq_{\text{top}} N$ is equal to the homeomorphism induced by the inverse isomorphism $f^{-1} \colon N \simeq_{\text{top}} M$.

ContinuousMulEquiv.equivLike_inv_eq_symm theorem

(f : M ≃ₜ* N) : EquivLike.inv f = f.symm

Full source

@[to_additive (attr := simp)]
theorem equivLike_inv_eq_symm (f : M ≃ₜ* N) : EquivLike.inv f = f.symm := rfl

Inverse of Continuous Multiplicative Isomorphism Equals Its Symmetric Counterpart

Informal description

For any continuous multiplicative isomorphism $f : M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the inverse function defined by the equivalence-like structure on $f$ is equal to the symmetric isomorphism $f^{-1} : N \simeq_{\text{top}}^* M$.

ContinuousMulEquiv.symm_symm theorem

(f : M ≃ₜ* N) : f.symm.symm = f

Full source

@[to_additive (attr := simp)]
theorem symm_symm (f : M ≃ₜ* N) : f.symm.symm = f := rfl

Double Inverse of Continuous Multiplicative Isomorphism

Informal description

For any continuous multiplicative isomorphism $f \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the inverse of the inverse of $f$ is equal to $f$ itself, i.e., $(f^{-1})^{-1} = f$.

ContinuousMulEquiv.symm_bijective theorem

: Function.Bijective (symm : M ≃ₜ* N → _)

Full source

@[to_additive]
theorem symm_bijective : Function.Bijective (symm : M ≃ₜ* N → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Continuous Multiplicative Isomorphisms

Informal description

The function that maps a continuous multiplicative isomorphism $f \colon M \simeq_{\text{top}}^* N$ to its inverse $f^{-1} \colon N \simeq_{\text{top}}^* M$ is bijective.

ContinuousMulEquiv.apply_symm_apply theorem

(e : M ≃ₜ* N) (y : N) : e (e.symm y) = y

Full source

/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`."]
theorem apply_symm_apply (e : M ≃ₜ* N) (y : N) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

Inverse Property of Continuous Multiplicative Isomorphism: $e(e^{-1}(y)) = y$

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, and for any $y \in N$, the composition of $e$ with its inverse satisfies $e(e^{-1}(y)) = y$.

ContinuousMulEquiv.symm_apply_apply theorem

(e : M ≃ₜ* N) (x : M) : e.symm (e x) = x

Full source

/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
@[to_additive (attr := simp) "`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`."]
theorem symm_apply_apply (e : M ≃ₜ* N) (x : M) : e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply x

Inverse Property of Continuous Multiplicative Isomorphism: $e^{-1}(e(x)) = x$

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, and for any $x \in M$, the inverse $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

ContinuousMulEquiv.symm_comp_self theorem

(e : M ≃ₜ* N) : e.symm ∘ e = id

Full source

@[to_additive (attr := simp)]
theorem symm_comp_self (e : M ≃ₜ* N) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

Inverse Composition Property: $e^{-1} \circ e = \text{id}_M$ for Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the composition of the inverse $e^{-1}$ with $e$ is equal to the identity function on $M$, i.e., $e^{-1} \circ e = \text{id}_M$.

ContinuousMulEquiv.self_comp_symm theorem

(e : M ≃ₜ* N) : e ∘ e.symm = id

Full source

@[to_additive (attr := simp)]
theorem self_comp_symm (e : M ≃ₜ* N) : e ∘ e.symm = id :=
  funext e.apply_symm_apply

Composition of Continuous Multiplicative Isomorphism with its Inverse Yields Identity

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $N$, i.e., $e \circ e^{-1} = \text{id}_N$.

ContinuousMulEquiv.apply_eq_iff_symm_apply theorem

(e : M ≃ₜ* N) {x : M} {y : N} : e x = y ↔ x = e.symm y

Full source

@[to_additive]
theorem apply_eq_iff_symm_apply (e : M ≃ₜ* N) {x : M} {y : N} : e x = y ↔ x = e.symm y :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

Equivalence of Application and Inverse Application for Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, and for any elements $x \in M$ and $y \in N$, the equality $e(x) = y$ holds if and only if $x = e^{-1}(y)$.

ContinuousMulEquiv.symm_apply_eq theorem

(e : M ≃ₜ* N) {x y} : e.symm x = y ↔ x = e y

Full source

@[to_additive]
theorem symm_apply_eq (e : M ≃ₜ* N) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

Inverse Application Equivalence for Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, and for any elements $x \in N$ and $y \in M$, we have $e^{-1}(x) = y$ if and only if $x = e(y)$.

ContinuousMulEquiv.comp_symm_eq theorem

{α : Type*} (e : M ≃ₜ* N) (f : N → α) (g : M → α) : g ∘ e.symm = f ↔ g = f ∘ e

Full source

@[to_additive]
theorem comp_symm_eq {α : Type*} (e : M ≃ₜ* N) (f : N → α) (g : M → α) :
    g ∘ e.symmg ∘ e.symm = f ↔ g = f ∘ e :=
  e.toEquiv.comp_symm_eq f g

Composition with Inverse Characterization for Continuous Multiplicative Isomorphisms

Informal description

Let $e \colon M \simeq_{\text{top}}^* N$ be a continuous multiplicative isomorphism between topological groups $M$ and $N$, and let $f \colon N \to \alpha$ and $g \colon M \to \alpha$ be arbitrary functions to some type $\alpha$. Then the composition $g \circ e^{-1}$ equals $f$ if and only if $g$ equals $f \circ e$.

ContinuousMulEquiv.symm_comp_eq theorem

{α : Type*} (e : M ≃ₜ* N) (f : α → M) (g : α → N) : e.symm ∘ g = f ↔ g = e ∘ f

Full source

@[to_additive]
theorem symm_comp_eq {α : Type*} (e : M ≃ₜ* N) (f : α → M) (g : α → N) :
    e.symm ∘ ge.symm ∘ g = f ↔ g = e ∘ f :=
  e.toEquiv.symm_comp_eq f g

Inverse Composition Characterization for Continuous Multiplicative Isomorphisms

Informal description

Let $e \colon M \simeq^* N$ be a continuous multiplicative isomorphism between topological groups $M$ and $N$, and let $f \colon \alpha \to M$ and $g \colon \alpha \to N$ be arbitrary functions from some type $\alpha$. Then the composition $e^{-1} \circ g$ equals $f$ if and only if $g$ equals $e \circ f$.

ContinuousMulEquiv.trans definition

(cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L) : M ≃ₜ* L

Full source

/-- The composition of two ContinuousMulEquiv. -/
@[to_additive "The composition of two ContinuousAddEquiv."]
def trans (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L) : M ≃ₜ* L where
  __ := cme1.toMulEquiv.trans cme2.toMulEquiv
  continuous_toFun := by convert Continuous.comp cme2.continuous_toFun cme1.continuous_toFun
  continuous_invFun := by convert Continuous.comp cme1.continuous_invFun cme2.continuous_invFun

Composition of continuous multiplicative isomorphisms

Informal description

Given two continuous multiplicative isomorphisms $cme_1 : M \simeq^* N$ and $cme_2 : N \simeq^* L$, the composition $cme_2 \circ cme_1$ is a continuous multiplicative isomorphism from $M$ to $L$. This composition preserves both the multiplicative structure and continuity in both directions.

ContinuousMulEquiv.coe_trans theorem

(e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) : ↑(e₁.trans e₂) = e₂ ∘ e₁

Full source

@[to_additive (attr := simp)]
theorem coe_trans (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) : ↑(e₁.trans e₂) = e₂ ∘ e₁ := rfl

Composition of Continuous Multiplicative Isomorphisms Preserves Function Composition

Informal description

For any continuous multiplicative isomorphisms $e_1 \colon M \simeq^* N$ and $e_2 \colon N \simeq^* L$, the underlying function of the composition $e_1 \circ e_2$ is equal to the composition of the underlying functions $e_2 \circ e_1$.

ContinuousMulEquiv.trans_apply theorem

(e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (m : M) : e₁.trans e₂ m = e₂ (e₁ m)

Full source

@[to_additive (attr := simp)]
theorem trans_apply (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (m : M) : e₁.trans e₂ m = e₂ (e₁ m) := rfl

Application of Composition of Continuous Multiplicative Isomorphisms: $(e_1 \circ e_2)(m) = e_2(e_1(m))$

Informal description

For any continuous multiplicative isomorphisms $e_1 \colon M \simeq^* N$ and $e_2 \colon N \simeq^* L$, and any element $m \in M$, the application of the composed isomorphism $e_1 \circ e_2$ to $m$ equals the application of $e_2$ to the result of applying $e_1$ to $m$, i.e., $(e_1 \circ e_2)(m) = e_2(e_1(m))$.

ContinuousMulEquiv.symm_trans_apply theorem

(e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (l : L) : (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)

Full source

@[to_additive (attr := simp)]
theorem symm_trans_apply (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (l : L) :
    (e₁.trans e₂).symm l = e₁.symm (e₂.symm l) := rfl

Inverse of Composition of Continuous Multiplicative Isomorphisms

Informal description

For any continuous multiplicative isomorphisms $e_1 \colon M \simeq^* N$ and $e_2 \colon N \simeq^* L$, and any element $l \in L$, the inverse of the composition $e_1 \circ e_2$ applied to $l$ equals the composition of the inverses $e_1^{-1} \circ e_2^{-1}$ applied to $l$, i.e., $(e_1 \circ e_2)^{-1}(l) = e_1^{-1}(e_2^{-1}(l))$.

ContinuousMulEquiv.symm_trans_self theorem

(e : M ≃ₜ* N) : e.symm.trans e = refl N

Full source

@[to_additive (attr := simp)]
theorem symm_trans_self (e : M ≃ₜ* N) : e.symm.trans e = refl N :=
  DFunLike.ext _ _ e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}_N$

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the composition of the inverse isomorphism $e^{-1}$ with $e$ is equal to the identity isomorphism on $N$, i.e., $e^{-1} \circ e = \text{id}_N$.

ContinuousMulEquiv.self_trans_symm theorem

(e : M ≃ₜ* N) : e.trans e.symm = refl M

Full source

@[to_additive (attr := simp)]
theorem self_trans_symm (e : M ≃ₜ* N) : e.trans e.symm = refl M :=
  DFunLike.ext _ _ e.symm_apply_apply

Composition of Continuous Multiplicative Isomorphism with Its Inverse Yields Identity on $M$

Informal description

For any continuous multiplicative isomorphism $e \colon M \simeq_{\text{top}}^* N$ between topological groups $M$ and $N$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity isomorphism on $M$, i.e., $e \circ e^{-1} = \text{id}_M$.

ContinuousMulEquiv.ofUnique definition

{M N} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] : M ≃ₜ* N

Full source

/-- The `MulEquiv` between two monoids with a unique element. -/
@[to_additive "The `AddEquiv` between two `AddMonoid`s with a unique element."]
def ofUnique {M N} [Unique M] [Unique N] [Mul M] [Mul N]
    [TopologicalSpace M] [TopologicalSpace N] : M ≃ₜ* N where
  __ := MulEquiv.ofUnique
  continuous_toFun := by continuity
  continuous_invFun := by continuity

Continuous multiplicative isomorphism between unique monoids

Informal description

The multiplicative isomorphism between two monoids $M$ and $N$ each having a unique element, equipped with multiplication operations and topological structures. This isomorphism is both continuous and has a continuous inverse.

ContinuousMulEquiv.instUnique instance

{M N} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] : Unique (M ≃ₜ* N)

Full source

/-- There is a unique monoid homomorphism between two monoids with a unique element. -/
@[to_additive "There is a unique additive monoid homomorphism between two additive monoids with
  a unique element."]
instance {M N} [Unique M] [Unique N] [Mul M] [Mul N]
    [TopologicalSpace M] [TopologicalSpace N] : Unique (M ≃ₜ* N) where
  default := ofUnique
  uniq _ := ext fun _ ↦ Subsingleton.elim _ _

Uniqueness of Continuous Multiplicative Isomorphism Between Unique Monoids

Informal description

For any two monoids $M$ and $N$ each having a unique element, equipped with multiplication operations and topological structures, there is a unique continuous multiplicative isomorphism between them.

Mathlib.Topology.Algebra.ContinuousMonoidHom

Main definitions

Main definitions