doc-next-gen

Mathlib.GroupTheory.GroupAction.Pointwise

Module docstring

{"# 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 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.

"}

image_smul_setₛₗ theorem
(f : F) (c : M) (s : Set α) : f '' (c • s) = σ c • f '' s
Full source 
@[to_additive (attr := simp)]
theorem image_smul_setₛₗ (f : F) (c : M) (s : Set α) :
    f '' (c • s) = σ c • f '' s :=
  Semiconj.set_image (map_smulₛₗ f c) s
Image of Scaled Set under $\sigma$-Equivariant Map
Informal description
Let $F$ be a type of $\sigma$-equivariant maps between sets $X$ and $Y$ with actions of monoids $M$ and $N$ respectively, where $\sigma \colon M \to N$ is a homomorphism. For any $f \in F$, $c \in M$, and subset $s \subseteq X$, the image of the scaled set $c \cdot s$ under $f$ equals the scaled image of $s$ under $\sigma(c)$, i.e., \[ f(c \cdot s) = \sigma(c) \cdot f(s). \]
Set.MapsTo.smul_setₛₗ theorem
(hst : MapsTo f s t) (c : M) : MapsTo f (c • s) (σ c • t)
Full source 
@[to_additive]
theorem Set.MapsTo.smul_setₛₗ (hst : MapsTo f s t) (c : M) : MapsTo f (c • s) (σ c • t) :=
  Function.Semiconj.mapsTo_image_right (map_smulₛₗ _ _) hst
$\sigma$-Equivariant Map Preserves Scaled Subset Inclusion
Informal description
Let $F$ be a type of $\sigma$-equivariant maps between sets $X$ and $Y$ with actions of monoids $M$ and $N$ respectively, where $\sigma \colon M \to N$ is a homomorphism. Given a map $f \in F$ such that $f$ maps a subset $s \subseteq X$ into a subset $t \subseteq Y$ (i.e., $f(s) \subseteq t$), then for any $c \in M$, $f$ maps the scaled set $c \cdot s$ into the scaled set $\sigma(c) \cdot t$, i.e., \[ f(c \cdot s) \subseteq \sigma(c) \cdot t. \]
smul_preimage_set_subsetₛₗ theorem
(f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (σ c • t)
Full source 
/-- Translation of preimage is contained in preimage of translation -/
@[to_additive]
theorem smul_preimage_set_subsetₛₗ (f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (σ c • t) :=
  ((mapsTo_preimage f t).smul_setₛₗ c).subset_preimage
Inclusion of Scaled Preimage in Preimage of Scaled Set under $\sigma$-Equivariant Map
Informal description
Let $F$ be a type of $\sigma$-equivariant maps between sets $X$ and $Y$ with actions of monoids $M$ and $N$ respectively, where $\sigma \colon M \to N$ is a homomorphism. For any $f \in F$, $c \in M$, and subset $t \subseteq Y$, the scaled preimage of $t$ under $f$ is contained in the preimage of the scaled set $\sigma(c) \cdot t$ under $f$, i.e., \[ c \cdot f^{-1}(t) \subseteq f^{-1}(\sigma(c) \cdot t). \]
preimage_smul_setₛₗ' theorem
{c : M} (hc : Function.Surjective (fun (m : α) ↦ c • m)) (hc' : Function.Injective (fun (n : β) ↦ σ c • n)) : f ⁻¹' (σ c • t) = c • f ⁻¹' t
Full source 
/-- 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. -/
@[to_additive "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."]
theorem preimage_smul_setₛₗ' {c : M}
    (hc : Function.Surjective (fun (m : α) ↦ c • m))
    (hc' : Function.Injective (fun (n : β) ↦ σ c • n)) :
    f ⁻¹' (σ c • t) = c • f ⁻¹' t := by
  refine Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)
  rw [subset_def, hc.forall]
  rintro x ⟨y, hy, hxy⟩
  rw [map_smulₛₗ, hc'.eq_iff] at hxy
  subst y
  exact smul_mem_smul_set hy
Preimage of Scaled Set under $\sigma$-Equivariant Map Equals Scaled Preimage
Informal description
Let $M$ and $N$ be monoids acting on sets $\alpha$ and $\beta$ respectively, and let $\sigma \colon M \to N$ be a homomorphism. Let $f \colon \alpha \to \beta$ be a $\sigma$-equivariant map (i.e., $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in M$ and $x \in \alpha$). For any $c \in M$ such that the scalar multiplication by $c$ is surjective on $\alpha$ and the scalar multiplication by $\sigma(c)$ is injective on $\beta$, the preimage of the scaled set $\sigma(c) \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t). \]
preimage_smul_setₛₗ_of_isUnit_isUnit theorem
(f : F) (hc : IsUnit c) (hc' : IsUnit (σ c)) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t
Full source 
/-- `preimage_smul_setₛₗ` when both scalars act by unit -/
@[to_additive]
theorem preimage_smul_setₛₗ_of_isUnit_isUnit (f : F)
    (hc : IsUnit c) (hc' : IsUnit (σ c)) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ' hc.smul_bijective.surjective hc'.smul_bijective.injective
Preimage of Scaled Set under $\sigma$-Equivariant Map Equals Scaled Preimage for Units
Informal description
Let $M$ and $N$ be monoids acting on sets $\alpha$ and $\beta$ respectively, and let $\sigma \colon M \to N$ be a homomorphism. Let $f \colon \alpha \to \beta$ be a $\sigma$-equivariant map (i.e., $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in M$ and $x \in \alpha$). For any $c \in M$ and $\sigma(c) \in N$ that are both units, the preimage of the scaled set $\sigma(c) \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t). \]
IsUnit.preimage_smul_setₛₗ theorem
{F G : Type*} [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
Full source 
/-- `preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism. -/
@[to_additive]
theorem IsUnit.preimage_smul_setₛₗ {F G : Type*} [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ₛₗ_of_isUnit_isUnit _ hc (hc.map _) _
Preimage of Scaled Set under $\sigma$-Equivariant Map Equals Scaled Preimage for Units
Informal description
Let $M$ and $N$ be monoids acting on sets $\alpha$ and $\beta$ respectively, and let $\sigma \colon M \to N$ be a monoid homomorphism. Let $f \colon \alpha \to \beta$ be a $\sigma$-equivariant map (i.e., $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in M$ and $x \in \alpha$). For any unit $c \in M$, the preimage of the scaled set $\sigma(c) \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t). \]
MonoidHom.preimage_smul_setₛₗ theorem
{F : Type*} (σ : M →* N) [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (hc : IsUnit c) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t
Full source 
/-- `preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism. -/
@[to_additive]
protected theorem MonoidHom.preimage_smul_setₛₗ {F : Type*} (σ : M →* N) [FunLike F α β]
    [MulActionSemiHomClass F σ α β] (f : F) (hc : IsUnit c) (t : Set β) :
    f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  hc.preimage_smul_setₛₗ σ f t
Preimage of Scaled Set under Monoid Homomorphism Equivariant Map Equals Scaled Preimage for Units
Informal description
Let $M$ and $N$ be monoids acting on sets $\alpha$ and $\beta$ respectively, and let $\sigma \colon M \to N$ be a monoid homomorphism. Let $f \colon \alpha \to \beta$ be a $\sigma$-equivariant map (i.e., $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in M$ and $x \in \alpha$). For any unit $c \in M$ and subset $t \subseteq \beta$, the preimage of the scaled set $\sigma(c) \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t). \]
Group.preimage_smul_setₛₗ theorem
{G H α β : Type*} [Group G] [Group H] (σ : G → H) [MulAction G α] [MulAction H β] {F : Type*} [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t
Full source 
/-- `preimage_smul_setₛₗ` in the context of groups -/
@[to_additive]
theorem Group.preimage_smul_setₛₗ {G H α β : Type*} [Group G] [Group H] (σ : G → H)
    [MulAction G α] [MulAction H β]
    {F : Type*} [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β) :
    f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ_of_isUnit_isUnit _ (Group.isUnit _) (Group.isUnit _) _
Preimage of Scaled Set under Group Equivariant Map Equals Scaled Preimage
Informal description
Let $G$ and $H$ be groups acting on sets $\alpha$ and $\beta$ respectively, and let $\sigma \colon G \to H$ be a group homomorphism. Let $f \colon \alpha \to \beta$ be a $\sigma$-equivariant map (i.e., $f(g \cdot x) = \sigma(g) \cdot f(x)$ for all $g \in G$ and $x \in \alpha$). Then for any $c \in G$ and subset $t \subseteq \beta$, the preimage of the scaled set $\sigma(c) \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t). \]
image_smul_set theorem
(f : F) (c : M) (s : Set α) : f '' (c • s) = c • f '' s
Full source 
@[to_additive]
theorem image_smul_set (f : F) (c : M) (s : Set α) : f '' (c • s) = c • f '' s :=
  image_smul_setₛₗ f c s
Image of Scaled Set under Equivariant Map
Informal description
Let $F$ be a type of equivariant maps between sets $\alpha$ and $\beta$ with actions of a monoid $M$. For any $f \in F$, $c \in M$, and subset $s \subseteq \alpha$, the image of the scaled set $c \cdot s$ under $f$ equals the scaled image of $s$ under $c$, i.e., \[ f(c \cdot s) = c \cdot f(s). \]
smul_preimage_set_subset theorem
(f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (c • t)
Full source 
@[to_additive]
theorem smul_preimage_set_subset (f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (c • t) :=
  smul_preimage_set_subsetₛₗ f c t
Inclusion of Scaled Preimage in Preimage of Scaled Set under Equivariant Map
Informal description
Let $F$ be a type of equivariant maps between sets $\alpha$ and $\beta$ with actions of a monoid $M$. For any map $f \in F$, scalar $c \in M$, and subset $t \subseteq \beta$, the scaled preimage of $t$ under $f$ is contained in the preimage of the scaled set $c \cdot t$ under $f$, i.e., \[ c \cdot f^{-1}(t) \subseteq f^{-1}(c \cdot t). \]
Set.MapsTo.smul_set theorem
{f : F} {s : Set α} {t : Set β} (hst : MapsTo f s t) (c : M) : MapsTo f (c • s) (c • t)
Full source 
@[to_additive]
theorem Set.MapsTo.smul_set {f : F} {s : Set α} {t : Set β} (hst : MapsTo f s t) (c : M) :
    MapsTo f (c • s) (c • t) :=
  hst.smul_setₛₗ c
Equivariant Map Preserves Scaled Subset Inclusion
Informal description
Let $F$ be a type of equivariant maps between sets $\alpha$ and $\beta$ with actions of a monoid $M$. For any map $f \in F$ such that $f$ maps a subset $s \subseteq \alpha$ into a subset $t \subseteq \beta$ (i.e., $f(s) \subseteq t$), and for any $c \in M$, the map $f$ also maps the scaled set $c \cdot s$ into the scaled set $c \cdot t$, i.e., \[ f(c \cdot s) \subseteq c \cdot t. \]
IsUnit.preimage_smul_set theorem
{M α β F : Type*} [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
Full source 
@[to_additive]
theorem IsUnit.preimage_smul_set {M α β F : Type*} [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 :=
  preimage_smul_setₛₗ_of_isUnit_isUnit f hc hc t
Preimage of Scaled Set under Equivariant Map Equals Scaled Preimage for Units
Informal description
Let $M$ be a monoid acting on sets $\alpha$ and $\beta$, and let $F$ be a type of $M$-equivariant maps from $\alpha$ to $\beta$. For any map $f \in F$ and any unit $c \in M$, the preimage of the scaled set $c \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(c \cdot t) = c \cdot f^{-1}(t). \]
Group.preimage_smul_set theorem
{G : Type*} [Group G] {α β : Type*} [MulAction G α] [MulAction G β] {F : Type*} [FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β) : f ⁻¹' (c • t) = c • f ⁻¹' t
Full source 
@[to_additive]
theorem Group.preimage_smul_set {G : Type*} [Group G] {α β : Type*} [MulAction G α] [MulAction G β]
    {F : Type*} [FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β) :
    f ⁻¹' (c • t) = c • f ⁻¹' t :=
  (Group.isUnit c).preimage_smul_set f t
Preimage of Scaled Set under Group Equivariant Map Equals Scaled Preimage
Informal description
Let $G$ be a group acting on sets $\alpha$ and $\beta$, and let $F$ be a type of $G$-equivariant maps from $\alpha$ to $\beta$. For any map $f \in F$ and any element $c \in G$, the preimage of the scaled set $c \cdot t$ under $f$ equals the scaled preimage of $t$ under $f$, i.e., \[ f^{-1}(c \cdot t) = c \cdot f^{-1}(t). \]