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 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 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ᵃᵒᵖ

@[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 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 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)

@[deprecated Units.isInducing_embedProduct (since := "2024-10-28")]

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

Topology.IsInducing ⇑(embedProduct M)

Alias of Units.isInducing_embedProduct.

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)

@[deprecated Units.isEmbedding_embedProduct (since := "2024-10-26")]

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

Topology.IsEmbedding ⇑(embedProduct M)

Alias of Units.isEmbedding_embedProduct.

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_3} [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_3} [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.

@[deprecated Units.isEmbedding_val_mk' (since := "2024-10-26")]

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

Topology.IsEmbedding val

Alias of Units.isEmbedding_val_mk'.

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 Units.embedding_val_mk {M : Type u_3} [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_3} [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_2} [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_2} [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)