Documentation

Mathlib.Algebra.Hom.GroupAction

Equivariant homomorphisms #

Main definitions #

The above types have corresponding classes:

Notations #

structure MulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
Type (max u_2 u_3)

Equivariant functions.

Instances For

    Equivariant functions.

    Instances For
      class SMulHomClass (F : Type u_16) (M : outParam (Type u_17)) (X : outParam (Type u_18)) (Y : outParam (Type u_19)) [SMul M X] [SMul M Y] extends FunLike :
      Type (max (max u_16 u_18) u_19)
      • coe : FXY
      • coe_injective' : Function.Injective FunLike.coe
      • map_smul : ∀ (f : F) (c : M) (x : X), f (c x) = c f x

        The proposition that the function preserves the action.

      SMulHomClass F M X Y states that F is a type of morphisms preserving scalar multiplication by M.

      You should extend this class when you extend MulActionHom.

      Instances
        instance instSMulHomClassMulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
        SMulHomClass (X →[M'] Y) M' X Y
        def SMulHomClass.toMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] (f : F) :
        X →[M] Y

        Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

        Instances For
          instance MulActionHom.instCoeTCMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] :
          CoeTC F (X →[M] Y)

          Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

          theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) (m : M') (x : X) :
          f (m x) = m f x
          theorem MulActionHom.ext {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
          (∀ (x : X), f x = g x) → f = g
          theorem MulActionHom.ext_iff {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
          f = g ∀ (x : X), f x = g x
          theorem MulActionHom.congr_fun {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} (h : f = g) (x : X) :
          f x = g x
          def MulActionHom.id (M' : Type u_1) {X : Type u_2} [SMul M' X] :
          X →[M'] X

          The identity map as an equivariant map.

          Instances For
            @[simp]
            theorem MulActionHom.id_apply (M' : Type u_1) {X : Type u_2} [SMul M' X] (x : X) :
            ↑(MulActionHom.id M') x = x
            def MulActionHom.comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) :
            X →[M'] Z

            Composition of two equivariant maps.

            Instances For
              @[simp]
              theorem MulActionHom.comp_apply {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) :
              ↑(MulActionHom.comp g f) x = g (f x)
              @[simp]
              theorem MulActionHom.id_comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
              @[simp]
              theorem MulActionHom.comp_id {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
              @[simp]
              theorem MulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
              ∀ (a : B), ↑(MulActionHom.inverse f g h₁ h₂) a = g a
              def MulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
              B →[M] A

              The inverse of a bijective equivariant map is equivariant.

              Instances For
                @[simp]
                theorem SMulCommClass.toMulActionHom_apply {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
                ∀ (x : α), ↑(SMulCommClass.toMulActionHom N α c) x = c x
                def SMulCommClass.toMulActionHom {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
                α →[N] α

                If actions of M and N on α commute, then for c : M, (c • · : α → α) is an N-action homomorphism.

                Instances For
                  structure DistribMulActionHom (M : Type u_5) [Monoid M] (A : Type u_6) [AddMonoid A] [DistribMulAction M A] (B : Type u_8) [AddMonoid B] [DistribMulAction M B] extends MulActionHom :
                  Type (max u_6 u_8)

                  Equivariant additive monoid homomorphisms.

                  Instances For
                    @[reducible]
                    abbrev DistribMulActionHom.toAddMonoidHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (self : A →+[M] B) :
                    A →+ B

                    Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.

                    Instances For

                      Equivariant additive monoid homomorphisms.

                      Instances For
                        class DistribMulActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (A : outParam (Type u_18)) (B : outParam (Type u_19)) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] extends SMulHomClass :
                        Type (max (max u_16 u_18) u_19)
                        • coe : FAB
                        • coe_injective' : Function.Injective FunLike.coe
                        • map_smul : ∀ (f : F) (c : M) (x : A), f (c x) = c f x
                        • map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y

                          The proposition that the function preserves addition

                        • map_zero : ∀ (f : F), f 0 = 0

                          The proposition that the function preserves 0

                        DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and scalar multiplication by M.

                        You should extend this class when you extend DistribMulActionHom.

                        Instances
                          def DistribMulActionHomClass.toDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [DistribMulActionHomClass F M A B] (f : F) :
                          A →+[M] B

                          Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

                          Instances For
                            instance DistribMulActionHom.instCoeTCDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [DistribMulActionHomClass F M A B] :
                            CoeTC F (A →+[M] B)

                            Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

                            @[simp]
                            theorem DistribMulActionHom.toFun_eq_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
                            f.toFun = f
                            theorem DistribMulActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
                            f = f
                            theorem DistribMulActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
                            f = f
                            theorem DistribMulActionHom.ext {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :
                            (∀ (x : A), f x = g x) → f = g
                            theorem DistribMulActionHom.ext_iff {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :
                            f = g ∀ (x : A), f x = g x
                            theorem DistribMulActionHom.congr_fun {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) (x : A) :
                            f x = g x
                            theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
                            f = g
                            theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
                            f = g
                            theorem DistribMulActionHom.map_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
                            f 0 = 0
                            theorem DistribMulActionHom.map_add {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (x : A) (y : A) :
                            f (x + y) = f x + f y
                            theorem DistribMulActionHom.map_neg {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') :
                            f (-x) = -f x
                            theorem DistribMulActionHom.map_sub {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') (y : A') :
                            f (x - y) = f x - f y
                            theorem DistribMulActionHom.map_smul {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (m : M) (x : A) :
                            f (m x) = m f x
                            def DistribMulActionHom.id (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] :
                            A →+[M] A

                            The identity map as an equivariant additive monoid homomorphism.

                            Instances For
                              @[simp]
                              theorem DistribMulActionHom.id_apply (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (x : A) :
                              @[simp]
                              theorem DistribMulActionHom.coe_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] :
                              0 = 0
                              @[simp]
                              theorem DistribMulActionHom.coe_one {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] :
                              1 = id
                              theorem DistribMulActionHom.zero_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (a : A) :
                              0 a = 0
                              theorem DistribMulActionHom.one_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (a : A) :
                              1 a = a
                              def DistribMulActionHom.comp {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) :
                              A →+[M] C

                              Composition of two equivariant additive monoid homomorphisms.

                              Instances For
                                @[simp]
                                theorem DistribMulActionHom.comp_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :
                                ↑(DistribMulActionHom.comp g f) x = g (f x)
                                @[simp]
                                theorem DistribMulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                ∀ (a : B), ↑(DistribMulActionHom.inverse f g h₁ h₂) a = g a
                                def DistribMulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                B →+[M] A

                                The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

                                Instances For
                                  theorem DistribMulActionHom.ext_ring {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} (h : f 1 = g 1) :
                                  f = g
                                  theorem DistribMulActionHom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} :
                                  f = g f 1 = g 1
                                  @[simp]
                                  theorem SMulCommClass.toDistribMulActionHom_apply {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) :
                                  ∀ (x : A), ↑(SMulCommClass.toDistribMulActionHom N A c) x = c x
                                  def SMulCommClass.toDistribMulActionHom {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) :
                                  A →+[N] A

                                  If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

                                  Instances For
                                    structure MulSemiringActionHom (M : Type u_5) [Monoid M] (R : Type u_11) [Semiring R] [MulSemiringAction M R] (S : Type u_13) [Semiring S] [MulSemiringAction M S] extends DistribMulActionHom :
                                    Type (max u_11 u_13)

                                    Equivariant ring homomorphisms.

                                    Instances For
                                      @[reducible]
                                      abbrev MulSemiringActionHom.toRingHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (self : R →+*[M] S) :
                                      R →+* S

                                      Reinterpret an equivariant ring homomorphism as a ring homomorphism.

                                      Instances For

                                        Equivariant ring homomorphisms.

                                        Instances For
                                          class MulSemiringActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [Monoid M] [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction M S] extends DistribMulActionHomClass :
                                          Type (max (max u_16 u_18) u_19)
                                          • coe : FRS
                                          • coe_injective' : Function.Injective FunLike.coe
                                          • map_smul : ∀ (f : F) (c : M) (x : R), f (c x) = c f x
                                          • map_add : ∀ (f : F) (x y : R), f (x + y) = f x + f y
                                          • map_zero : ∀ (f : F), f 0 = 0
                                          • map_mul : ∀ (f : F) (x y : R), f (x * y) = f x * f y

                                            The proposition that the function preserves multiplication

                                          • map_one : ∀ (f : F), f 1 = 1

                                            The proposition that the function preserves 1

                                          MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and scalar multiplication by M.

                                          You should extend this class when you extend MulSemiringActionHom.

                                          Instances
                                            def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {F : Type u_16} [MulSemiringActionHomClass F M R S] (f : F) :
                                            R →+*[M] S

                                            Turn an element of a type F satisfying MulSemiringActionHomClass F M R S into an actual MulSemiringActionHom. This is declared as the default coercion from F to MulSemiringActionHom M X Y.

                                            Instances For
                                              theorem MulSemiringActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
                                              f = f
                                              theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
                                              f = f
                                              theorem MulSemiringActionHom.ext {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :
                                              (∀ (x : R), f x = g x) → f = g
                                              theorem MulSemiringActionHom.ext_iff {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :
                                              f = g ∀ (x : R), f x = g x
                                              theorem MulSemiringActionHom.map_zero {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
                                              f 0 = 0
                                              theorem MulSemiringActionHom.map_add {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :
                                              f (x + y) = f x + f y
                                              theorem MulSemiringActionHom.map_neg {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') :
                                              f (-x) = -f x
                                              theorem MulSemiringActionHom.map_sub {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') (y : R') :
                                              f (x - y) = f x - f y
                                              theorem MulSemiringActionHom.map_one {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
                                              f 1 = 1
                                              theorem MulSemiringActionHom.map_mul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :
                                              f (x * y) = f x * f y
                                              theorem MulSemiringActionHom.map_smul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) :
                                              f (m x) = m f x
                                              def MulSemiringActionHom.id (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] :
                                              R →+*[M] R

                                              The identity map as an equivariant ring homomorphism.

                                              Instances For
                                                @[simp]
                                                theorem MulSemiringActionHom.id_apply (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] (x : R) :
                                                def MulSemiringActionHom.comp {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) :
                                                R →+*[M] T

                                                Composition of two equivariant additive monoid homomorphisms.

                                                Instances For
                                                  @[simp]
                                                  theorem MulSemiringActionHom.comp_apply {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :
                                                  ↑(MulSemiringActionHom.comp g f) x = g (f x)