Commit 2024-04-13 12:00 7a71e528

View on Github →

Feat (GroupTheory/GroupAction/Hom/Pointwise) : generalize smul set lemmas to group actions (#12023) This is a generalization of Mathlib/Algebra/Module/LinearMap/Pointwise.lean from LinearMapClass to MulActionHomClass. The preexisting lemmas are generalized.

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. It is provided with specific versions:
preimage_smul_setₛₗ_of_units requires that c and σ c are units
MonoidHom.preimage_smul_setₛₗ requires that σ is a MonoidHom and c is a unit
MonoidHomClass.preimage_smul_setₛₗ requires that σ belongs to a MonoidHomClassand that c is a unit
Group.preimage_smul_setₛₗ requires that 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.