# Pointwise actions of equivariant maps #

- `image_smul_setₛₗ` : under a `σ`-equivariant map, one has `f '' (c • s) = (σ c) • f '' s`.

- `preimage_smul_setₛₗ'` is a general version of the equality `f ⁻¹' (σ c • s) = c • f⁻¹' s`. It requires that `c` acts surjectively and `σ c` acts injectively and is provided with specific versions:

  - `preimage_smul_setₛₗ_of_isUnit_isUnit` when `c` and `σ c` are units
  - `IsUnit.preimage_smul_setₛₗ` when `σ` belongs to a `MonoidHomClass`and `c` is a unit
  - `MonoidHom.preimage_smul_setₛₗ` when `σ` is a `MonoidHom` and `c` is a unit
  - `Group.preimage_smul_setₛₗ` : when the types of `c` and `σ c` are groups.

- `image_smul_set`, `preimage_smul_set` and `Group.preimage_smul_set` are the variants when `σ` is the identity.

source
@[simp]
theorem image_smul_setₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [SMul M α] [SMul N β] [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : M) (s : Set α) :
⇑f '' (c • s) = σ c • ⇑f '' s
source
@[simp]
theorem image_vadd_setₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [VAdd M α] [VAdd N β] [FunLike F α β] [AddActionSemiHomClass F σ α β] (f : F) (c : M) (s : Set α) :
⇑f '' (c +ᵥ s) = σ c +ᵥ ⇑f '' s
source
theorem Set.MapsTo.smul_setₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [SMul M α] [SMul N β] [FunLike F α β] [MulActionSemiHomClass F σ α β] {f : F} {s : Set α} {t : Set β} (hst : MapsTo (⇑f) s t) (c : M) :
MapsTo (⇑f) (c • s) (σ c • t)
source
theorem Set.MapsTo.vadd_setₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [VAdd M α] [VAdd N β] [FunLike F α β] [AddActionSemiHomClass F σ α β] {f : F} {s : Set α} {t : Set β} (hst : MapsTo (⇑f) s t) (c : M) :
MapsTo (⇑f) (c +ᵥ s) (σ c +ᵥ t)
source
theorem smul_preimage_set_subsetₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [SMul M α] [SMul N β] [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : M) (t : Set β) :
c • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (σ c • t)

Translation of preimage is contained in preimage of translation

source
theorem vadd_preimage_set_subsetₛₗ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [VAdd M α] [VAdd N β] [FunLike F α β] [AddActionSemiHomClass F σ α β] (f : F) (c : M) (t : Set β) :
c +ᵥ ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (σ c +ᵥ t)
source
theorem preimage_smul_setₛₗ' {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [SMul M α] [SMul N β] [FunLike F α β] [MulActionSemiHomClass F σ α β] {f : F} {t : Set β} {c : M} (hc : Function.Surjective fun (m : α) => c • m) (hc' : Function.Injective fun (n : β) => σ c • n) :
⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

General version of `preimage_smul_setₛₗ`. This version assumes that the scalar multiplication by `c` is surjective while the scalar multiplication by `σ c` is injective.

source
theorem preimage_vadd_setₛₗ' {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [VAdd M α] [VAdd N β] [FunLike F α β] [AddActionSemiHomClass F σ α β] {f : F} {t : Set β} {c : M} (hc : Function.Surjective fun (m : α) => c +ᵥ m) (hc' : Function.Injective fun (n : β) => σ c +ᵥ n) :
⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t

General version of `preimage_vadd_setₛₗ`. This version assumes that the vector addition of `c` is surjective while the vector addition of `σ c` is injective.

