Mathlib.Algebra.Group.Action.Hom

Function.Surjective.mulActionLeft abbrev

 {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Surjective f)
  (hsmul : ∀ (c) (x : M), f c • x = c • x) : MulAction S M

Full source

/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.

See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
-/
@[to_additive
"Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`."]
abbrev Function.Surjective.mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S]
    [SMul S M] (f : R →* S) (hf : Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) :
    MulAction S M where
  smul := (· • ·)
  one_smul b := by rw [← f.map_one, hsmul, one_smul]
  mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]

Pushforward of Monoid Action Along Surjective Homomorphism

Informal description

Let $R$ and $S$ be monoids, and $M$ be a type with a multiplicative action of $R$ (i.e., $[MulAction R M]$). Given a surjective monoid homomorphism $f \colon R \to S$ and a scalar multiplication operation $\bullet \colon S \times M \to M$ such that for all $c \in R$ and $x \in M$, we have $f(c) \bullet x = c \bullet x$, then $M$ inherits a multiplicative action of $S$ via $f$.

MulAction.compHom abbrev

[Monoid N] (g : N →* M) : MulAction N α

Full source

/-- A multiplicative action of `M` on `α` and a monoid homomorphism `N → M` induce
a multiplicative action of `N` on `α`.

See note [reducible non-instances]. -/
@[to_additive]
abbrev compHom [Monoid N] (g : N →* M) : MulAction N α where
  smul := SMul.comp.smul g
  one_smul _ := by simpa [(· • ·)] using MulAction.one_smul ..
  mul_smul _ _ _ := by simpa [(· • ·)] using MulAction.mul_smul ..

Induced Multiplicative Action via Monoid Homomorphism

Informal description

Given a monoid $N$ and a monoid homomorphism $g \colon N \to M$, the multiplicative action of $M$ on $\alpha$ induces a multiplicative action of $N$ on $\alpha$ via composition with $g$. Specifically, for $n \in N$ and $a \in \alpha$, the action is defined by $n \bullet a = g(n) \bullet a$.

MulAction.compHom_smul_def theorem

 {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
  letI : MulAction E G := MulAction.compHom _ f
  a • x = (f a) • x

Full source

@[to_additive]
lemma compHom_smul_def
    {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
    letI : MulAction E G := MulAction.compHom _ f
    a • x = (f a) • x := rfl

Definition of Induced Action via Homomorphism: $a \cdot x = f(a) \cdot x$

Informal description

Let $E$ and $F$ be monoids, and let $G$ be a type with a multiplicative action of $F$. Given a monoid homomorphism $f \colon E \to F$, the induced action of $E$ on $G$ via $f$ satisfies $a \cdot x = f(a) \cdot x$ for all $a \in E$ and $x \in G$.

MulAction.isPretransitive_compHom theorem

 {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] [IsPretransitive F G] {f : E →* F} (hf : Surjective f) :
  letI : MulAction E G := MulAction.compHom _ f
  IsPretransitive E G

Full source

/-- If an action is transitive, then composing this action with a surjective homomorphism gives
again a transitive action. -/
@[to_additive]
lemma isPretransitive_compHom {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G]
    [IsPretransitive F G] {f : E →* F} (hf : Surjective f) :
    letI : MulAction E G := MulAction.compHom _ f
    IsPretransitive E G := by
  let _ : MulAction E G := MulAction.compHom _ f
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
  obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
  exact ⟨e, rfl⟩

Transitivity of Induced Group Action via Surjective Homomorphism

Informal description

Let $E$ and $F$ be monoids, and let $G$ be a type with a multiplicative action of $F$. Suppose the action of $F$ on $G$ is pretransitive (i.e., for any $x, y \in G$, there exists $f \in F$ such that $f \cdot x = y$). Given a surjective monoid homomorphism $f \colon E \to F$, the induced action of $E$ on $G$ via $f$ is also pretransitive. More precisely, for the induced action defined by $e \cdot x = f(e) \cdot x$ (for $e \in E$ and $x \in G$), the action of $E$ on $G$ is pretransitive.

MulAction.IsPretransitive.of_compHom theorem

 {M N α : Type*} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N)
  [h :
    letI := compHom α f;
    IsPretransitive M α] :
  IsPretransitive N α

Full source

@[to_additive]
lemma IsPretransitive.of_compHom {M N α : Type*} [Monoid M] [Monoid N] [MulAction N α]
    (f : M →* N) [h : letI := compHom α f; IsPretransitive M α] : IsPretransitive N α :=
  letI := compHom α f; h.of_smul_eq f rfl

Pretransitivity of Group Action via Induced Homomorphism

Informal description

Let $M$ and $N$ be monoids with a monoid homomorphism $f \colon M \to N$, and let $\alpha$ be a type with a multiplicative action of $N$. If the induced action of $M$ on $\alpha$ via $f$ is pretransitive (i.e., for any $x, y \in \alpha$, there exists $m \in M$ such that $m \cdot x = y$), then the original action of $N$ on $\alpha$ is also pretransitive.

MonoidHom.smulOneHom definition

{M N} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] : M →* N

