# mathlib3documentation

topology.algebra.constructions

# Topological space structure on the opposite monoid and on the units group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define topological_space structure on Mᵐᵒᵖ, Mᵃᵒᵖ, Mˣ, and add_units M. This file does not import definitions of a topological monoid and/or a continuous multiplicative action, so we postpone the proofs of has_continuous_mul Mᵐᵒᵖ etc till we have these definitions.

## Tags #

topological space, opposite monoid, units

@[protected, instance]

Put the same topological space structure on the opposite monoid as on the original space.

Equations
@[protected, instance]

Put the same topological space structure on the opposite monoid as on the original space.

Equations
@[continuity]
theorem add_opposite.continuous_unop {M : Type u_1}  :
@[continuity]
theorem mul_opposite.continuous_unop {M : Type u_1}  :
@[continuity]
theorem add_opposite.continuous_op {M : Type u_1}  :
@[continuity]
theorem mul_opposite.continuous_op {M : Type u_1}  :
@[simp]
theorem add_opposite.op_homeomorph_apply {M : Type u_1} (ᾰ : M) :
@[simp]
theorem add_opposite.op_homeomorph_symm_apply {M : Type u_1} (ᾰ : Mᵃᵒᵖ) :
@[simp]
theorem mul_opposite.op_homeomorph_apply {M : Type u_1} (ᾰ : M) :
@[simp]
theorem mul_opposite.op_homeomorph_symm_apply {M : Type u_1} (ᾰ : Mᵐᵒᵖ) :

mul_opposite.op as a homeomorphism.

Equations

add_opposite.op as a homeomorphism.

Equations
@[protected, instance]
def add_opposite.t2_space {M : Type u_1} [t2_space M] :
@[protected, instance]
def mul_opposite.t2_space {M : Type u_1} [t2_space M] :
@[simp]
theorem mul_opposite.map_op_nhds {M : Type u_1} (x : M) :
@[simp]
theorem add_opposite.map_op_nhds {M : Type u_1} (x : M) :
@[simp]
theorem mul_opposite.map_unop_nhds {M : Type u_1} (x : Mᵐᵒᵖ) :
@[simp]
theorem add_opposite.map_unop_nhds {M : Type u_1} (x : Mᵃᵒᵖ) :
@[simp]
theorem add_opposite.comap_op_nhds {M : Type u_1} (x : Mᵃᵒᵖ) :
@[simp]
theorem mul_opposite.comap_op_nhds {M : Type u_1} (x : Mᵐᵒᵖ) :
@[simp]
theorem add_opposite.comap_unop_nhds {M : Type u_1} (x : M) :
@[simp]
theorem mul_opposite.comap_unop_nhds {M : Type u_1} (x : M) :
@[protected, instance]
def units.topological_space {M : Type u_1} [monoid M] :

The units of a monoid are equipped with a topology, via the embedding into M × M.

Equations
@[protected, instance]

The additive units of a monoid are equipped with a topology, via the embedding into M × M.

Equations
theorem units.inducing_embed_product {M : Type u_1} [monoid M] :
theorem units.embedding_embed_product {M : Type u_1} [monoid M] :
theorem units.topology_eq_inf {M : Type u_1} [monoid M] :
theorem units.embedding_coe_mk {M : Type u_1} (h : {x : M | is_unit x}) :

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use units.coe_embedding₀, units.coe_embedding, or to_units_homeomorph instead.

theorem add_units.embedding_coe_mk {M : Type u_1} (h : {x : M | ) :

An auxiliary lemma that can be used to prove that coercion add_units M → M is a topological embedding. Use add_units.coe_embedding or to_add_units_homeomorph instead.

theorem units.continuous_coe {M : Type u_1} [monoid M] :
theorem add_units.continuous_coe {M : Type u_1} [add_monoid M] :
@[protected]
theorem units.continuous_iff {M : Type u_1} {X : Type u_2} [monoid M] {f : X Mˣ} :
continuous (coe f) continuous (λ (x : X), (f x)⁻¹)
@[protected]
theorem add_units.continuous_iff {M : Type u_1} {X : Type u_2} [add_monoid M] {f : X } :
continuous (coe f) continuous (λ (x : X), -f x)
theorem add_units.continuous_coe_neg {M : Type u_1} [add_monoid M] :
continuous (λ (u : , -u)
theorem units.continuous_coe_inv {M : Type u_1} [monoid M] :
continuous (λ (u : Mˣ), u⁻¹)