Pointwise actions of equivariant maps #
image_smul_setₛₗ: under aσ-equivariant map, one hasf '' (c • s) = (σ c) • f '' s.preimage_smul_setₛₗ'is a general version of the equalityf ⁻¹' (σ c • s) = c • f⁻¹' s. It requires thatcacts surjectively andσ cacts injectively and is provided with specific versions:preimage_smul_setₛₗ_of_isUnit_isUnitwhencandσ care unitsIsUnit.preimage_smul_setₛₗwhenσbelongs to aMonoidHomClassandcis a unitMonoidHom.preimage_smul_setₛₗwhenσis aMonoidHomandcis a unitGroup.preimage_smul_setₛₗ: when the types ofcandσ care groups.
image_smul_set,preimage_smul_setandGroup.preimage_smul_setare the variants whenσis the identity.
@[deprecated vadd_preimage_set_subsetₛₗ (since := "2025-03-03")]
theorem
vadd_preimage_set_leₛₗ
{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 β)
:
Alias of vadd_preimage_set_subsetₛₗ.
@[deprecated smul_preimage_set_subsetₛₗ (since := "2025-03-03")]
theorem
smul_preimage_set_leₛₗ
{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 β)
:
Alias of smul_preimage_set_subsetₛₗ.
Translation of preimage is contained in preimage of translation
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)
:
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.
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)
:
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ₛₗ_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 β)
:
preimage_smul_setₛₗ when both scalars act by unit
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 β)
:
@[deprecated preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit (since := "2025-03-04")]
theorem
preimage_vadd_setₛₗ_of_addUnits
{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 β)
:
@[deprecated preimage_smul_setₛₗ_of_isUnit_isUnit (since := "2025-03-04")]
theorem
preimage_smul_setₛₗ_of_units
{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 β)
:
Alias of preimage_smul_setₛₗ_of_isUnit_isUnit.
preimage_smul_setₛₗ when both scalars act by unit
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 β)
:
preimage_smul_setₛₗ when c is a unit and σ is a monoid homomorphism.
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 β)
:
@[deprecated IsAddUnit.preimage_vadd_setₛₗ (since := "2025-03-04")]
theorem
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 β)
:
Alias of IsAddUnit.preimage_vadd_setₛₗ.
@[deprecated IsUnit.preimage_smul_setₛₗ (since := "2025-03-04")]
theorem
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 β)
:
Alias of IsUnit.preimage_smul_setₛₗ.
preimage_smul_setₛₗ when c is a unit and σ is a monoid homomorphism.
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 β)
:
preimage_smul_setₛₗ when c is a unit and σ is a monoid homomorphism.
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 β)
:
preimage_smul_setₛₗ in the context of groups
@[deprecated vadd_preimage_set_subset (since := "2025-03-04")]
theorem
vadd_preimage_set_le
{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 β)
:
Alias of vadd_preimage_set_subset.
@[deprecated smul_preimage_set_subset (since := "2025-03-04")]
theorem
smul_preimage_set_le
{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 β)
:
Alias of smul_preimage_set_subset.
@[deprecated IsAddUnit.preimage_vadd_set (since := "2025-03-04")]
theorem
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 β)
:
Alias of IsAddUnit.preimage_vadd_set.
@[deprecated IsUnit.preimage_smul_set (since := "2025-03-04")]
theorem
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 β)
:
Alias of IsUnit.preimage_smul_set.