Documentation

Mathlib.Algebra.GroupWithZero.Action.Defs

Definitions of group actions #

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

The hierarchy is extended further by Module, defined elsewhere.

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

class SMulZeroClass (M : Type u_7) (A : Type u_8) [Zero A] extends SMul :
Type (max u_7 u_8)

Typeclass for scalar multiplication that preserves 0 on the right.

  • smul : MAA
  • smul_zero : ∀ (a : M), a 0 = 0

    Multiplying 0 by a scalar gives 0

Instances
    theorem SMulZeroClass.smul_zero {M : Type u_7} {A : Type u_8} :
    ∀ {inst : Zero A} [self : SMulZeroClass M A] (a : M), a 0 = 0

    Multiplying 0 by a scalar gives 0

    @[simp]
    theorem smul_zero {M : Type u_1} {A : Type u_3} [Zero A] [SMulZeroClass M A] (a : M) :
    a 0 = 0
    theorem smul_ite_zero {M : Type u_1} {A : Type u_3} [Zero A] [SMulZeroClass M A] (p : Prop) [Decidable p] (a : M) (b : A) :
    (a if p then b else 0) = if p then a b else 0
    theorem smul_eq_zero_of_right {M : Type u_1} {A : Type u_3} [Zero A] [SMulZeroClass M A] (a : M) {b : A} (h : b = 0) :
    a b = 0
    theorem right_ne_zero_of_smul {M : Type u_1} {A : Type u_3} [Zero A] [SMulZeroClass M A] {a : M} {b : A} :
    a b 0b 0
    @[reducible, inline]
    abbrev Function.Injective.smulZeroClass {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom B A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

    Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].

    Equations
    @[reducible, inline]
    abbrev ZeroHom.smulZeroClass {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

    Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].

    Equations
    @[reducible, inline]
    abbrev Function.Surjective.smulZeroClassLeft {R : Type u_7} {S : Type u_8} {M : Type u_9} [Zero M] [SMulZeroClass R M] [SMul S M] (f : RS) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

    Push forward the multiplication of R on M along a compatible surjective map f : R → S.

    See also Function.Surjective.distribMulActionLeft.

    Equations
    @[reducible, inline]
    abbrev SMulZeroClass.compFun {M : Type u_1} {N : Type u_2} (A : Type u_3) [Zero A] [SMulZeroClass M A] (f : NM) :

    Compose a SMulZeroClass with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

    Equations
    @[simp]
    theorem SMulZeroClass.toZeroHom_apply {M : Type u_1} (A : Type u_3) [Zero A] [SMulZeroClass M A] (x : M) :
    ∀ (x_1 : A), (SMulZeroClass.toZeroHom A x) x_1 = x x_1
    def SMulZeroClass.toZeroHom {M : Type u_1} (A : Type u_3) [Zero A] [SMulZeroClass M A] (x : M) :

    Each element of the scalars defines a zero-preserving map.

    Equations
    theorem DistribSMul.ext {M : Type u_7} {A : Type u_8} :
    ∀ {inst : AddZeroClass A} {x y : DistribSMul M A}, SMul.smul = SMul.smulx = y
    theorem DistribSMul.ext_iff {M : Type u_7} {A : Type u_8} :
    ∀ {inst : AddZeroClass A} {x y : DistribSMul M A}, x = y SMul.smul = SMul.smul
    class DistribSMul (M : Type u_7) (A : Type u_8) [AddZeroClass A] extends SMulZeroClass :
    Type (max u_7 u_8)

    Typeclass for scalar multiplication that preserves 0 and + on the right.

    This is exactly DistribMulAction without the MulAction part.

    • smul : MAA
    • smul_zero : ∀ (a : M), a 0 = 0
    • smul_add : ∀ (a : M) (x y : A), a (x + y) = a x + a y

      Scalar multiplication distributes across addition

    Instances
      theorem DistribSMul.smul_add {M : Type u_7} {A : Type u_8} :
      ∀ {inst : AddZeroClass A} [self : DistribSMul M A] (a : M) (x y : A), a (x + y) = a x + a y

      Scalar multiplication distributes across addition

      theorem smul_add {M : Type u_1} {A : Type u_3} [AddZeroClass A] [DistribSMul M A] (a : M) (b₁ : A) (b₂ : A) :
      a (b₁ + b₂) = a b₁ + a b₂
      instance AddMonoidHom.smulZeroClass {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] :
      Equations
      @[reducible, inline]
      abbrev Function.Injective.distribSMul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : B →+ A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

      Pullback a distributive scalar multiplication along an injective additive monoid homomorphism. See note [reducible non-instances].

      Equations
      @[reducible, inline]
      abbrev Function.Surjective.distribSMul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : A →+ B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

      Pushforward a distributive scalar multiplication along a surjective additive monoid homomorphism. See note [reducible non-instances].

      Equations
      @[reducible, inline]
      abbrev Function.Surjective.distribSMulLeft {R : Type u_7} {S : Type u_8} {M : Type u_9} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : RS) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

      Push forward the multiplication of R on M along a compatible surjective map f : R → S.

      See also Function.Surjective.distribMulActionLeft.

      Equations
      @[reducible, inline]
      abbrev DistribSMul.compFun {M : Type u_1} {N : Type u_2} (A : Type u_3) [AddZeroClass A] [DistribSMul M A] (f : NM) :

      Compose a DistribSMul with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

      Equations
      @[simp]
      theorem DistribSMul.toAddMonoidHom_apply {M : Type u_1} (A : Type u_3) [AddZeroClass A] [DistribSMul M A] (x : M) :
      ∀ (x_1 : A), (DistribSMul.toAddMonoidHom A x) x_1 = x x_1
      def DistribSMul.toAddMonoidHom {M : Type u_1} (A : Type u_3) [AddZeroClass A] [DistribSMul M A] (x : M) :
      A →+ A

      Each element of the scalars defines an additive monoid homomorphism.

      Equations
      theorem DistribMulAction.ext {M : Type u_7} {A : Type u_8} :
      ∀ {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A}, SMul.smul = SMul.smulx = y
      theorem DistribMulAction.ext_iff {M : Type u_7} {A : Type u_8} :
      ∀ {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A}, x = y SMul.smul = SMul.smul
      class DistribMulAction (M : Type u_7) (A : Type u_8) [Monoid M] [AddMonoid A] extends MulAction :
      Type (max u_7 u_8)

      Typeclass for multiplicative actions on additive structures. This generalizes group modules.

      • smul : MAA
      • one_smul : ∀ (b : A), 1 b = b
      • mul_smul : ∀ (x y : M) (b : A), (x * y) b = x y b
      • smul_zero : ∀ (a : M), a 0 = 0

        Multiplying 0 by a scalar gives 0

      • smul_add : ∀ (a : M) (x y : A), a (x + y) = a x + a y

        Scalar multiplication distributes across addition

      Instances
        theorem DistribMulAction.smul_zero {M : Type u_7} {A : Type u_8} :
        ∀ {inst : Monoid M} {inst_1 : AddMonoid A} [self : DistribMulAction M A] (a : M), a 0 = 0

        Multiplying 0 by a scalar gives 0

        theorem DistribMulAction.smul_add {M : Type u_7} {A : Type u_8} :
        ∀ {inst : Monoid M} {inst_1 : AddMonoid A} [self : DistribMulAction M A] (a : M) (x y : A), a (x + y) = a x + a y

        Scalar multiplication distributes across addition

        @[instance 100]
        instance DistribMulAction.toDistribSMul {M : Type u_1} {A : Type u_3} [Monoid M] [AddMonoid A] [DistribMulAction M A] :
        Equations

        Since Lean 3 does not have definitional eta for structures, we have to make sure that the definition of DistribMulAction.toDistribSMul was done correctly, and the two paths from DistribMulAction to SMul are indeed definitionally equal.

        @[reducible, inline]
        abbrev Function.Injective.distribMulAction {M : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : B →+ A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

        Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].

        Equations
        @[reducible, inline]
        abbrev Function.Surjective.distribMulAction {M : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

        Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].

        Equations
        @[simp]
        theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_1} (A : Type u_3) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) :
        ∀ (x_1 : A), (DistribMulAction.toAddMonoidHom A x) x_1 = x x_1
        def DistribMulAction.toAddMonoidHom {M : Type u_1} (A : Type u_3) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) :
        A →+ A

        Each element of the monoid defines an additive monoid homomorphism.

        Equations

        Each element of the monoid defines an additive monoid homomorphism.

        Equations
        instance AddMonoid.nat_smulCommClass (M : Type u_1) (A : Type u_3) [Monoid M] [AddMonoid A] [DistribMulAction M A] :
        Equations
        • =
        Equations
        • =
        instance AddGroup.int_smulCommClass {M : Type u_1} {A : Type u_3} [Monoid M] [AddGroup A] [DistribMulAction M A] :
        Equations
        • =
        instance AddGroup.int_smulCommClass' {M : Type u_1} {A : Type u_3} [Monoid M] [AddGroup A] [DistribMulAction M A] :
        Equations
        • =
        @[simp]
        theorem smul_neg {M : Type u_1} {A : Type u_3} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) :
        r -x = -(r x)
        theorem smul_sub {M : Type u_1} {A : Type u_3} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) (y : A) :
        r (x - y) = r x - r y
        theorem MulDistribMulAction.ext {M : Type u_7} {A : Type u_8} :
        ∀ {inst : Monoid M} {inst_1 : Monoid A} {x y : MulDistribMulAction M A}, SMul.smul = SMul.smulx = y
        theorem MulDistribMulAction.ext_iff {M : Type u_7} {A : Type u_8} :
        ∀ {inst : Monoid M} {inst_1 : Monoid A} {x y : MulDistribMulAction M A}, x = y SMul.smul = SMul.smul
        class MulDistribMulAction (M : Type u_7) (A : Type u_8) [Monoid M] [Monoid A] extends MulAction :
        Type (max u_7 u_8)

        Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.

        • smul : MAA
        • one_smul : ∀ (b : A), 1 b = b
        • mul_smul : ∀ (x y : M) (b : A), (x * y) b = x y b
        • smul_mul : ∀ (r : M) (x y : A), r (x * y) = r x * r y

          Distributivity of across *

        • smul_one : ∀ (r : M), r 1 = 1

          Multiplying 1 by a scalar gives 1

        Instances
          theorem MulDistribMulAction.smul_mul {M : Type u_7} {A : Type u_8} :
          ∀ {inst : Monoid M} {inst_1 : Monoid A} [self : MulDistribMulAction M A] (r : M) (x y : A), r (x * y) = r x * r y

          Distributivity of across *

          theorem MulDistribMulAction.smul_one {M : Type u_7} {A : Type u_8} :
          ∀ {inst : Monoid M} {inst_1 : Monoid A} [self : MulDistribMulAction M A] (r : M), r 1 = 1

          Multiplying 1 by a scalar gives 1

          theorem smul_mul' {M : Type u_1} {A : Type u_3} [Monoid M] [Monoid A] [MulDistribMulAction M A] (a : M) (b₁ : A) (b₂ : A) :
          a (b₁ * b₂) = a b₁ * a b₂
          @[reducible, inline]
          abbrev Function.Injective.mulDistribMulAction {M : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : B →* A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

          Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].

          Equations
          @[reducible, inline]
          abbrev Function.Surjective.mulDistribMulAction {M : Type u_1} {A : Type u_3} {B : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : A →* B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

          Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].

          Equations
          def MulDistribMulAction.toMonoidHom {M : Type u_1} (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) :
          A →* A

          Scalar multiplication by r as a MonoidHom.

          Equations
          @[simp]
          theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_1} {A : Type u_3} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) :
          @[simp]
          theorem smul_pow' {M : Type u_1} {A : Type u_3} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) (n : ) :
          r x ^ n = (r x) ^ n
          @[simp]
          theorem smul_inv' {M : Type u_1} {A : Type u_3} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) :
          r x⁻¹ = (r x)⁻¹
          theorem smul_div' {M : Type u_1} {A : Type u_3} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) (y : A) :
          r (x / y) = r x / r y
          theorem smul_eq_zero_iff_eq {α : Type u_5} {β : Type u_6} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} :
          a x = 0 x = 0
          theorem smul_ne_zero_iff_ne {α : Type u_5} {β : Type u_6} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} :
          a x 0 x 0