Documentation

Mathlib.GroupTheory.GroupAction.Pointwise

Pointwise actions of equivariant maps #

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] (σ : RS) [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] (σ : RS) [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] (σ : RS) [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] (σ : RS) [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] [MulAction R M] [MulAction S N] {G : Type u_8} [FunLike G R S] [MonoidHomClass G R S] (σ : G) {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] (σ : RS) [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