Documentation

Mathlib.Topology.Algebra.ProperConstSMul

Actions by proper maps #

In this file we define ProperConstSMul M X to be a mixin Prop-value class stating that (c • ·) is a proper map for all c.

Note that this is not the same as a proper action (not yet in Mathlib) which requires (c, x) ↦ (c • x, x) to be a proper map.

We also provide 4 instances:

source
class ProperConstVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [TopologicalSpace X] :
Prop

A mixin typeclass saying that the (c +ᵥ ·) is a proper map for all c.

Note that this is not the same as a proper additive action (not yet in Mathlib).

  • isProperMap_vadd : ∀ (c : M), IsProperMap fun (x : X) => c +ᵥ x

    (c +ᵥ ·) is a proper map.

Instances
    source
    class ProperConstSMul (M : Type u_1) (X : Type u_2) [SMul M X] [TopologicalSpace X] :
    Prop

    A mixin typeclass saying that (c • ·) is a proper map for all c.

    Note that this is not the same as a proper multiplicative action (not yet in Mathlib).

    • isProperMap_smul : ∀ (c : M), IsProperMap fun (x : X) => c • x

      (c • ·) is a proper map.

    Instances
      source
      theorem isProperMap_vadd {M : Type u_1} (c : M) (X : Type u_2) [VAdd M X] [TopologicalSpace X] [h : ProperConstVAdd M X] :
      IsProperMap fun (x : X) => c +ᵥ x

      (c +ᵥ ·) is a proper map.

      source
      theorem isProperMap_smul {M : Type u_1} (c : M) (X : Type u_2) [SMul M X] [TopologicalSpace X] [h : ProperConstSMul M X] :
      IsProperMap fun (x : X) => c • x

      (c • ·) is a proper map.

      source
      theorem IsCompact.preimage_vadd {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [ProperConstVAdd M X] {s : Set X} (hs : IsCompact s) (c : M) :
      IsCompact ((fun (x : X) => c +ᵥ x) ⁻¹' s)

      The preimage of a compact set under (c +ᵥ ·) is a compact set.

      source
      theorem IsCompact.preimage_smul {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace X] [ProperConstSMul M X] {s : Set X} (hs : IsCompact s) (c : M) :
      IsCompact ((fun (x : X) => c • x) ⁻¹' s)

      The preimage of a compact set under (c • ·) is a compact set.

      source
      instance instProperConstVAdd {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [ContinuousConstVAdd M X] [T2Space X] [CompactSpace X] :
      ProperConstVAdd M X
      Equations
      • ⋯ = ⋯
      source
      instance instProperConstSMul {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X] [T2Space X] [CompactSpace X] :
      ProperConstSMul M X
      Equations
      • ⋯ = ⋯
      source
      instance instProperConstVAddToVAddToAddMonoidToSubNegAddMonoid {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace X] [ContinuousConstVAdd G X] :
      ProperConstVAdd G X
      Equations
      • ⋯ = ⋯
      source
      instance instProperConstSMulToSMulToMonoidToDivInvMonoid {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] :
      ProperConstSMul G X
      Equations
      • ⋯ = ⋯
      source
      instance instProperConstSMulProdSmulInstTopologicalSpaceProd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [SMul M X] [TopologicalSpace X] [ProperConstSMul M X] [SMul M Y] [TopologicalSpace Y] [ProperConstSMul M Y] :
      ProperConstSMul M (X × Y)
      Equations
      • ⋯ = ⋯
      source
      instance instProperConstSMulForAllInstSMulTopologicalSpace {M : Type u_1} {ι : Type u_2} {X : ι → Type u_3} [(i : ι) → SMul M (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ProperConstSMul M (X i)] :
      ProperConstSMul M ((i : ι) → X i)
      Equations
      • ⋯ = ⋯