Mathlib.Algebra.Group.Action.Faithful

Module docstring

{"# Faithful group actions

This file provides typeclasses for faithful actions.

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 ","### Faithful actions "}

FaithfulVAdd structure

(G : Type*) (P : Type*) [VAdd G P]

Full source

/-- Typeclass for faithful actions. -/
class FaithfulVAdd (G : Type*) (P : Type*) [VAdd G P] : Prop where
  /-- Two elements `g₁` and `g₂` are equal whenever they act in the same way on all points. -/
  eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ p : P, g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂

Faithful additive group action

Informal description

A structure representing a faithful additive group action, where the action of a group $G$ on a type $P$ is injective in the group element. That is, for any $g_1, g_2 \in G$, if $g_1 +ᵥ p = g_2 +ᵥ p$ for all $p \in P$, then $g_1 = g_2$.

FaithfulSMul structure

(M : Type*) (α : Type*) [SMul M α]

Full source

/-- Typeclass for faithful actions. -/
@[to_additive]
class FaithfulSMul (M : Type*) (α : Type*) [SMul M α] : Prop where
  /-- Two elements `m₁` and `m₂` are equal whenever they act in the same way on all points. -/
  eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ a : α, m₁ • a = m₂ • a) → m₁ = m₂

Faithful scalar multiplication

Informal description

The structure `FaithfulSMul M α` represents the property that the scalar multiplication action of `M` on `α` is faithful, meaning that the map `(· • ·) : M → α → α` is injective. In other words, distinct elements of `M` act differently on `α`.

smul_left_injective' theorem

[SMul M α] [FaithfulSMul M α] : Injective ((· • ·) : M → α → α)

Full source

@[to_additive]
lemma smul_left_injective' [SMul M α] [FaithfulSMul M α] : Injective ((· • ·) : M → α → α) :=
  fun _ _ h ↦ FaithfulSMul.eq_of_smul_eq_smul (congr_fun h)

Injectivity of Scalar Multiplication in Faithful Actions

Informal description

For a type $M$ acting on a type $\alpha$ via scalar multiplication, if the action is faithful (i.e., distinct elements of $M$ act differently on $\alpha$), then the map $(m \mapsto (a \mapsto m \cdot a)) : M \to (\alpha \to \alpha)$ is injective.

RightCancelMonoid.faithfulSMul instance

[RightCancelMonoid α] : FaithfulSMul α α

Full source

/-- `Monoid.toMulAction` is faithful on cancellative monoids. -/
@[to_additive "`AddMonoid.toAddAction` is faithful on additive cancellative monoids."]
instance RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
  ⟨fun h ↦ mul_right_cancel (h 1)⟩

Faithful Action of Right Cancellative Monoids on Themselves

Informal description

For any right cancellative monoid $\alpha$, the scalar multiplication action of $\alpha$ on itself is faithful. This means that if two elements $m, n \in \alpha$ satisfy $m \cdot a = n \cdot a$ for all $a \in \alpha$, then $m = n$.

LefttCancelMonoid.to_faithfulSMul_mulOpposite instance

[LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α

Full source

/-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
@[to_additive " `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids. "]
instance LefttCancelMonoid.to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
  ⟨fun h ↦ MulOpposite.unop_injective <| mul_left_cancel (h 1)⟩

Faithful Action of Opposite Monoid on Left Cancellative Monoid

Informal description

For any left cancellative monoid $\alpha$, the scalar multiplication action of the opposite monoid $\alpha^\mathrm{op}$ on $\alpha$ is faithful. This means that if two elements $m, n \in \alpha^\mathrm{op}$ satisfy $m \cdot a = n \cdot a$ for all $a \in \alpha$, then $m = n$.