Documentation

Mathlib.Topology.Algebra.Constructions

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

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

Tags #

topological space, opposite monoid, units

@[instance_reducible]

instance MulOpposite.instTopologicalSpaceMulOpposite {M : Type u_1} [TopologicalSpace M] :

TopologicalSpace Mᵐᵒᵖ

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

Equations

MulOpposite.instTopologicalSpaceMulOpposite = TopologicalSpace.induced MulOpposite.unop inst✝

@[instance_reducible]

instance AddOpposite.instTopologicalSpaceAddOpposite {M : Type u_1} [TopologicalSpace M] :

TopologicalSpace Mᵃᵒᵖ

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

Equations

AddOpposite.instTopologicalSpaceAddOpposite = TopologicalSpace.induced AddOpposite.unop inst✝

theorem MulOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :

Continuous unop

theorem AddOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :

Continuous unop

theorem MulOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :

theorem AddOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :

def MulOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] :

M ≃ₜ Mᵐᵒᵖ

MulOpposite.op as a homeomorphism.

Equations

MulOpposite.opHomeomorph = { toEquiv := MulOpposite.opEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

def AddOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] :

M ≃ₜ Mᵃᵒᵖ

AddOpposite.op as a homeomorphism.

Equations

AddOpposite.opHomeomorph = { toEquiv := AddOpposite.opEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[simp]

theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] (a✝ : Mᵐᵒᵖ) :

opHomeomorph.symm a✝ = unop a✝

@[simp]

theorem AddOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] (a✝ : M) :

opHomeomorph a✝ = op a✝

@[simp]

theorem AddOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] (a✝ : Mᵃᵒᵖ) :

opHomeomorph.symm a✝ = unop a✝

@[simp]

theorem MulOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] (a✝ : M) :

opHomeomorph a✝ = op a✝

instance MulOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :

T2Space Mᵐᵒᵖ

instance AddOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :

T2Space Mᵃᵒᵖ

instance MulOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :

DiscreteTopology Mᵐᵒᵖ

instance AddOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :

DiscreteTopology Mᵃᵒᵖ

instance MulOpposite.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :

CompactSpace Mᵐᵒᵖ

instance AddOpposite.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :

CompactSpace Mᵃᵒᵖ

instance MulOpposite.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :

WeaklyLocallyCompactSpace Mᵐᵒᵖ

instance AddOpposite.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :

WeaklyLocallyCompactSpace Mᵃᵒᵖ

instance MulOpposite.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :

LocallyCompactSpace Mᵐᵒᵖ

instance AddOpposite.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :

LocallyCompactSpace Mᵃᵒᵖ

@[simp]

theorem MulOpposite.map_op_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.map op (nhds x) = nhds (op x)

@[simp]

theorem AddOpposite.map_op_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.map op (nhds x) = nhds (op x)

@[simp]

theorem MulOpposite.map_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) :

Filter.map unop (nhds x) = nhds (unop x)

@[simp]

theorem AddOpposite.map_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵃᵒᵖ) :

Filter.map unop (nhds x) = nhds (unop x)

@[simp]

theorem MulOpposite.comap_op_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) :

Filter.comap op (nhds x) = nhds (unop x)

@[simp]

theorem AddOpposite.comap_op_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵃᵒᵖ) :

Filter.comap op (nhds x) = nhds (unop x)

@[simp]

theorem MulOpposite.comap_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.comap unop (nhds x) = nhds (op x)

@[simp]

theorem AddOpposite.comap_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.comap unop (nhds x) = nhds (op x)

@[instance_reducible]

instance Units.instTopologicalSpaceUnits {M : Type u_1} [TopologicalSpace M] [Monoid M] :

TopologicalSpace Mˣ

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

Equations

Units.instTopologicalSpaceUnits = TopologicalSpace.induced (⇑(Units.embedProduct M)) inferInstance

@[instance_reducible]

