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.

      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