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.

Estimated changes