Documentation

Mathlib.Topology.Algebra.Constructions.DomMulAct

Topological space structure on Mᵈᵐᵃ and Mᵈᵃᵃ #

In this file we define TopologicalSpace structure on Mᵈᵐᵃ and Mᵈᵃᵃ and prove basic theorems about these topologies. The topologies on Mᵈᵐᵃ and Mᵈᵃᵃ are the same as the topology on M. Formally, they are induced by DomMulAct.mk.symm and DomAddAct.mk.symm, since the types aren't definitionally equal.

Tags #

topological space, group action, domain action

source
instance DomMulAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
TopologicalSpace Mᵈᵐᵃ

Put the same topological space structure on Mᵈᵐᵃ as on the original space.

Equations
source
instance DomAddAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
TopologicalSpace Mᵈᵃᵃ

Put the same topological space structure on Mᵈᵃᵃ as on the original space.

Equations
source
theorem DomMulAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomMulAct.mk
source
theorem DomAddAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomAddAct.mk
source
theorem DomMulAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomMulAct.mk.symm
source
theorem DomAddAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomAddAct.mk.symm
source
def DomMulAct.mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
M ≃ₜ Mᵈᵐᵃ

DomMulAct.mk as a homeomorphism.

Equations
  • DomMulAct.mkHomeomorph = { toEquiv := DomMulAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
    source
    def DomAddAct.mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
    M ≃ₜ Mᵈᵃᵃ

    DomAddAct.mk as a homeomorphism.

    Equations
    • DomAddAct.mkHomeomorph = { toEquiv := DomAddAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
    Instances For
      source
      @[simp]
      theorem DomMulAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
      DomMulAct.mkHomeomorph.toEquiv = DomMulAct.mk
      source
      @[simp]
      theorem DomAddAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
      DomAddAct.mkHomeomorph.toEquiv = DomAddAct.mk
      source
      @[simp]
      theorem DomMulAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
      ⇑DomMulAct.mkHomeomorph = ⇑DomMulAct.mk
      source
      @[simp]
      theorem DomAddAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
      ⇑DomAddAct.mkHomeomorph = ⇑DomAddAct.mk
      source
      @[simp]
      theorem DomMulAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
      ⇑DomMulAct.mkHomeomorph.symm = ⇑DomMulAct.mk.symm
      source
      @[simp]
      theorem DomAddAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
      ⇑DomAddAct.mkHomeomorph.symm = ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomMulAct.mk
      source
      theorem DomAddAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomAddAct.mk
      source
      theorem DomMulAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsOpenEmbedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsOpenEmbedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomMulAct.mk
      source
      theorem DomAddAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomAddAct.mk
      source
      @[deprecated DomMulAct.isInducing_mk]
      theorem DomMulAct.inducing_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomMulAct.mk

      Alias of DomMulAct.isInducing_mk.

      source
      @[deprecated DomMulAct.isEmbedding_mk]
      theorem DomMulAct.embedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomMulAct.mk

      Alias of DomMulAct.isEmbedding_mk.

      source
      @[deprecated DomMulAct.isQuotientMap_mk]
      theorem DomMulAct.quotientMap_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomMulAct.mk

      Alias of DomMulAct.isQuotientMap_mk.

      source
      @[deprecated DomMulAct.isClosedEmbedding_mk]
      theorem DomMulAct.closedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomMulAct.mk

      Alias of DomMulAct.isClosedEmbedding_mk.

      source
      @[deprecated DomMulAct.isOpenEmbedding_mk]
      theorem DomMulAct.openEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      Topology.IsOpenEmbedding ⇑DomMulAct.mk

      Alias of DomMulAct.isOpenEmbedding_mk.

      source
      theorem DomMulAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomAddAct.mk.symm
      source
      @[deprecated DomMulAct.isInducing_mk_symm]
      theorem DomMulAct.inducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsInducing ⇑DomMulAct.mk.symm

      Alias of DomMulAct.isInducing_mk_symm.

      source
      @[deprecated DomMulAct.isEmbedding_mk_symm]
      theorem DomMulAct.embedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsEmbedding ⇑DomMulAct.mk.symm

      Alias of DomMulAct.isEmbedding_mk_symm.

      source
      theorem DomMulAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsOpenEmbedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsOpenEmbedding ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomAddAct.mk.symm
      source
      @[deprecated DomMulAct.isClosedEmbedding_mk_symm]
      theorem DomMulAct.closedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsClosedEmbedding ⇑DomMulAct.mk.symm

      Alias of DomMulAct.isClosedEmbedding_mk_symm.

      source
      theorem DomMulAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomAddAct.mk.symm
      source
      @[deprecated DomMulAct.isQuotientMap_mk_symm]
      theorem DomMulAct.quotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Topology.IsQuotientMap ⇑DomMulAct.mk.symm

      Alias of DomMulAct.isQuotientMap_mk_symm.

      source
      instance DomMulAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
      T0Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
      T0Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
      T1Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
      T1Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
      T25Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
      T25Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
      T3Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
      T3Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
      T4Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
      T4Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
      T5Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
      T5Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
      R0Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
      R0Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
      R1Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
      R1Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
      RegularSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
      RegularSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
      NormalSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
      NormalSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
      CompletelyNormalSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
      CompletelyNormalSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
      TopologicalSpace.SeparableSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
      TopologicalSpace.SeparableSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
      FirstCountableTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
      FirstCountableTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
      SecondCountableTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
      SecondCountableTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :
      CompactSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :
      CompactSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :
      LocallyCompactSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :
      LocallyCompactSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :
      WeaklyLocallyCompactSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :
      WeaklyLocallyCompactSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem DomMulAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk x)
      source
      @[simp]
      theorem DomAddAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk x)
      source
      @[simp]
      theorem DomMulAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
      Filter.map (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk.symm x)
      source
      @[simp]
      theorem DomAddAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
      Filter.map (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk.symm x)
      source
      @[simp]
      theorem DomMulAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
      Filter.comap (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk.symm x)
      source
      @[simp]
      theorem DomAddAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
      Filter.comap (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk.symm x)
      source
      @[simp]
      theorem DomMulAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk x)
      source
      @[simp]
      theorem DomAddAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk x)