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 instFaithfulSMul (R : Type u_4) [MulOneClass R] :
      FaithfulSMul R R

      instSMulOfMul is faithful when there is a (right) identity.

      source
      instance instFaithfulVAdd (R : Type u_4) [AddZeroClass R] :
      FaithfulVAdd R R

      instVAddOfAdd is faithful when there is a (right) identity.

      source
      instance instFaithfulSMulMulOpposite (R : Type u_4) [MulOneClass R] :
      FaithfulSMul Rᵐᵒᵖ R

      Mul.toSMulMulOpposite is faithful when there is a (left) identity.

      source
      instance instFaithfulVAddAddOpposite (R : Type u_4) [AddZeroClass R] :
      FaithfulVAdd Rᵃᵒᵖ R

      Add.toVAddAddOpposite is faithful when there is a (left) identity.

      source
      instance instFaithfulSMulOfIsRightCancelMul (R : Type u_4) [Mul R] [IsRightCancelMul R] :
      FaithfulSMul R R

      instSMulOfMul is faithful when multiplication is right cancellative.

      source
      instance instFaithfulVAddOfIsRightCancelAdd (R : Type u_4) [Add R] [IsRightCancelAdd R] :
      FaithfulVAdd R R

      instVAddOfAdd is faithful when addition is right cancellative.

      source
      instance instFaithfulSMulMulOppositeOfIsLeftCancelMul (R : Type u_4) [Mul R] [IsLeftCancelMul R] :
      FaithfulSMul Rᵐᵒᵖ R

      Mul.toSMulMulOpposite is faithful when multiplication is left cancellative

      source
      instance instFaithfulVAddAddOppositeOfIsLeftCancelAdd (R : Type u_4) [Add R] [IsLeftCancelAdd R] :
      FaithfulVAdd Rᵃᵒᵖ R

      Add.toVAddAddOpposite is faithful when addition is left cancellative

      source
      @[deprecated "subsumed by `instFaithfulSMul` or `instFaithfulSMulOfIsRightCancelMul`" (since := "2026-02-03")]
      theorem RightCancelMonoid.faithfulSMul {α : Type u_3} [RightCancelMonoid α] :
      FaithfulSMul α α

      Monoid.toMulAction is faithful on cancellative monoids.

      source
      @[deprecated "subsumed by `instFaithfulSMul` or `instFaithfulSMulOfIsRightCancelMul`" (since := "2026-02-03")]
      theorem AddRightCancelMonoid.faithfulVAdd {α : Type u_3} [AddRightCancelMonoid α] :
      FaithfulVAdd α α

      AddMonoid.toAddAction is faithful on additive cancellative monoids.

      source
      @[deprecated "subsumed by `instFaithfulSMulMulOpposite` or `instFaithfulSMulMulOppositeOfIsLeftCancelMul`" (since := "2026-02-03")]
      theorem LeftCancelMonoid.to_faithfulSMul_mulOpposite {α : Type u_3} [LeftCancelMonoid α] :
      FaithfulSMul αᵐᵒᵖ α

      Monoid.toOppositeMulAction is faithful on cancellative monoids.

      source
      @[deprecated "subsumed by `instFaithfulSMulMulOpposite` or `instFaithfulSMulMulOppositeOfIsLeftCancelMul`" (since := "2026-02-03")]
      theorem 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
      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 faithfulVAdd_iff_injective_vadd_zero (R : Type u_4) (A : Type u_5) [AddZeroClass A] [VAdd R A] [VAddAssocClass R A A] :
      FaithfulVAdd R A ↔ Function.Injective fun (r : R) => r +ᵥ 0
      source
      theorem faithfulSMul_iff {G : Type u_2} {α : Type u_3} [Group G] [MulAction G α] :
      FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
      source
      theorem faithfulVAdd_iff {G : Type u_2} {α : Type u_3} [AddGroup G] [AddAction G α] :
      FaithfulVAdd G α ↔ ∀ (g : G), (∀ (a : α), g +ᵥ a = a) → g = 0
      source
      theorem FaithfulSMul.tower_bot (R : Type u_4) (S : Type u_5) (T : Type u_6) [Monoid S] [MulOneClass T] [SMul R S] [SMul R T] [MulAction S T] [IsScalarTower R S S] [IsScalarTower R T T] [IsScalarTower R S T] [FaithfulSMul R T] :
      FaithfulSMul R S
      source
      theorem FaithfulVAdd.tower_bot (R : Type u_4) (S : Type u_5) (T : Type u_6) [AddMonoid S] [AddZeroClass T] [VAdd R S] [VAdd R T] [AddAction S T] [VAddAssocClass R S S] [VAddAssocClass R T T] [VAddAssocClass R S T] [FaithfulVAdd R T] :
      FaithfulVAdd R S
      source
      theorem FaithfulSMul.trans (R : Type u_4) (S : Type u_5) (T : Type u_6) [Monoid S] [MulOneClass T] [SMul R S] [IsScalarTower R S S] [MulAction S T] [IsScalarTower S T T] [SMul R T] [IsScalarTower R T T] [IsScalarTower R S T] [FaithfulSMul R S] [FaithfulSMul S T] :
      FaithfulSMul R T
      source
      theorem FaithfulVAdd.trans (R : Type u_4) (S : Type u_5) (T : Type u_6) [AddMonoid S] [AddZeroClass T] [VAdd R S] [VAddAssocClass R S S] [AddAction S T] [VAddAssocClass S T T] [VAdd R T] [VAddAssocClass R T T] [VAddAssocClass R S T] [FaithfulVAdd R S] [FaithfulVAdd S T] :
      FaithfulVAdd R T
      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
      source
      instance instFaithfulSMulMulOpposite_1 {M : Type u_1} {α : Type u_3} [SMul α M] [FaithfulSMul α M] :
      FaithfulSMul α Mᵐᵒᵖ