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.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group 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

class SMulZeroClass (M : Type u_10) (A : Type u_11) [Zero A] extends SMul :
Type (max u_10 u_11)

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_10} {A : Type u_11} [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_4} [Zero A] [SMulZeroClass M A] (a : M) :
    a 0 = 0
    theorem smul_ite_zero {M : Type u_1} {A : Type u_4} [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_4} [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_4} [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_4} {B : Type u_5} [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
    Instances For
      @[reducible, inline]
      abbrev ZeroHom.smulZeroClass {M : Type u_1} {A : Type u_4} {B : Type u_5} [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
      Instances For
        @[reducible, inline]
        abbrev Function.Surjective.smulZeroClassLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [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
        Instances For
          @[reducible, inline]
          abbrev SMulZeroClass.compFun {M : Type u_1} {N : Type u_2} (A : Type u_4) [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
          Instances For
            @[simp]
            theorem SMulZeroClass.toZeroHom_apply {M : Type u_1} (A : Type u_4) [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_4) [Zero A] [SMulZeroClass M A] (x : M) :

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

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

              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_10} {A : Type u_11} [AddZeroClass A] [self : DistribSMul M A] (a : M) (x : A) (y : A) :
                a (x + y) = a x + a y

                Scalar multiplication distributes across addition

                theorem smul_add {M : Type u_1} {A : Type u_4} [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_4} {B : Type u_5} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] :
                Equations
                @[reducible, inline]
                abbrev Function.Injective.distribSMul {M : Type u_1} {A : Type u_4} {B : Type u_5} [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
                Instances For
                  @[reducible, inline]
                  abbrev Function.Surjective.distribSMul {M : Type u_1} {A : Type u_4} {B : Type u_5} [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
                  Instances For
                    @[reducible, inline]
                    abbrev Function.Surjective.distribSMulLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [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
                    Instances For
                      @[reducible, inline]
                      abbrev DistribSMul.compFun {M : Type u_1} {N : Type u_2} (A : Type u_4) [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
                      Instances For
                        @[simp]
                        theorem DistribSMul.toAddMonoidHom_apply {M : Type u_1} (A : Type u_4) [AddZeroClass A] [DistribSMul M A] (x : M) :
                        ∀ (x_1 : A), (DistribSMul.toAddMonoidHom A x) x_1 = (fun (x : M) (x_2 : A) => x x_2) x x_1
                        def DistribSMul.toAddMonoidHom {M : Type u_1} (A : Type u_4) [AddZeroClass A] [DistribSMul M A] (x : M) :
                        A →+ A

                        Each element of the scalars defines an additive monoid homomorphism.

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

                          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_10} {A : Type u_11} [Monoid M] [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_10} {A : Type u_11} [Monoid M] [AddMonoid A] [self : DistribMulAction M A] (a : M) (x : A) (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_4} [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_4} {B : Type u_5} [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
                            Instances For
                              @[reducible, inline]
                              abbrev Function.Surjective.distribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [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
                              Instances For
                                @[reducible, inline]
                                abbrev Function.Surjective.distribMulActionLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

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

                                See also Function.Surjective.mulActionLeft and Function.Surjective.moduleLeft.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[reducible, inline]
                                  abbrev DistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] [Monoid N] (f : N →* M) :

                                  Compose a DistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_1} (A : Type u_4) [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_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) :
                                    A →+ A

                                    Each element of the monoid defines an additive monoid homomorphism.

                                    Equations
                                    Instances For

                                      Each element of the monoid defines an additive monoid homomorphism.

                                      Equations
                                      Instances For
                                        instance AddMonoid.nat_smulCommClass (M : Type u_1) (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] :
                                        Equations
                                        • =
                                        Equations
                                        • =
                                        instance AddGroup.int_smulCommClass {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] :
                                        Equations
                                        • =
                                        instance AddGroup.int_smulCommClass' {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] :
                                        Equations
                                        • =
                                        @[simp]
                                        theorem smul_neg {M : Type u_1} {A : Type u_4} [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_4} [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_10} {A : Type u_11} :
                                        ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), SMul.smul = SMul.smulx = y
                                        theorem MulDistribMulAction.ext_iff {M : Type u_10} {A : Type u_11} :
                                        ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), x = y SMul.smul = SMul.smul
                                        class MulDistribMulAction (M : Type u_10) (A : Type u_11) [Monoid M] [Monoid A] extends MulAction :
                                        Type (max u_10 u_11)

                                        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_10} {A : Type u_11} [Monoid M] [Monoid A] [self : MulDistribMulAction M A] (r : M) (x : A) (y : A) :
                                          r (x * y) = r x * r y

                                          Distributivity of across *

                                          theorem MulDistribMulAction.smul_one {M : Type u_10} {A : Type u_11} [Monoid M] [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_4} [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_4} {B : Type u_5} [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
                                          Instances For
                                            @[reducible, inline]
                                            abbrev Function.Surjective.mulDistribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [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
                                            Instances For
                                              @[reducible, inline]
                                              abbrev MulDistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_4) [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid N] (f : N →* M) :

                                              Compose a MulDistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

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

                                                Scalar multiplication by r as a MonoidHom.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_1} {A : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) :
                                                  @[simp]
                                                  theorem smul_pow' {M : Type u_1} {A : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) (n : ) :
                                                  r x ^ n = (r x) ^ n

                                                  Each element of the monoid defines a monoid homomorphism.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem smul_inv' {M : Type u_1} {A : Type u_4} [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_4} [Monoid M] [Group A] [MulDistribMulAction M A] (r : M) (x : A) (y : A) :
                                                    r (x / y) = r x / r y

                                                    The tautological action by AddMonoid.End α on α.

                                                    This generalizes Function.End.applyMulAction.

                                                    Equations
                                                    @[simp]
                                                    theorem AddMonoid.End.smul_def {α : Type u_6} [AddMonoid α] (f : AddMonoid.End α) (a : α) :
                                                    f a = f a