Mathlib.Algebra.GroupWithZero.Action.Basic

Module docstring

{"# Definitions of group actions

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

MulAction M α and its additive version AddAction G P are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classes SMul and VAdd that are defined in Algebra.Group.Defs;
DistribMulAction M A is a typeclass for an action of a multiplicative monoid on an additive monoid such that a • (b + c) = a • b + a • c and a • 0 = 0.

The hierarchy is extended further by Module, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

SMulCommClass M N α and its additive version VAddCommClass M N α;
IsScalarTower M N α and its additive version VAddAssocClass M N α;
IsCentralScalar M α and its additive version IsCentralVAdd M N α.

Notation

a • b is used as notation for SMul.smul a b.
a +ᵥ b is used as notation for VAdd.vadd a b.

Implementation details

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags

group action "}

MulAction.bijective₀ theorem

(ha : a ≠ 0) : Bijective (a • · : α → α)

Full source

protected lemma MulAction.bijective₀ (ha : a ≠ 0) : Bijective (a • · : α → α) :=
  MulAction.bijective <| Units.mk0 a ha

Bijectivity of Nonzero Group Action Elements

Informal description

For any nonzero element $a$ of a group with zero $G_0$ acting on a set $\alpha$, the function $x \mapsto a \cdot x$ from $\alpha$ to $\alpha$ is bijective.

MulAction.injective₀ theorem

(ha : a ≠ 0) : Injective (a • · : α → α)

Full source

protected lemma MulAction.injective₀ (ha : a ≠ 0) : Injective (a • · : α → α) :=
  (MulAction.bijective₀ ha).injective

Injectivity of Nonzero Group Action Elements

Informal description

For any nonzero element $a$ of a group with zero $G_0$ acting on a set $\alpha$, the function $x \mapsto a \cdot x$ from $\alpha$ to $\alpha$ is injective.

MulAction.surjective₀ theorem

(ha : a ≠ 0) : Surjective (a • · : α → α)

Full source

protected lemma MulAction.surjective₀ (ha : a ≠ 0) : Surjective (a • · : α → α) :=
  (MulAction.bijective₀ ha).surjective

Surjectivity of Nonzero Group Action Elements

Informal description

For any nonzero element $a$ of a group with zero $G_0$ acting on a set $\alpha$, the function $x \mapsto a \cdot x$ from $\alpha$ to $\alpha$ is surjective.

DistribMulAction.toAddEquiv definition

[DistribMulAction G A] (x : G) : A ≃+ A

Full source

/-- Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPerm`. -/
@[simps +simpRhs]
def DistribMulAction.toAddEquiv [DistribMulAction G A] (x : G) : A ≃+ A where
  __ := toAddMonoidHom A x
  __ := MulAction.toPermHom G A x

Additive monoid isomorphism induced by a group action

Informal description

For a group $ G $ acting distributively on an additive monoid $ A $, each element $ x \in G $ defines an additive monoid isomorphism $ A \simeq A $. This isomorphism is given by the action of $ x $ on $ A $, i.e., $ a \mapsto x \cdot a $, and preserves both the additive structure and the action properties.

DistribMulAction.toAddAut definition

[DistribMulAction G A] : G →* AddAut A

Full source

/-- Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPermHom`. -/
@[simps]
def DistribMulAction.toAddAut [DistribMulAction G A] : G →* AddAut A where
  toFun := toAddEquiv _
  map_one' := AddEquiv.ext (one_smul _)
  map_mul' _ _ := AddEquiv.ext (mul_smul _ _)

Group homomorphism from group action to additive automorphisms

Informal description

For a group $ G $ acting distributively on an additive monoid $ A $, the function that maps each element $ g \in G $ to the corresponding additive automorphism $ A \simeq A $ (given by $ a \mapsto g \cdot a $) is a group homomorphism from $ G $ to the group of additive automorphisms of $ A $. This homomorphism preserves the group structure, meaning it maps the identity element of $ G $ to the identity automorphism and the product of two elements in $ G $ to the composition of their corresponding automorphisms.

smulMonoidWithZeroHom definition

 [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] :
  M₀ × N₀ →*₀ N₀

Full source

/-- Scalar multiplication as a monoid homomorphism with zero. -/
@[simps]
def smulMonoidWithZeroHom [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀]
    [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] : M₀ × N₀M₀ × N₀ →*₀ N₀ :=
  { smulMonoidHom with map_zero' := smul_zero _ }

Scalar multiplication as a monoid with zero homomorphism

Informal description

Given a monoid with zero $M₀$ and a multiplicative monoid with zero $N₀$ equipped with a multiplicative action of $M₀$ on $N₀$ such that $M₀$ forms a scalar tower over $N₀$ and the actions of $M₀$ and $N₀$ commute, the function $\text{smulMonoidWithZeroHom}$ maps a pair $(m, n) \in M₀ \times N₀$ to the scalar product $m \cdot n \in N₀$. This function is a monoid homomorphism with zero, meaning it preserves the multiplicative identity, the zero element, and the multiplicative operation.

AddAut.applyDistribMulAction instance

[AddMonoid A] : DistribMulAction (AddAut A) A

Full source

/-- The tautological action by `AddAut A` on `A`.

This generalizes `Function.End.applyMulAction`. -/
instance applyDistribMulAction [AddMonoid A] : DistribMulAction (AddAut A) A where
  smul := (· <| ·)
  smul_zero := map_zero
  smul_add := map_add
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Distributive Action of Additive Automorphisms on an Additive Monoid

Informal description

For any additive monoid $A$, the group of additive automorphisms $\text{AddAut}(A)$ acts distributively on $A$ via function application. This means that for any automorphism $f \in \text{AddAut}(A)$ and elements $a, b \in A$, we have $f(a + b) = f(a) + f(b)$ and $f(0) = 0$.

IsUnit.smul_sub_iff_sub_inv_smul theorem

 [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R] [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) :
  IsUnit (r • (1 : R) - a) ↔ IsUnit (1 - r⁻¹ • a)

Full source

lemma IsUnit.smul_sub_iff_sub_inv_smul [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R]
    [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) :
    IsUnitIsUnit (r • (1 : R) - a) ↔ IsUnit (1 - r⁻¹ • a) := by
  rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

Equivalence of Unit Conditions under Group Action: $r \cdot 1 - a$ is a unit $\leftrightarrow$ $1 - r^{-1} \cdot a$ is a unit

Informal description

Let $G$ be a group and $R$ be an additive group with a multiplicative monoid structure, equipped with a distributive multiplicative action of $G$ on $R$ such that $G$ forms a scalar tower over $R$ and the actions of $G$ and $R$ commute. For any $r \in G$ and $a \in R$, the element $r \cdot 1 - a$ is a unit in $R$ if and only if $1 - r^{-1} \cdot a$ is a unit in $R$.