Documentation

Mathlib.Algebra.Group.Action.Hom

Homomorphisms and group actions #

source
@[reducible, inline]
abbrev Function.Surjective.mulActionLeft {R : Type u_4} {S : Type u_5} {M : Type u_6} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) :
MulAction S M

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

See also Function.Surjective.distribMulActionLeft and Function.Surjective.moduleLeft.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Function.Surjective.addActionLeft {R : Type u_4} {S : Type u_5} {M : Type u_6} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) :
      AddAction S M

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

      Equations
        Instances For
          source
          @[reducible, inline]
          abbrev MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_3) [Monoid M] [MulAction M α] [Monoid N] (g : N →* M) :
          MulAction N α

          A multiplicative action of M on α and a monoid homomorphism N → M induce a multiplicative action of N on α.

          See note [reducible non-instances].

          Equations
            Instances For
              source
              @[reducible, inline]
              abbrev AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_3) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) :
              AddAction N α

              An additive action of M on α and an additive monoid homomorphism N → M induce an additive action of N on α.

              See note [reducible non-instances].

              Equations
                Instances For
                  source
                  theorem MulAction.compHom_smul_def {E : Type u_4} {F : Type u_5} {G : Type u_6} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
                  a • x = f a • x
                  source
                  theorem AddAction.compHom_vadd_def {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddMonoid E] [AddMonoid F] [AddAction F G] (f : E →+ F) (a : E) (x : G) :
                  a +ᵥ x = f a +ᵥ x
                  source
                  theorem MulAction.isPretransitive_compHom {E : Type u_4} {F : Type u_5} {G : Type u_6} [Monoid E] [Monoid F] [MulAction F G] [IsPretransitive F G] {f : E →* F} (hf : Function.Surjective ⇑f) :
                  IsPretransitive E G

                  If an action is transitive, then composing this action with a surjective homomorphism gives again a transitive action.

                  source
                  theorem AddAction.isPretransitive_compHom {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddMonoid E] [AddMonoid F] [AddAction F G] [IsPretransitive F G] {f : E →+ F} (hf : Function.Surjective ⇑f) :
                  IsPretransitive E G
                  source
                  theorem MulAction.IsPretransitive.of_compHom {M : Type u_4} {N : Type u_5} {α : Type u_6} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N) [h : IsPretransitive M α] :
                  IsPretransitive N α
                  source
                  theorem AddAction.IsPretransitive.of_compHom {M : Type u_4} {N : Type u_5} {α : Type u_6} [AddMonoid M] [AddMonoid N] [AddAction N α] (f : M →+ N) [h : IsPretransitive M α] :
                  IsPretransitive N α
                  source
                  def MonoidHom.smulOneHom {M : Type u_4} {N : Type u_5} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] :
                  M →* N

                  If the multiplicative action of M on N is compatible with multiplication on N, then fun x ↦ x • 1 is a monoid homomorphism from M to N.

                  Equations
                    Instances For
                      source
                      def AddMonoidHom.vaddZeroHom {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] :
                      M →+ N

                      If the additive action of M on N is compatible with addition on N, then fun x ↦ x +ᵥ 0 is an additive monoid homomorphism from M to N.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) :
                          vaddZeroHom x = x +ᵥ 0
                          source
                          @[simp]
                          theorem MonoidHom.smulOneHom_apply {M : Type u_4} {N : Type u_5} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) :
                          smulOneHom x = x • 1
                          source
                          def monoidHomEquivMulActionIsScalarTower (M : Type u_4) (N : Type u_5) [Monoid M] [Monoid N] :
                          (M →* N) ≃ { _inst : MulAction M N // IsScalarTower M N N }

                          A monoid homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.

                          Equations
                            Instances For
                              source
                              def addMonoidHomEquivAddActionVAddAssocClass (M : Type u_4) (N : Type u_5) [AddMonoid M] [AddMonoid N] :
                              (M →+ N) ≃ { _inst : AddAction M N // VAddAssocClass M N N }

                              A monoid homomorphism between two additive monoids M and N can be equivalently specified by an additive action of M on N that is compatible with the addition on N.

                              Equations
                                Instances For