mathlib3 documentation

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

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.

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.

@[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 units.continuous_coe_inv {M : Type u_1} [topological_space M] [monoid M] :
continuous (λ (u : Mˣ), u⁻¹)