Full source

/-- If the multiplicative action of `M` on `N` is compatible with multiplication on `N`, then
`fun x ↦ x • 1` is a monoid homomorphism from `M` to `N`. -/
@[to_additive (attr := simps)
"If the additive action of `M` on `N` is compatible with addition on `N`, then
`fun x ↦ x +ᵥ 0` is an additive monoid homomorphism from `M` to `N`."]
def MonoidHom.smulOneHom {M N} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] :
    M →* N where
  toFun x := x • (1 : N)
  map_one' := one_smul _ _
  map_mul' x y := by rw [smul_one_mul, smul_smul]

Monoid homomorphism induced by scalar multiplication with identity

Informal description

Given a monoid $ M $ acting on a multiplicative monoid $ N $ such that the action is compatible with multiplication on $ N $ (i.e., $ [\text{IsScalarTower}\ M\ N\ N] $), the function $ x \mapsto x \cdot 1_N $ is a monoid homomorphism from $ M $ to $ N $. Here, $ 1_N $ denotes the multiplicative identity of $ N $.

monoidHomEquivMulActionIsScalarTower definition

(M N) [Monoid M] [Monoid N] : (M →* N) ≃ { _inst : MulAction M N // IsScalarTower M N N }

Full source

/-- A monoid homomorphism between two monoids M and N can be equivalently specified by a
multiplicative action of M on N that is compatible with the multiplication on N. -/
@[to_additive
"A monoid homomorphism between two additive monoids M and N can be equivalently
specified by an additive action of M on N that is compatible with the addition on N."]
def monoidHomEquivMulActionIsScalarTower (M N) [Monoid M] [Monoid N] :
    (M →* N) ≃ {_inst : MulAction M N // IsScalarTower M N N} where
  toFun f := ⟨MulAction.compHom N f, SMul.comp.isScalarTower _⟩
  invFun := fun ⟨_, _⟩ ↦ MonoidHom.smulOneHom
  left_inv f := MonoidHom.ext fun m ↦ mul_one (f m)
  right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| MulAction.ext <| funext₂ <| smul_one_smul N

Equivalence between monoid homomorphisms and compatible multiplicative actions

Informal description

Given monoids $M$ and $N$, there is a natural equivalence between the type of monoid homomorphisms $M \to N$ and the type of multiplicative actions of $M$ on $N$ that are compatible with the multiplication on $N$ (i.e., satisfy the scalar tower condition). The equivalence is constructed as follows: - The forward direction takes a monoid homomorphism $f \colon M \to N$ and produces the multiplicative action of $M$ on $N$ defined by $m \cdot n = f(m) \cdot n$. - The backward direction takes a compatible multiplicative action and produces the monoid homomorphism $m \mapsto m \cdot 1_N$. This shows that monoid homomorphisms can be equivalently described via compatible multiplicative actions.