mathlib documentation

topology.algebra.constructions

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

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

source
@[protected, instance]
def mul_opposite.topological_space {M : Type u_1} [topological_space M] :
topological_space Mᵐᵒᵖ

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

Equations
source
@[protected, instance]
def add_opposite.topological_space {M : Type u_1} [topological_space M] :
topological_space Mᵃᵒᵖ
Equations
source
@[continuity]
theorem add_opposite.continuous_unop {M : Type u_1} [topological_space M] :
continuous add_opposite.unop
source
@[continuity]
theorem mul_opposite.continuous_unop {M : Type u_1} [topological_space M] :
continuous mul_opposite.unop
source
@[continuity]
theorem add_opposite.continuous_op {M : Type u_1} [topological_space M] :
continuous add_opposite.op
source
@[continuity]
theorem mul_opposite.continuous_op {M : Type u_1} [topological_space M] :
continuous mul_opposite.op
source
def mul_opposite.op_homeomorph {M : Type u_1} [topological_space M] :
M ≃ₜ Mᵐᵒᵖ

mul_opposite.op as a homeomorphism.

Equations
source
def add_opposite.op_homeomorph {M : Type u_1} [topological_space M] :
M ≃ₜ Mᵃᵒᵖ

add_opposite.op as a homeomorphism.

Equations
source
@[simp]
theorem mul_opposite.map_op_nhds {M : Type u_1} [topological_space M] (x : M) :
filter.map mul_opposite.op (𝓝 x) = 𝓝 (mul_opposite.op x)
source
@[simp]
theorem add_opposite.map_op_nhds {M : Type u_1} [topological_space M] (x : M) :
filter.map add_opposite.op (𝓝 x) = 𝓝 (add_opposite.op x)
source
@[simp]
theorem mul_opposite.map_unop_nhds {M : Type u_1} [topological_space M] (x : Mᵐᵒᵖ) :
filter.map mul_opposite.unop (𝓝 x) = 𝓝 (mul_opposite.unop x)
source
@[simp]
theorem add_opposite.map_unop_nhds {M : Type u_1} [topological_space M] (x : Mᵃᵒᵖ) :
filter.map add_opposite.unop (𝓝 x) = 𝓝 (add_opposite.unop x)
source
@[simp]
theorem add_opposite.comap_op_nhds {M : Type u_1} [topological_space M] (x : Mᵃᵒᵖ) :
filter.comap add_opposite.op (𝓝 x) = 𝓝 (add_opposite.unop x)
source
@[simp]
theorem mul_opposite.comap_op_nhds {M : Type u_1} [topological_space M] (x : Mᵐᵒᵖ) :
filter.comap mul_opposite.op (𝓝 x) = 𝓝 (mul_opposite.unop x)
source
@[simp]
theorem add_opposite.comap_unop_nhds {M : Type u_1} [topological_space M] (x : M) :
filter.comap add_opposite.unop (𝓝 x) = 𝓝 (add_opposite.op x)
source
@[simp]
theorem mul_opposite.comap_unop_nhds {M : Type u_1} [topological_space M] (x : M) :
filter.comap mul_opposite.unop (𝓝 x) = 𝓝 (mul_opposite.op x)
source
@[protected, instance]
def units.topological_space {M : Type u_1} [topological_space M] [monoid M] :
topological_space Mˣ

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

Equations
source
@[protected, instance]
def add_units.topological_space {M : Type u_1} [topological_space M] [add_monoid M] :
topological_space (add_units M)
Equations
source
theorem units.continuous_embed_product {M : Type u_1} [topological_space M] [monoid M] :
continuous ⇑(units.embed_product M)
source
theorem add_units.continuous_embed_product {M : Type u_1} [topological_space M] [add_monoid M] :
continuous ⇑(add_units.embed_product M)
source
theorem units.continuous_coe {M : Type u_1} [topological_space M] [monoid M] :
continuous coe
source
theorem add_units.continuous_coe {M : Type u_1} [topological_space M] [add_monoid M] :
continuous coe