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ᵃᵒᵖ, , 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]
@[continuity]
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[protected, instance]

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
@[protected]
theorem units.continuous_iff {M : Type u_1} {X : Type u_2} [topological_space M] [monoid M] [topological_space X] {f : X → Mˣ} :
@[protected]
theorem add_units.continuous_iff {M : Type u_1} {X : Type u_2} [topological_space M] [add_monoid M] [topological_space X] {f : X → add_units M} :
theorem add_units.continuous_coe_neg {M : Type u_1} [topological_space M] [add_monoid M] :
continuous (λ (u : add_units M), -u)
theorem units.continuous_coe_inv {M : Type u_1} [topological_space M] [monoid M] :
continuous (λ (u : Mˣ), u⁻¹)