Mathlib.Algebra.Group.Embedding

mulLeftEmbedding definition

[Mul G] [IsLeftCancelMul G] (g : G) : G ↪ G

Full source

/-- If left-multiplication by any element is cancellative, left-multiplication by `g` is an
embedding. -/
@[to_additive (attr := simps)
      "If left-addition by any element is cancellative, left-addition by `g` is an
        embedding."]
def mulLeftEmbedding [Mul G] [IsLeftCancelMul G] (g : G) : G ↪ G where
  toFun h := g * h
  inj' := mul_right_injective g

Left multiplication embedding in a cancellative semigroup

Informal description

Given a multiplicative semigroup $ G $ where left-multiplication is cancellative (i.e., $ \forall a b c \in G, c * a = c * b \implies a = b $), the function $ h \mapsto g * h $ is an injective embedding of $ G $ into itself for any fixed element $ g \in G $.

mulRightEmbedding definition

[Mul G] [IsRightCancelMul G] (g : G) : G ↪ G

Full source

/-- If right-multiplication by any element is cancellative, right-multiplication by `g` is an
embedding. -/
@[to_additive (attr := simps)
      "If right-addition by any element is cancellative, right-addition by `g` is an
        embedding."]
def mulRightEmbedding [Mul G] [IsRightCancelMul G] (g : G) : G ↪ G where
  toFun h := h * g
  inj' := mul_left_injective g

Right multiplication embedding in a cancellative semigroup

Informal description

Given a multiplicative semigroup $ G $ where right-multiplication is cancellative (i.e., $ \forall a b c \in G, a * c = b * c \implies a = b $), the function $ h \mapsto h * g $ is an injective embedding of $ G $ into itself for any fixed element $ g \in G $.

mulLeftEmbedding_eq_mulRightEmbedding theorem

[CommMagma G] [IsCancelMul G] (g : G) : mulLeftEmbedding g = mulRightEmbedding g

Full source

@[to_additive]
theorem mulLeftEmbedding_eq_mulRightEmbedding [CommMagma G] [IsCancelMul G] (g : G) :
    mulLeftEmbedding g = mulRightEmbedding g := by
  ext
  exact mul_comm _ _

Equality of Left and Right Multiplication Embeddings in a Cancellative Commutative Magma

Informal description

Let $G$ be a commutative magma with cancellative multiplication. For any element $g \in G$, the left multiplication embedding $h \mapsto g * h$ is equal to the right multiplication embedding $h \mapsto h * g$.