Mathlib.Algebra.Ring.AddAut

Module docstring

{"# Multiplication on the left/right as additive automorphisms

In this file we define AddAut.mulLeft and AddAut.mulRight.

See also AddMonoidHom.mulLeft, AddMonoidHom.mulRight, AddMonoid.End.mulLeft, and AddMonoid.End.mulRight for multiplication by R as an endomorphism instead of multiplication by Rˣ as an automorphism. "}

AddAut.mulLeft definition

: Rˣ →* AddAut R

Full source

/-- Left multiplication by a unit of a semiring as an additive automorphism. -/
@[simps! +simpRhs]
def mulLeft : RˣRˣ →* AddAut R :=
  DistribMulAction.toAddAut _ _

Left multiplication by a unit as an additive automorphism

Informal description

The function that maps each unit $ u $ of a semiring $ R $ to the additive automorphism of $ R $ given by left multiplication by $ u $, i.e., $ x \mapsto u \cdot x $. This is a group homomorphism from the group of units $ R^\times $ to the group of additive automorphisms of $ R $.

AddAut.mulRight definition

(u : Rˣ) : AddAut R

Full source

/-- Right multiplication by a unit of a semiring as an additive automorphism. -/
def mulRight (u : Rˣ) : AddAut R :=
  DistribMulAction.toAddAut RᵐᵒᵖRᵐᵒᵖˣ R (Units.opEquiv.symm <| MulOpposite.op u)

Right multiplication by a unit as an additive automorphism

Informal description

For any unit $ u $ in a semiring $ R $, the function that maps each element $ x \in R $ to $ x \cdot u $ is an additive automorphism of $ R $. This automorphism is obtained by considering the right multiplication by $ u $ as a distributive multiplicative action on $ R $, where the action is given by the multiplicative opposite structure of $ R $.

AddAut.mulRight_apply theorem

(u : Rˣ) (x : R) : mulRight u x = x * u

Full source

@[simp]
theorem mulRight_apply (u : Rˣ) (x : R) : mulRight u x = x * u :=
  rfl

Evaluation of Right Multiplication by a Unit as an Additive Automorphism: $\text{mulRight}(u)(x) = x \cdot u$

Informal description

For any unit $u$ in a semiring $R$ and any element $x \in R$, the additive automorphism `mulRight u` evaluated at $x$ equals $x \cdot u$.

AddAut.mulRight_symm_apply theorem

(u : Rˣ) (x : R) : (mulRight u).symm x = x * u⁻¹

Full source

@[simp]
theorem mulRight_symm_apply (u : Rˣ) (x : R) : (mulRight u).symm x = x * u⁻¹ :=
  rfl

Inverse of Right Multiplication by a Unit as an Additive Automorphism

Informal description

For any unit $u$ in a semiring $R$ and any element $x \in R$, the inverse of the additive automorphism induced by right multiplication by $u$ satisfies $(f_u)^{-1}(x) = x \cdot u^{-1}$, where $f_u$ is the automorphism defined by $f_u(y) = y \cdot u$.