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

source
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
source
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
source
theorem MulOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :
Continuous MulOpposite.unop
source
theorem AddOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :
Continuous AddOpposite.unop
source
theorem MulOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :
Continuous MulOpposite.op
source
theorem AddOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :
Continuous AddOpposite.op
source
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
    source
    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
      source
      @[simp]
      theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] (a✝ : Mᵐᵒᵖ) :
      MulOpposite.opHomeomorph.symm a✝ = MulOpposite.unop a✝
      source
      @[simp]
      theorem AddOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] (a✝ : M) :
      AddOpposite.opHomeomorph a✝ = AddOpposite.op a✝
      source
      @[simp]
      theorem AddOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] (a✝ : Mᵃᵒᵖ) :
      AddOpposite.opHomeomorph.symm a✝ = AddOpposite.unop a✝
      source
      @[simp]
      theorem MulOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] (a✝ : M) :
      MulOpposite.opHomeomorph a✝ = MulOpposite.op a✝
      source
      instance MulOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵐᵒᵖ
      source
      instance AddOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵃᵒᵖ
      source
      instance MulOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵐᵒᵖ
      source
      instance AddOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵃᵒᵖ
      source
      @[simp]
      theorem MulOpposite.map_op_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map MulOpposite.op (nhds x) = nhds (MulOpposite.op x)
      source
      @[simp]
      theorem AddOpposite.map_op_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map AddOpposite.op (nhds x) = nhds (AddOpposite.op x)
      source
      @[simp]
      theorem MulOpposite.map_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) :
      Filter.map MulOpposite.unop (nhds x) = nhds (MulOpposite.unop x)
      source
      @[simp]
      theorem AddOpposite.map_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵃᵒᵖ) :
      Filter.map AddOpposite.unop (nhds x) = nhds (AddOpposite.unop x)
      source
      @[simp]
      theorem MulOpposite.comap_op_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵐᵒᵖ) :
      Filter.comap MulOpposite.op (nhds x) = nhds (MulOpposite.unop x)
      source
      @[simp]
      theorem AddOpposite.comap_op_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵃᵒᵖ) :
      Filter.comap AddOpposite.op (nhds x) = nhds (AddOpposite.unop x)
      source
      @[simp]
      theorem MulOpposite.comap_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap MulOpposite.unop (nhds x) = nhds (MulOpposite.op x)
      source
      @[simp]
      theorem AddOpposite.comap_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap AddOpposite.unop (nhds x) = nhds (AddOpposite.op x)
      source
      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
      source
      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
      source
      theorem Units.isInducing_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Topology.IsInducing ⇑(Units.embedProduct M)
      source
      theorem AddUnits.isInducing_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Topology.IsInducing ⇑(AddUnits.embedProduct M)
      source
      @[deprecated Units.isInducing_embedProduct]
      theorem Units.inducing_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Topology.IsInducing ⇑(Units.embedProduct M)

      Alias of Units.isInducing_embedProduct.

      source
      theorem Units.isEmbedding_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Topology.IsEmbedding ⇑(Units.embedProduct M)
      source
      theorem AddUnits.isEmbedding_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Topology.IsEmbedding ⇑(AddUnits.embedProduct M)
      source
      @[deprecated Units.isEmbedding_embedProduct]
      theorem Units.embedding_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Topology.IsEmbedding ⇑(Units.embedProduct M)

      Alias of Units.isEmbedding_embedProduct.

      source
      instance Units.instT2Space {M : Type u_1} [TopologicalSpace M] [Monoid M] [T2Space M] :
      T2Space Mˣ
      source
      instance AddUnits.instT2Space {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [T2Space M] :
      T2Space (AddUnits M)
      source
      instance Units.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [Monoid M] [DiscreteTopology M] :
      DiscreteTopology Mˣ
      source
      instance AddUnits.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [DiscreteTopology M] :
      DiscreteTopology (AddUnits M)
      source
      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✝
      source
      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✝
      source
      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.

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

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

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

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

      source
      theorem Units.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Continuous ⇑(Units.embedProduct M)
      source
      theorem AddUnits.continuous_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Continuous ⇑(AddUnits.embedProduct M)
      source
      theorem Units.continuous_val {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Continuous Units.val
      source
      theorem AddUnits.continuous_val {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Continuous AddUnits.val
      source
      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)⁻¹
      source
      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)
      source
      theorem Units.continuous_coe_inv {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Continuous fun (u : Mˣ) => ↑u⁻¹
      source
      theorem AddUnits.continuous_coe_neg {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Continuous fun (u : AddUnits M) => ↑(-u)