Pointwise actions of equivariant maps

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

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

  • preimage_smul_setₛₗ_of_units when c and σ c are units
  • preimage_smul_setₛₗ when σ belongs to a MonoidHomClassand 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.

theorem MulAction.smul_bijective_of_is_unit {M : Type u_1} [Monoid M] {α : Type u_2} [MulAction M α] {m : M} (hm : IsUnit m) : Function.Bijective fun (a : α) => m • a

theorem image_smul_setₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] (σ : R → S) [MulAction R M] [MulAction S N] {F : Type u_7} (h : F) [FunLike F M N] [MulActionSemiHomClass F σ M N] (c : R) (s : Set M) : ⇑h '' (c • s) = σ c • ⇑h '' s

theorem smul_preimage_set_leₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] (σ : R → S) [MulAction R M] [MulAction S N] {F : Type u_7} (h : F) [FunLike F M N] [MulActionSemiHomClass F σ M N] (c : R) (t : Set N) : c • ⇑h ⁻¹' t ⊆ ⇑h ⁻¹' (σ c • t)

Translation of preimage is contained in preimage of translation

theorem preimage_smul_setₛₗ' {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] (σ : R → S) [MulAction R M] [MulAction S N] {F : Type u_7} (h : F) [FunLike F M N] [MulActionSemiHomClass F σ M N] {c : R} (t : Set N) (hc : Function.Surjective fun (m : M) => c • m) (hc' : Function.Injective fun (n : N) => σ c • n) : ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

General version of preimage_smul_setₛₗ

theorem preimage_smul_setₛₗ_of_units {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] (σ : R → S) [MulAction R M] [MulAction S N] {F : Type u_7} (h : F) [FunLike F M N] [MulActionSemiHomClass F σ M N] {c : R} (t : Set N) (hc : IsUnit c) (hc' : IsUnit (σ c)) : ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

preimage_smul_setₛₗ when both scalars act by unit

theorem MonoidHom.preimage_smul_setₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] [MulAction R M] [MulAction S N] (σ : R →* S) {F : Type u_8} [FunLike F M N] [MulActionSemiHomClass F (⇑σ) M N] (h : F) {c : R} (hc : IsUnit c) (t : Set N) : ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

preimage_smul_setₛₗ in the context of a MonoidHom

theorem preimage_smul_setₛₗ {R : Type u_1} {S : Type u_2} (M : Type u_3) (N : Type u_6) [Monoid R] [Monoid S] {G : Type u_8} [FunLike G R S] [MonoidHomClass G R S] (σ : G) [MulAction R M] [MulAction S N] {F : Type u_9} [FunLike F M N] [MulActionSemiHomClass F (⇑σ) M N] (h : F) {c : R} (hc : IsUnit c) (t : Set N) : ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

preimage_smul_setₛₗ in the context of a MonoidHomClass

theorem Group.preimage_smul_setₛₗ (M : Type u_3) (N : Type u_6) {R : Type u_8} {S : Type u_9} [Group R] [Group S] (σ : R → S) [MulAction R M] [MulAction S N] {F : Type u_10} [FunLike F M N] [MulActionSemiHomClass F σ M N] (h : F) (c : R) (t : Set N) : ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

preimage_smul_setₛₗ in the context of a groups

@[simp]

theorem image_smul_set (R : Type u_1) (M₁ : Type u_4) (M₂ : Type u_5) [Monoid R] [MulAction R M₁] [MulAction R M₂] {F : Type u_7} (h : F) [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (c : R) (s : Set M₁) : ⇑h '' (c • s) = c • ⇑h '' s

theorem smul_preimage_set_le (R : Type u_1) (M₁ : Type u_4) (M₂ : Type u_5) [Monoid R] [MulAction R M₁] [MulAction R M₂] {F : Type u_7} (h : F) [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (c : R) (t : Set M₂) : c • ⇑h ⁻¹' t ⊆ ⇑h ⁻¹' (c • t)

theorem preimage_smul_set (R : Type u_1) (M₁ : Type u_4) (M₂ : Type u_5) [Monoid R] [MulAction R M₁] [MulAction R M₂] {F : Type u_7} (h : F) [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] {c : R} (t : Set M₂) (hc : IsUnit c) : ⇑h ⁻¹' (c • t) = c • ⇑h ⁻¹' t

theorem Group.preimage_smul_set {R : Type u_8} [Group R] (M₁ : Type u_9) (M₂ : Type u_10) [MulAction R M₁] [MulAction R M₂] {F : Type u_11} [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (h : F) (c : R) (t : Set M₂) : ⇑h ⁻¹' (c • t) = c • ⇑h ⁻¹' t