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

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

DomMulAct.instTopologicalSpace = TopologicalSpace.induced (⇑DomMulAct.mk.symm) inst✝

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

DomAddAct.instTopologicalSpace = TopologicalSpace.induced (⇑DomAddAct.mk.symm) inst✝

theorem DomMulAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :

Continuous ⇑mk

theorem DomAddAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :

Continuous ⇑mk

theorem DomMulAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :

Continuous ⇑mk.symm

theorem DomAddAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :

Continuous ⇑mk.symm

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

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

@[simp]

theorem DomMulAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :

mkHomeomorph.toEquiv = mk

@[simp]

theorem DomAddAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :

mkHomeomorph.toEquiv = mk

@[simp]

theorem DomMulAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :

⇑mkHomeomorph = ⇑mk

@[simp]

theorem DomAddAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :

⇑mkHomeomorph = ⇑mk

@[simp]

theorem DomMulAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :

⇑mkHomeomorph.symm = ⇑mk.symm

@[simp]

theorem DomAddAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :

⇑mkHomeomorph.symm = ⇑mk.symm

theorem DomMulAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk

theorem DomAddAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk

theorem DomMulAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk

theorem DomAddAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk

theorem DomMulAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsOpenEmbedding ⇑mk

theorem DomAddAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsOpenEmbedding ⇑mk

theorem DomMulAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsClosedEmbedding ⇑mk

theorem DomAddAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsClosedEmbedding ⇑mk

theorem DomMulAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk

theorem DomAddAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk

@[deprecated DomMulAct.isInducing_mk (since := "2024-10-28")]

theorem DomMulAct.inducing_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk

Alias of DomMulAct.isInducing_mk.

@[deprecated DomMulAct.isEmbedding_mk (since := "2024-10-26")]

theorem DomMulAct.embedding_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk

Alias of DomMulAct.isEmbedding_mk.

@[deprecated DomMulAct.isQuotientMap_mk (since := "2024-10-22")]

theorem DomMulAct.quotientMap_mk {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk

Alias of DomMulAct.isQuotientMap_mk.

theorem DomMulAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk.symm

theorem DomAddAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk.symm

theorem DomMulAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk.symm

theorem DomAddAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk.symm

@[deprecated DomMulAct.isInducing_mk_symm (since := "2024-10-28")]

theorem DomMulAct.inducing_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsInducing ⇑mk.symm

Alias of DomMulAct.isInducing_mk_symm.

@[deprecated DomMulAct.isEmbedding_mk_symm (since := "2024-10-26")]

theorem DomMulAct.embedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsEmbedding ⇑mk.symm

Alias of DomMulAct.isEmbedding_mk_symm.

theorem DomMulAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsOpenEmbedding ⇑mk.symm

theorem DomAddAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsOpenEmbedding ⇑mk.symm

theorem DomMulAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsClosedEmbedding ⇑mk.symm

theorem DomAddAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsClosedEmbedding ⇑mk.symm

theorem DomMulAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk.symm

theorem DomAddAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk.symm

@[deprecated DomMulAct.isQuotientMap_mk_symm (since := "2024-10-22")]

theorem DomMulAct.quotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :

Topology.IsQuotientMap ⇑mk.symm

Alias of DomMulAct.isQuotientMap_mk_symm.

instance DomMulAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :

T0Space Mᵈᵐᵃ

instance DomAddAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :

T0Space Mᵈᵃᵃ

instance DomMulAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :

T1Space Mᵈᵐᵃ

instance DomAddAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :

T1Space Mᵈᵃᵃ

instance DomMulAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :

T2Space Mᵈᵐᵃ

instance DomAddAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :

T2Space Mᵈᵃᵃ

instance DomMulAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :

T25Space Mᵈᵐᵃ

instance DomAddAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :

T25Space Mᵈᵃᵃ

instance DomMulAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :

T3Space Mᵈᵐᵃ

instance DomAddAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :

T3Space Mᵈᵃᵃ

instance DomMulAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :

T4Space Mᵈᵐᵃ

instance DomAddAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :

T4Space Mᵈᵃᵃ

instance DomMulAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :

T5Space Mᵈᵐᵃ

instance DomAddAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :

T5Space Mᵈᵃᵃ

instance DomMulAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :

R0Space Mᵈᵐᵃ

instance DomAddAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :

R0Space Mᵈᵃᵃ

instance DomMulAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :

R1Space Mᵈᵐᵃ

instance DomAddAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :

R1Space Mᵈᵃᵃ

instance DomMulAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :

RegularSpace Mᵈᵐᵃ

instance DomAddAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :

RegularSpace Mᵈᵃᵃ

instance DomMulAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :

NormalSpace Mᵈᵐᵃ

instance DomAddAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :

NormalSpace Mᵈᵃᵃ

instance DomMulAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :

CompletelyNormalSpace Mᵈᵐᵃ

instance DomAddAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :

CompletelyNormalSpace Mᵈᵃᵃ

instance DomMulAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :

DiscreteTopology Mᵈᵐᵃ

instance DomAddAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :

DiscreteTopology Mᵈᵃᵃ

instance DomMulAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :

TopologicalSpace.SeparableSpace Mᵈᵐᵃ

instance DomAddAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :

TopologicalSpace.SeparableSpace Mᵈᵃᵃ

instance DomMulAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :

FirstCountableTopology Mᵈᵐᵃ

instance DomAddAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :

FirstCountableTopology Mᵈᵃᵃ

instance DomMulAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :

SecondCountableTopology Mᵈᵐᵃ

instance DomAddAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :

SecondCountableTopology Mᵈᵃᵃ

instance DomMulAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :

CompactSpace Mᵈᵐᵃ

instance DomAddAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :

CompactSpace Mᵈᵃᵃ

instance DomMulAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :

LocallyCompactSpace Mᵈᵐᵃ

instance DomAddAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :

LocallyCompactSpace Mᵈᵃᵃ

instance DomMulAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :

WeaklyLocallyCompactSpace Mᵈᵐᵃ

instance DomAddAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :

WeaklyLocallyCompactSpace Mᵈᵃᵃ

@[simp]

theorem DomMulAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.map (⇑mk) (nhds x) = nhds (mk x)

@[simp]

theorem DomAddAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.map (⇑mk) (nhds x) = nhds (mk x)

@[simp]

theorem DomMulAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :

Filter.map (⇑mk.symm) (nhds x) = nhds (mk.symm x)

@[simp]

theorem DomAddAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :

Filter.map (⇑mk.symm) (nhds x) = nhds (mk.symm x)

@[simp]

theorem DomMulAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :

Filter.comap (⇑mk) (nhds x) = nhds (mk.symm x)

@[simp]

theorem DomAddAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :

Filter.comap (⇑mk) (nhds x) = nhds (mk.symm x)

@[simp]

theorem DomMulAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.comap (⇑mk.symm) (nhds x) = nhds (mk x)

@[simp]

theorem DomAddAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :

Filter.comap (⇑mk.symm) (nhds x) = nhds (mk x)