# 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 #

source
class FaithfulVAdd (G : Type u_4) (P : Type u_5) [VAdd G P] :
Prop

Typeclass for faithful actions.

- eq_of_vadd_eq_vadd {g₁ g₂ : G} : (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂

  Two elements `g₁` and `g₂` are equal whenever they act in the same way on all points.

Instances

source
class FaithfulSMul (M : Type u_4) (α : Type u_5) [SMul M α] :
Prop

Typeclass for faithful actions.

- eq_of_smul_eq_smul {m₁ m₂ : M} : (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂

  Two elements `m₁` and `m₂` are equal whenever they act in the same way on all points.

Instances

source
theorem smul_left_injective' {M : Type u_1} {α : Type u_3} [SMul M α] [FaithfulSMul M α] :
Function.Injective fun (x1 : M) (x2 : α) => x1 • x2
source
theorem vadd_left_injective' {M : Type u_1} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] :
Function.Injective fun (x1 : M) (x2 : α) => x1 +ᵥ x2
source
instance RightCancelMonoid.faithfulSMul {α : Type u_3} [RightCancelMonoid α] :
FaithfulSMul α α

`Monoid.toMulAction` is faithful on cancellative monoids.

source
instance AddRightCancelMonoid.faithfulVAdd {α : Type u_3} [AddRightCancelMonoid α] :
FaithfulVAdd α α

`AddMonoid.toAddAction` is faithful on additive cancellative monoids.

source
instance LeftCancelMonoid.to_faithfulSMul_mulOpposite {α : Type u_3} [LeftCancelMonoid α] :
FaithfulSMul α ᵐᵒᵖ α

`Monoid.toOppositeMulAction` is faithful on cancellative monoids.

source
instance AddLeftCancelMonoid.to_faithfulVAdd_addOpposite {α : Type u_3} [AddLeftCancelMonoid α] :
FaithfulVAdd α ᵃᵒᵖ α

`AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids.

source
@[deprecated LeftCancelMonoid.to_faithfulSMul_mulOpposite (since := "2025-09-15")]
theorem LefttCancelMonoid.to_faithfulSMul_mulOpposite {α : Type u_3} [LeftCancelMonoid α] :
FaithfulSMul α ᵐᵒᵖ α

Alias of `LeftCancelMonoid.to_faithfulSMul_mulOpposite`.

`Monoid.toOppositeMulAction` is faithful on cancellative monoids.

source
instance instFaithfulSMul (R : Type u_4) [MulOneClass R] :
FaithfulSMul R R
source
theorem faithfulSMul_iff_injective_smul_one (R : Type u_4) (A : Type u_5) [MulOneClass A] [SMul R A] [IsScalarTower R A A] :
FaithfulSMul R A ↔ Function.Injective fun (r : R) => r • 1
source
theorem IsScalarTower.to₁₂₃ (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [SMul P Q] [FaithfulSMul P Q] [IsScalarTower M N Q] [IsScalarTower M P Q] [IsScalarTower N P Q] :
IsScalarTower M N P

Let `Q / P / N / M` be a tower. If `Q / N / M`, `Q / P / M` and `Q / P / N` are scalar towers, then `P / N / M` is also a scalar tower.

source
theorem VAddAssocClass.to₁₂₃ (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [VAdd M N] [VAdd M P] [VAdd M Q] [VAdd N P] [VAdd N Q] [VAdd P Q] [FaithfulVAdd P Q] [VAddAssocClass M N Q] [VAddAssocClass M P Q] [VAddAssocClass N P Q] :
VAddAssocClass M N P