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ᵃᵒᵖ, , 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

Put the same topological space structure on the opposite monoid as on the original space.

Equations

Put the same topological space structure on the opposite monoid as on the original space.

Equations
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

AddOpposite.op as a homeomorphism.

Equations
  • AddOpposite.opHomeomorph = { toEquiv := AddOpposite.opEquiv, continuous_toFun := , continuous_invFun := }
Instances For
    @[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ᵃᵒᵖ), AddOpposite.opHomeomorph.symm a = AddOpposite.unop a
    @[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

    MulOpposite.op as a homeomorphism.

    Equations
    • MulOpposite.opHomeomorph = { toEquiv := MulOpposite.opEquiv, continuous_toFun := , continuous_invFun := }
    Instances For
      Equations
      • =
      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)

      The additive units of a monoid are equipped with a topology, via the embedding into M × M.

      Equations

      The units of a monoid are equipped with a topology, via the embedding into M × M.

      Equations
      Equations
      • =
      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.embedding_val_mk' {M : Type u_3} [AddMonoid M] [TopologicalSpace M] {f : MM} (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 : MM} (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_iff {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [AddMonoid M] [TopologicalSpace X] {f : XAddUnits 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 : XMˣ} :
      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⁻¹