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 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
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
theorem AddOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :
Continuous AddOpposite.unop
source
theorem MulOpposite.continuous_unop {M : Type u_1} [TopologicalSpace M] :
Continuous MulOpposite.unop
source
theorem AddOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :
Continuous AddOpposite.op
source
theorem MulOpposite.continuous_op {M : Type u_1} [TopologicalSpace M] :
Continuous MulOpposite.op
source
def AddOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] :
M ≃ₜ Mᵃᵒᵖ

AddOpposite.op as a homeomorphism.

Equations
Instances For
    source
    @[simp]
    theorem MulOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] :
    ∀ (a : Mᵐᵒᵖ), ↑(Homeomorph.symm MulOpposite.opHomeomorph) 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 MulOpposite.opHomeomorph_apply {M : Type u_1} [TopologicalSpace M] :
    ∀ (a : M), ↑MulOpposite.opHomeomorph a = MulOpposite.op a
    source
    @[simp]
    theorem AddOpposite.opHomeomorph_symm_apply {M : Type u_1} [TopologicalSpace M] :
    ∀ (a : Mᵃᵒᵖ), ↑(Homeomorph.symm AddOpposite.opHomeomorph) a = AddOpposite.unop a
    source
    def MulOpposite.opHomeomorph {M : Type u_1} [TopologicalSpace M] :
    M ≃ₜ Mᵐᵒᵖ

    MulOpposite.op as a homeomorphism.

    Equations
    Instances For
      source
      theorem AddOpposite.instT2Space.proof_1 {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵃᵒᵖ
      source
      instance AddOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵃᵒᵖ
      Equations
      source
      instance MulOpposite.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵐᵒᵖ
      Equations
      source
      theorem AddOpposite.instDiscreteTopology.proof_1 {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵃᵒᵖ
      source
      instance AddOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵃᵒᵖ
      Equations
      source
      instance MulOpposite.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵐᵒᵖ
      Equations
      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_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_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵃᵒᵖ) :
      Filter.map AddOpposite.unop (nhds x) = nhds (AddOpposite.unop 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.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_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_unop_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap AddOpposite.unop (nhds x) = nhds (AddOpposite.op 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
      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
      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
      theorem AddUnits.inducing_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Inducing ↑(AddUnits.embedProduct M)
      source
      theorem Units.inducing_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Inducing ↑(Units.embedProduct M)
      source
      theorem AddUnits.embedding_embedProduct {M : Type u_1} [TopologicalSpace M] [AddMonoid M] :
      Embedding ↑(AddUnits.embedProduct M)
      source
      theorem Units.embedding_embedProduct {M : Type u_1} [TopologicalSpace M] [Monoid M] :
      Embedding ↑(Units.embedProduct M)
      source
      instance AddUnits.instT2Space {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [T2Space M] :
      T2Space (AddUnits M)
      Equations
      source
      theorem AddUnits.instT2Space.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [T2Space M] :
      T2Space (AddUnits M)
      source
      instance Units.instT2Space {M : Type u_1} [TopologicalSpace M] [Monoid M] [T2Space M] :
      T2Space Mˣ
      Equations
      source
      theorem AddUnits.instDiscreteTopology.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [DiscreteTopology M] :
      DiscreteTopology (AddUnits M)
      source
      instance AddUnits.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [DiscreteTopology M] :
      DiscreteTopology (AddUnits M)
      Equations
      source
      instance Units.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [Monoid M] [DiscreteTopology M] :
      DiscreteTopology Mˣ
      Equations
      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 => ↑(-u)) inst✝
      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 => ↑u⁻¹) inst✝
      source
      theorem AddUnits.embedding_val_mk' {M : Type u_3} [AddMonoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x | 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.

      source
      theorem Units.embedding_val_mk' {M : Type u_3} [Monoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x | 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.

      source
      theorem AddUnits.embedding_val_mk {M : Type u_3} [SubtractionMonoid M] [TopologicalSpace M] (h : ContinuousOn Neg.neg {x | 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.

      source
      theorem Units.embedding_val_mk {M : Type u_3} [DivisionMonoid M] [TopologicalSpace M] (h : ContinuousOn Inv.inv {x | 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.

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