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

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.

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.

theorem smul_left_injective' {M : Type u_1} {α : Type u_3} [SMul M α] [FaithfulSMul M α] : Function.Injective fun (x1 : M) (x2 : α) => x1 • x2

theorem vadd_left_injective' {M : Type u_1} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] : Function.Injective fun (x1 : M) (x2 : α) => x1 +ᵥ x2

theorem RightCancelMonoid.faithfulSMul {α : Type u_3} [RightCancelMonoid α] : FaithfulSMul α α

Monoid.toMulAction is faithful on cancellative monoids.

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

AddMonoid.toAddAction is faithful on additive cancellative monoids.

theorem Function.End.apply_FaithfulSMul {α : Type u_3} : FaithfulSMul (Function.End α) α

Function.End.applyMulAction is faithful.