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_9) (P : Type u_10) [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.

theorem FaithfulVAdd.eq_of_vadd_eq_vadd {G : Type u_9} {P : Type u_10} : ∀ {inst : VAdd G P} [self : FaithfulVAdd G P] {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_9) (α : Type u_10) [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 FaithfulSMul.eq_of_smul_eq_smul {M : Type u_9} {α : Type u_10} : ∀ {inst : SMul M α} [self : FaithfulSMul M α] {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 vadd_left_injective' {M : Type u_1} {α : Type u_5} [VAdd M α] [FaithfulVAdd M α] : Function.Injective fun (x1 : M) (x2 : α) => x1 +ᵥ x2

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

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

AddMonoid.toAddAction is faithful on additive cancellative monoids.

Equations

• ⋯ = ⋯

instance RightCancelMonoid.faithfulSMul {α : Type u_5} [RightCancelMonoid α] : FaithfulSMul α α

Monoid.toMulAction is faithful on cancellative monoids.

Equations

• ⋯ = ⋯

instance Function.End.apply_FaithfulSMul {α : Type u_5} : FaithfulSMul (Function.End α) α

Function.End.applyMulAction is faithful.

Equations

• ⋯ = ⋯