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 MulOpposite.unop

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

Continuous AddOpposite.unop

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

Continuous MulOpposite.op

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

Continuous AddOpposite.op

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ᵐᵒᵖ) :

MulOpposite.opHomeomorph.symm a✝ = MulOpposite.unop a✝

@[simp]

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

AddOpposite.opHomeomorph a✝ = AddOpposite.op a✝

@[simp]

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

AddOpposite.opHomeomorph.symm a✝ = AddOpposite.unop a✝

@[simp]

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

MulOpposite.opHomeomorph a✝ = MulOpposite.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 MulOpposite.op (nhds x) = nhds (MulOpposite.op x)

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Filter.comap AddOpposite.unop (nhds x) = nhds (AddOpposite.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 ⇑(Units.embedProduct M)

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

Topology.IsInducing ⇑(AddUnits.embedProduct M)

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

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

Topology.IsInducing ⇑(Units.embedProduct M)

Alias of Units.isInducing_embedProduct.

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

Topology.IsEmbedding ⇑(Units.embedProduct M)

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

Topology.IsEmbedding ⇑(AddUnits.embedProduct M)

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

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

Topology.IsEmbedding ⇑(Units.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] :

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

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

AddUnits.instTopologicalSpaceAddUnits = TopologicalSpace.induced AddUnits.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 Units.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 AddUnits.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 Units.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 Units.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 AddUnits.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 ⇑(Units.embedProduct M)

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

Continuous ⇑(AddUnits.embedProduct M)

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

Continuous Units.val

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

Continuous AddUnits.val

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

Continuous f ↔ Continuous (Units.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 (AddUnits.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)