instance AddUnits.instTopologicalSpaceAddUnits {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

TopologicalSpace (AddUnits M)

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

Equations

AddUnits.instTopologicalSpaceAddUnits = TopologicalSpace.induced (⇑(AddUnits.embedProduct M)) inferInstance

theorem Units.isInducing_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :

Topology.IsInducing ⇑(embedProduct M)

theorem AddUnits.isInducing_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

Topology.IsInducing ⇑(embedProduct M)

theorem Units.isEmbedding_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :

Topology.IsEmbedding ⇑(embedProduct M)

theorem AddUnits.isEmbedding_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

Topology.IsEmbedding ⇑(embedProduct M)

instance Units.instT2Space {M : Type u_1} [TopologicalSpace M] [Monoid M] [T2Space M] :

instance AddUnits.instT2Space {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [T2Space M] :

T2Space (AddUnits M)

instance Units.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [Monoid M] [DiscreteTopology M] :

DiscreteTopology Mˣ

instance AddUnits.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [DiscreteTopology M] :

DiscreteTopology (AddUnits M)

theorem Units.topology_eq_inf {M : Type u_1} [TopologicalSpace M] [Monoid M] :

instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝ ⊓ TopologicalSpace.induced (fun (u : Mˣ) => ↑u⁻¹) inst✝

theorem AddUnits.topology_eq_inf {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

instTopologicalSpaceAddUnits = TopologicalSpace.induced val inst✝ ⊓ TopologicalSpace.induced (fun (u : AddUnits M) => ↑(-u)) inst✝

theorem Units.isEmbedding_val_mk' {M : Type u_4} [Monoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹) :

Topology.IsEmbedding val

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use Units.isEmbedding_val₀, Units.isEmbedding_val, or toUnits_homeomorph instead.

theorem AddUnits.isEmbedding_val_mk' {M : Type u_4} [AddMonoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x : M | IsAddUnit x}) (hf : ∀ (u : AddUnits M), f ↑u = ↑(-u)) :

Topology.IsEmbedding val

An auxiliary lemma that can be used to prove that coercion AddUnits M → M is a topological embedding. Use AddUnits.isEmbedding_val or toAddUnits_homeomorph instead.

theorem Units.embedding_val_mk {M : Type u_4} [DivisionMonoid M] [TopologicalSpace M] (h : ContinuousOn Inv.inv {x : M | IsUnit x}) :

Topology.IsEmbedding val

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use Units.isEmbedding_val₀, Units.isEmbedding_val, or toUnits_homeomorph instead.

theorem AddUnits.embedding_val_mk {M : Type u_4} [SubtractionMonoid M] [TopologicalSpace M] (h : ContinuousOn Neg.neg {x : M | IsAddUnit x}) :

Topology.IsEmbedding val

An auxiliary lemma that can be used to prove that coercion AddUnits M → M is a topological embedding. Use AddUnits.isEmbedding_val or toAddUnits_homeomorph instead.

theorem Units.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :

Continuous ⇑(embedProduct M)

theorem AddUnits.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

Continuous ⇑(embedProduct M)

theorem Units.continuous_val {M : Type u_1} [TopologicalSpace M] [Monoid M] :

theorem AddUnits.continuous_val {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

theorem Units.continuous_iff {M : Type u_1} {X : Type u_3} [TopologicalSpace M] [Monoid M] [TopologicalSpace X] {f : X → Mˣ} :

Continuous f ↔ Continuous (val ∘ f) ∧ Continuous fun (x : X) => ↑(f x)⁻¹

theorem AddUnits.continuous_iff {M : Type u_1} {X : Type u_3} [TopologicalSpace M] [AddMonoid M] [TopologicalSpace X] {f : X → AddUnits M} :

Continuous f ↔ Continuous (val ∘ f) ∧ Continuous fun (x : X) => ↑(-f x)

theorem Units.continuous_coe_inv {M : Type u_1} [TopologicalSpace M] [Monoid M] :

Continuous fun (u : Mˣ) => ↑u⁻¹

theorem AddUnits.continuous_coe_neg {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :

Continuous fun (u : AddUnits M) => ↑(-u)

theorem Units.continuous_map {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [Monoid M] [TopologicalSpace N] [Monoid N] {f : M →* N} (hf : Continuous ⇑f) :

Continuous ⇑(map f)

theorem AddUnits.continuous_map {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [AddMonoid M] [TopologicalSpace N] [AddMonoid N] {f : M →+ N} (hf : Continuous ⇑f) :

Continuous ⇑(map f)

theorem Units.isOpenMap_map {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [Monoid M] [TopologicalSpace N] [Monoid N] {f : M →* N} (hf_inj : Function.Injective ⇑f) (hf : IsOpenMap ⇑f) :

IsOpenMap ⇑(map f)

theorem AddUnits.isOpenMap_map {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [AddMonoid M] [TopologicalSpace N] [AddMonoid N] {f : M →+ N} (hf_inj : Function.Injective ⇑f) (hf : IsOpenMap ⇑f) :

IsOpenMap ⇑(map f)