Documentation

Mathlib.Algebra.Group.Action.Faithful

Faithful group actions #

This file provides typeclasses for faithful actions.

Notation #

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 LefttCancelMonoid.to_faithfulSMul_mulOpposite {α : Type u_3} [LeftCancelMonoid α] :
FaithfulSMul αᵐᵒᵖ α

Monoid.toOppositeMulAction is faithful on cancellative monoids.

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

AddMonoid.toOppositeAddAction is faithful on additive cancellative monoids.