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 = { toEquiv := AddOpposite.opEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

@[simp]

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

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 := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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.isInducing_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : IsInducing ⇑(AddUnits.embedProduct M)

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

@[deprecated Units.isInducing_embedProduct]

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

Alias of Units.isInducing_embedProduct.

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

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

@[deprecated Units.isEmbedding_embedProduct]

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

Alias of Units.isEmbedding_embedProduct.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

@[deprecated Units.isEmbedding_val_mk']

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⁻¹) : 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 AddUnits.embedding_val_mk {M : Type u_3} [SubtractionMonoid M] [TopologicalSpace M] (h : ContinuousOn Neg.neg {x : M | IsAddUnit x}) : 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.embedding_val_mk {M : Type u_3} [DivisionMonoid M] [TopologicalSpace M] (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : 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.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⁻¹