source
theorem preimage_smul_setₛₗ_of_isUnit_isUnit {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [Monoid M] [Monoid N] [MulAction M α] [MulAction N β] [FunLike F α β] [MulActionSemiHomClass F σ α β] {c : M} (f : F) (hc : IsUnit c) (hc' : IsUnit (σ c)) (t : Set β) :
⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

`preimage_smul_setₛₗ` when both scalars act by unit

source
theorem preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N β] [FunLike F α β] [AddActionSemiHomClass F σ α β] {c : M} (f : F) (hc : IsAddUnit c) (hc' : IsAddUnit (σ c)) (t : Set β) :
⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
source
theorem IsUnit.preimage_smul_setₛₗ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [Monoid M] [Monoid N] [MulAction M α] [MulAction N β] {c : M} {F : Type u_6} {G : Type u_7} [FunLike G M N] [MonoidHomClass G M N] (σ : G) [FunLike F α β] [MulActionSemiHomClass F (⇑σ) α β] (f : F) (hc : IsUnit c) (t : Set β) :
⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

`preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism.

source
theorem IsAddUnit.preimage_vadd_setₛₗ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N β] {c : M} {F : Type u_6} {G : Type u_7} [FunLike G M N] [AddMonoidHomClass G M N] (σ : G) [FunLike F α β] [AddActionSemiHomClass F (⇑σ) α β] (f : F) (hc : IsAddUnit c) (t : Set β) :
⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
source
theorem MonoidHom.preimage_smul_setₛₗ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [Monoid M] [Monoid N] [MulAction M α] [MulAction N β] {c : M} {F : Type u_6} (σ : M →* N) [FunLike F α β] [MulActionSemiHomClass F (⇑σ) α β] (f : F) (hc : IsUnit c) (t : Set β) :
⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

`preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism.

source
theorem AddMonoidHom.preimage_vadd_setₛₗ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N β] {c : M} {F : Type u_6} (σ : M →+ N) [FunLike F α β] [AddActionSemiHomClass F (⇑σ) α β] (f : F) (hc : IsAddUnit c) (t : Set β) :
⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
source
theorem Group.preimage_smul_setₛₗ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group H] (σ : G → H) [MulAction G α] [MulAction H β] {F : Type u_5} [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β) :
⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

`preimage_smul_setₛₗ` in the context of groups

source
theorem AddGroup.preimage_vadd_setₛₗ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup H] (σ : G → H) [AddAction G α] [AddAction H β] {F : Type u_5} [FunLike F α β] [AddActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β) :
⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
source
theorem image_smul_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [SMul M α] [SMul M β] [FunLike F α β] [MulActionHomClass F M α β] (f : F) (c : M) (s : Set α) :
⇑f '' (c • s) = c • ⇑f '' s
source
theorem image_vadd_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [VAdd M α] [VAdd M β] [FunLike F α β] [AddActionHomClass F M α β] (f : F) (c : M) (s : Set α) :
⇑f '' (c +ᵥ s) = c +ᵥ ⇑f '' s
source
theorem smul_preimage_set_subset {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [SMul M α] [SMul M β] [FunLike F α β] [MulActionHomClass F M α β] (f : F) (c : M) (t : Set β) :
c • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (c • t)
source
theorem vadd_preimage_set_subset {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [VAdd M α] [VAdd M β] [FunLike F α β] [AddActionHomClass F M α β] (f : F) (c : M) (t : Set β) :
c +ᵥ ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (c +ᵥ t)
source
theorem Set.MapsTo.smul_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [SMul M α] [SMul M β] [FunLike F α β] [MulActionHomClass F M α β] {f : F} {s : Set α} {t : Set β} (hst : MapsTo (⇑f) s t) (c : M) :
MapsTo (⇑f) (c • s) (c • t)
source
theorem Set.MapsTo.vadd_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [VAdd M α] [VAdd M β] [FunLike F α β] [AddActionHomClass F M α β] {f : F} {s : Set α} {t : Set β} (hst : MapsTo (⇑f) s t) (c : M) :
MapsTo (⇑f) (c +ᵥ s) (c +ᵥ t)
source
theorem IsUnit.preimage_smul_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [Monoid M] [MulAction M α] [MulAction M β] [FunLike F α β] [MulActionHomClass F M α β] (f : F) {c : M} (hc : IsUnit c) (t : Set β) :
⇑f ⁻¹' (c • t) = c • ⇑f ⁻¹' t
source
theorem IsAddUnit.preimage_vadd_set {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [AddMonoid M] [AddAction M α] [AddAction M β] [FunLike F α β] [AddActionHomClass F M α β] (f : F) {c : M} (hc : IsAddUnit c) (t : Set β) :
⇑f ⁻¹' (c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
source
theorem Group.preimage_smul_set {G : Type u_1} [Group G] {α : Type u_2} {β : Type u_3} [MulAction G α] [MulAction G β] {F : Type u_4} [FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β) :
⇑f ⁻¹' (c • t) = c • ⇑f ⁻¹' t
source
theorem AddGroup.preimage_vadd_set {G : Type u_1} [AddGroup G] {α : Type u_2} {β : Type u_3} [AddAction G α] [AddAction G β] {F : Type u_4} [FunLike F α β] [AddActionHomClass F G α β] (f : F) (c : G) (t : Set β) :
⇑f ⁻¹' (c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t