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 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

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

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

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

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

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

def AddOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] : M ≃ₜ Mᵃᵒᵖ

AddOpposite.op as a homeomorphism.

Equations

• AddOpposite.opHomeomorph = Homeomorph.mk AddOpposite.opEquiv

@[simp]

theorem MulOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] : ∀ (a : M), MulOpposite.opHomeomorph a = MulOpposite.op a

@[simp]

theorem AddOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] : ∀ (a : Mᵃᵒᵖ), (Homeomorph.symm AddOpposite.opHomeomorph) a = AddOpposite.unop a

@[simp]

theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] : ∀ (a : Mᵐᵒᵖ), (Homeomorph.symm MulOpposite.opHomeomorph) a = MulOpposite.unop a

@[simp]

theorem AddOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] : ∀ (a : M), AddOpposite.opHomeomorph a = AddOpposite.op a

def MulOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] : M ≃ₜ Mᵐᵒᵖ

MulOpposite.op as a homeomorphism.

Equations

• MulOpposite.opHomeomorph = Homeomorph.mk MulOpposite.opEquiv

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

Equations

• (_ : T2Space Mᵃᵒᵖ) = (_ : T2Space Mᵃᵒᵖ)

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

Equations

• (_ : T2Space Mᵐᵒᵖ) = (_ : T2Space Mᵐᵒᵖ)

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

Equations

• (_ : DiscreteTopology Mᵃᵒᵖ) = (_ : DiscreteTopology Mᵃᵒᵖ)

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

Equations

• (_ : DiscreteTopology Mᵐᵒᵖ) = (_ : DiscreteTopology Mᵐᵒᵖ)

@[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_op_nhds {M : Type u_1} [TopologicalSpace M] (x : M) : Filter.map MulOpposite.op (nhds x) = nhds (MulOpposite.op 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.map_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) : Filter.map MulOpposite.unop (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_op_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) : Filter.comap MulOpposite.op (nhds x) = nhds (MulOpposite.unop 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)

@[simp]

theorem MulOpposite.comap_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) : Filter.comap MulOpposite.unop (nhds x) = nhds (MulOpposite.op x)

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

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

theorem AddUnits.inducing_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : Inducing ⇑(AddUnits.embedProduct M)

theorem Units.inducing_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] : Inducing ⇑(Units.embedProduct M)

theorem AddUnits.embedding_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : Embedding ⇑(AddUnits.embedProduct M)

theorem Units.embedding_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] : Embedding ⇑(Units.embedProduct M)

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

Equations

• (_ : T2Space (AddUnits M)) = (_ : T2Space (AddUnits M))

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

Equations

• (_ : T2Space Mˣ) = (_ : T2Space Mˣ)

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

Equations

• (_ : DiscreteTopology (AddUnits M)) = (_ : DiscreteTopology (AddUnits M))

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

Equations

• (_ : DiscreteTopology Mˣ) = (_ : DiscreteTopology Mˣ)

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.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.embedding_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)) : Embedding AddUnits.val

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

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⁻¹) : Embedding Units.val

An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding. Use Units.embedding_val₀, Units.embedding_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}) : Embedding AddUnits.val

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

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

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

theorem AddUnits.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : Continuous ⇑(AddUnits.embedProduct M)

theorem Units.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] : Continuous ⇑(Units.embedProduct M)

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

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

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_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_coe_neg {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : Continuous fun (u : AddUnits M) => ↑(-u)

theorem Units.continuous_coe_inv {M : Type u_1} [TopologicalSpace M] [Monoid M] : Continuous fun (u : Mˣ) => ↑u⁻¹