Documentation

Mathlib.GroupTheory.GroupAction.Hom

Equivariant homomorphisms #

Main definitions #

The above types have corresponding classes:

Notation #

We introduce the following notation to code equivariant maps (the subscript index is for equivariant) :

When M = N and φ = MonoidHom.id M, we provide the backward compatible notation :

The notation for MulActionHom and AddActionHom is the same, because it is unlikely that it could lead to confusion — unless one needs types M and X with simultaneous instances of Mul M, Add M, SMul M X and VAdd M X

structure AddActionHom {M : Type u_8} {N : Type u_9} (φ : MN) (X : Type u_10) [VAdd M X] (Y : Type u_11) [VAdd N Y] :
Type (max u_10 u_11)

Equivariant functions : When φ : M → N is a function, and types X and Y are endowed with additive actions of M and N, a function f : X → Y is φ-equivariant if f (m +ᵥ x) = (φ m) +ᵥ (f x).

  • toFun : XY

    The underlying function.

  • map_vadd' (m : M) (x : X) : self.toFun (m +ᵥ x) = φ m +ᵥ self.toFun x

    The proposition that the function commutes with the additive actions.

Instances For
    structure MulActionHom {M : Type u_2} {N : Type u_3} (φ : MN) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :
    Type (max u_5 u_6)

    Equivariant functions : When φ : M → N is a function, and types X and Y are endowed with actions of M and N, a function f : X → Y is φ-equivariant if f (m • x) = (φ m) • (f x).

    • toFun : XY

      The underlying function.

    • map_smul' (m : M) (x : X) : self.toFun (m x) = φ m self.toFun x

      The proposition that the function commutes with the actions.

    Instances For

      φ-equivariant functions X → Y, where φ : M → N, where M and N act on X and Y respectively.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        M-equivariant functions X → Y with respect to the action of M. This is the same as X →ₑ[@id M] Y.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          φ-equivariant functions X → Y, where φ : M → N, where M and N act additively on X and Y respectively

          We use the same notation as for multiplicative actions, as conflicts are unlikely.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            M-equivariant functions X → Y with respect to the additive action of M. This is the same as X →ₑ[@id M] Y.

            We use the same notation as for multiplicative actions, as conflicts are unlikely.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              class AddActionSemiHomClass (F : Type u_8) {M : outParam (Type u_9)} {N : outParam (Type u_10)} (φ : outParam (MN)) (X : outParam (Type u_11)) (Y : outParam (Type u_12)) [VAdd M X] [VAdd N Y] [FunLike F X Y] :

              AddActionSemiHomClass F φ X Y states that F is a type of morphisms which are φ-equivariant.

              You should extend this class when you extend AddActionHom.

              • map_vaddₛₗ (f : F) (c : M) (x : X) : f (c +ᵥ x) = φ c +ᵥ f x

                The proposition that the function preserves the action.

              Instances
                class MulActionSemiHomClass (F : Type u_8) {M : outParam (Type u_9)} {N : outParam (Type u_10)} (φ : outParam (MN)) (X : outParam (Type u_11)) (Y : outParam (Type u_12)) [SMul M X] [SMul N Y] [FunLike F X Y] :

                MulActionSemiHomClass F φ X Y states that F is a type of morphisms which are φ-equivariant.

                You should extend this class when you extend MulActionHom.

                • map_smulₛₗ (f : F) (c : M) (x : X) : f (c x) = φ c f x

                  The proposition that the function preserves the action.

                Instances
                  @[reducible, inline]
                  abbrev MulActionHomClass (F : Type u_8) (M : outParam (Type u_9)) (X : outParam (Type u_10)) (Y : outParam (Type u_11)) [SMul M X] [SMul M Y] [FunLike F X Y] :

                  MulActionHomClass F M X Y states that F is a type of morphisms which are equivariant with respect to actions of M This is an abbreviation of MulActionSemiHomClass.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev AddActionHomClass (F : Type u_8) (M : outParam (Type u_9)) (X : outParam (Type u_10)) (Y : outParam (Type u_11)) [VAdd M X] [VAdd M Y] [FunLike F X Y] :

                    MulActionHomClass F M X Y states that F is a type of morphisms which are equivariant with respect to actions of M This is an abbreviation of MulActionSemiHomClass.

                    Equations
                    Instances For
                      instance instFunLikeMulActionHom {M : Type u_2} {N : Type u_3} (φ : MN) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :
                      FunLike (X →ₑ[φ] Y) X Y
                      Equations
                      instance instFunLikeAddActionHom {M : Type u_2} {N : Type u_3} (φ : MN) (X : Type u_5) [VAdd M X] (Y : Type u_6) [VAdd N Y] :
                      FunLike (X →ₑ[φ] Y) X Y
                      Equations
                      @[simp]
                      theorem map_smul {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [SMul M X] [SMul M Y] [FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M) (x : X) :
                      f (c x) = c f x
                      @[simp]
                      theorem map_vadd {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [VAdd M X] [VAdd M Y] [FunLike F X Y] [AddActionHomClass F M X Y] (f : F) (c : M) (x : X) :
                      f (c +ᵥ x) = c +ᵥ f x
                      instance instMulActionSemiHomClassMulActionHom {M : Type u_2} {N : Type u_3} (φ : MN) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :
                      instance instAddActionSemiHomClassAddActionHom {M : Type u_2} {N : Type u_3} (φ : MN) (X : Type u_5) [VAdd M X] (Y : Type u_6) [VAdd N Y] :
                      def MulActionSemiHomClass.toMulActionHom {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {F : Type u_8} [FunLike F X Y] [MulActionSemiHomClass F φ X Y] (f : F) :
                      X →ₑ[φ] Y

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

                      Equations
                      • f = { toFun := f, map_smul' := }
                      Instances For
                        def AddActionSemiHomClass.toAddActionHom {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {F : Type u_8} [FunLike F X Y] [AddActionSemiHomClass F φ X Y] (f : F) :
                        X →ₑ[φ] Y

                        Turn an element of a type F satisfying AddActionSemiHomClass F φ X Y into an actual AddActionHom. This is declared as the default coercion from F to AddActionSemiHom φ X Y.

                        Equations
                        • f = { toFun := f, map_vadd' := }
                        Instances For
                          instance MulActionHom.instCoeTCOfMulActionSemiHomClass {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {F : Type u_8} [FunLike F X Y] [MulActionSemiHomClass F φ X Y] :
                          CoeTC F (X →ₑ[φ] Y)

                          Any type satisfying MulActionSemiHomClass can be cast into MulActionHom via MulActionHomSemiClass.toMulActionHom.

                          Equations
                          • MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }
                          instance AddActionHom.instCoeTCOfAddActionSemiHomClass {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {F : Type u_8} [FunLike F X Y] [AddActionSemiHomClass F φ X Y] :
                          CoeTC F (X →ₑ[φ] Y)
                          Equations
                          • AddActionHom.instCoeTCOfAddActionSemiHomClass = { coe := AddActionSemiHomClass.toAddActionHom }
                          theorem IsScalarTower.smulHomClass (M' : Type u_1) (X : Type u_5) [SMul M' X] (Y : Type u_6) [SMul M' Y] (F : Type u_8) [FunLike F X Y] [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [MulActionHomClass F X X Y] :

                          If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action.

                          theorem VAddAssocClass.vaddHomClass (M' : Type u_1) (X : Type u_5) [VAdd M' X] (Y : Type u_6) [VAdd M' Y] (F : Type u_8) [FunLike F X Y] [AddZeroClass X] [VAdd X Y] [VAddAssocClass M' X Y] [AddActionHomClass F X X Y] :
                          theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_5} [SMul M' X] {Y : Type u_6} [SMul M' Y] (f : X →ₑ[id] Y) (m : M') (x : X) :
                          f (m x) = m f x
                          theorem AddActionHom.map_vadd {M' : Type u_1} {X : Type u_5} [VAdd M' X] {Y : Type u_6} [VAdd M' Y] (f : X →ₑ[id] Y) (m : M') (x : X) :
                          f (m +ᵥ x) = m +ᵥ f x
                          theorem AddActionHom.ext {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {f g : X →ₑ[φ] Y} :
                          (∀ (x : X), f x = g x)f = g
                          theorem MulActionHom.ext {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {f g : X →ₑ[φ] Y} :
                          (∀ (x : X), f x = g x)f = g
                          theorem MulActionHom.congr_fun {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {f g : X →ₑ[φ] Y} (h : f = g) (x : X) :
                          f x = g x
                          theorem AddActionHom.congr_fun {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {f g : X →ₑ[φ] Y} (h : f = g) (x : X) :
                          f x = g x
                          def MulActionHom.ofEq {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) :
                          X →ₑ[φ'] Y

                          Two equal maps on scalars give rise to an equivariant map for identity

                          Equations
                          Instances For
                            def AddActionHom.ofEq {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) :
                            X →ₑ[φ'] Y

                            Two equal maps on scalars give rise to an equivariant map for identity

                            Equations
                            Instances For
                              @[simp]
                              theorem MulActionHom.ofEq_coe {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) :
                              (MulActionHom.ofEq h f).toFun = f.toFun
                              @[simp]
                              theorem AddActionHom.ofEq_coe {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) :
                              (AddActionHom.ofEq h f).toFun = f.toFun
                              @[simp]
                              theorem MulActionHom.ofEq_apply {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :
                              (MulActionHom.ofEq h f) a = f a
                              @[simp]
                              theorem AddActionHom.ofEq_apply {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : MN} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :
                              (AddActionHom.ofEq h f) a = f a
                              def MulActionHom.id (M : Type u_2) {X : Type u_5} [SMul M X] :
                              X →ₑ[id] X

                              The identity map as an equivariant map.

                              Equations
                              Instances For
                                def AddActionHom.id (M : Type u_2) {X : Type u_5} [VAdd M X] :
                                X →ₑ[id] X

                                The identity map as an equivariant map.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem MulActionHom.id_apply {M : Type u_2} {X : Type u_5} [SMul M X] (x : X) :
                                  @[simp]
                                  theorem AddActionHom.id_apply {M : Type u_2} {X : Type u_5} [VAdd M X] (x : X) :
                                  def MulActionHom.comp {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :
                                  X →ₑ[χ] Z

                                  Composition of two equivariant maps.

                                  Equations
                                  • g.comp f = { toFun := g f, map_smul' := }
                                  Instances For
                                    def AddActionHom.comp {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :
                                    X →ₑ[χ] Z

                                    Composition of two equivariant maps.

                                    Equations
                                    • g.comp f = { toFun := g f, map_vadd' := }
                                    Instances For
                                      @[simp]
                                      theorem MulActionHom.comp_apply {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :
                                      (g.comp f) x = g (f x)
                                      @[simp]
                                      theorem AddActionHom.comp_apply {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :
                                      (g.comp f) x = g (f x)
                                      @[simp]
                                      theorem MulActionHom.id_comp {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] (f : X →ₑ[φ] Y) :
                                      (MulActionHom.id N).comp f = f
                                      @[simp]
                                      theorem AddActionHom.id_comp {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] (f : X →ₑ[φ] Y) :
                                      (AddActionHom.id N).comp f = f
                                      @[simp]
                                      theorem MulActionHom.comp_id {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] (f : X →ₑ[φ] Y) :
                                      f.comp (MulActionHom.id M) = f
                                      @[simp]
                                      theorem AddActionHom.comp_id {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] (f : X →ₑ[φ] Y) :
                                      f.comp (AddActionHom.id M) = f
                                      @[simp]
                                      theorem MulActionHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] {Q : Type u_8} {T : Type u_9} [SMul Q T] {η : PQ} {θ : MQ} {ζ : NQ} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] [CompTriple χ η θ] [CompTriple ψ η ζ] [CompTriple φ ζ θ] :
                                      h.comp (g.comp f) = (h.comp g).comp f
                                      @[simp]
                                      theorem AddActionHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : MN} {ψ : NP} {χ : MP} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] {Q : Type u_8} {T : Type u_9} [VAdd Q T] {η : PQ} {θ : MQ} {ζ : NQ} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] [CompTriple χ η θ] [CompTriple ψ η ζ] [CompTriple φ ζ θ] :
                                      h.comp (g.comp f) = (h.comp g).comp f
                                      def MulActionHom.inverse {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                      Y₁ →ₑ[id] X

                                      The inverse of a bijective equivariant map is equivariant.

                                      Equations
                                      • f.inverse g h₁ h₂ = { toFun := g, map_smul' := }
                                      Instances For
                                        def AddActionHom.inverse {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                        Y₁ →ₑ[id] X

                                        The inverse of a bijective equivariant map is equivariant.

                                        Equations
                                        • f.inverse g h₁ h₂ = { toFun := g, map_vadd' := }
                                        Instances For
                                          @[simp]
                                          theorem MulActionHom.inverse_apply {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : Y₁) :
                                          (f.inverse g h₁ h₂) a✝ = g a✝
                                          @[simp]
                                          theorem AddActionHom.inverse_apply {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : Y₁) :
                                          (f.inverse g h₁ h₂) a✝ = g a✝
                                          def MulActionHom.inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : NM} (f : X →ₑ[φ] Y) (g : YX) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                          Y →ₑ[φ'] X

                                          The inverse of a bijective equivariant map is equivariant.

                                          Equations
                                          • f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := }
                                          Instances For
                                            def AddActionHom.inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : NM} (f : X →ₑ[φ] Y) (g : YX) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                            Y →ₑ[φ'] X

                                            The inverse of a bijective equivariant map is equivariant.

                                            Equations
                                            • f.inverse' g k h₁ h₂ = { toFun := g, map_vadd' := }
                                            Instances For
                                              @[simp]
                                              theorem AddActionHom.inverse'_apply {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : NM} (f : X →ₑ[φ] Y) (g : YX) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : Y) :
                                              (f.inverse' g k h₁ h₂) a✝ = g a✝
                                              @[simp]
                                              theorem MulActionHom.inverse'_apply {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : NM} (f : X →ₑ[φ] Y) (g : YX) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : Y) :
                                              (f.inverse' g k h₁ h₂) a✝ = g a✝
                                              theorem MulActionHom.inverse_eq_inverse' {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                              f.inverse g h₁ h₂ = f.inverse' g h₁ h₂
                                              theorem AddActionHom.inverse_eq_inverse' {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁X) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                              f.inverse g h₁ h₂ = f.inverse' g h₁ h₂
                                              theorem MulActionHom.inverse'_inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              (f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f
                                              theorem AddActionHom.inverse'_inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              (f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f
                                              theorem MulActionHom.comp_inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M
                                              theorem AddActionHom.comp_inverse' {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              (f.inverse' g k₂ h₁ h₂).comp f = AddActionHom.id M
                                              theorem MulActionHom.inverse'_comp {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N
                                              theorem AddActionHom.inverse'_comp {M : Type u_2} {N : Type u_3} {φ : MN} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : NM} {f : X →ₑ[φ] Y} {g : YX} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
                                              f.comp (f.inverse' g k₂ h₁ h₂) = AddActionHom.id N
                                              def SMulCommClass.toMulActionHom {M : Type u_11} (N : Type u_9) (α : Type u_10) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
                                              α →ₑ[id] α

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

                                              Equations
                                              Instances For
                                                def VAddCommClass.toAddActionHom {M : Type u_11} (N : Type u_9) (α : Type u_10) [VAdd M α] [VAdd N α] [VAddCommClass M N α] (c : M) :
                                                α →ₑ[id] α

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

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem SMulCommClass.toMulActionHom_apply {M : Type u_11} (N : Type u_9) (α : Type u_10) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) (x✝ : α) :
                                                  (SMulCommClass.toMulActionHom N α c) x✝ = c x✝
                                                  @[simp]
                                                  theorem VAddCommClass.toAddActionHom_apply {M : Type u_11} (N : Type u_9) (α : Type u_10) [VAdd M α] [VAdd N α] [VAddCommClass M N α] (c : M) (x✝ : α) :
                                                  (VAddCommClass.toAddActionHom N α c) x✝ = c +ᵥ x✝
                                                  structure DistribMulActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] extends A →ₑ[φ] B, A →+ B :
                                                  Type (max u_4 u_5)

                                                  Equivariant additive monoid homomorphisms.

                                                  Instances For

                                                    Equivariant additive monoid homomorphisms.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      Equivariant additive monoid homomorphisms.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        class DistribMulActionSemiHomClass (F : Type u_10) {M : outParam (Type u_11)} {N : outParam (Type u_12)} (φ : outParam (MN)) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Monoid M] [Monoid N] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction N B] [FunLike F A B] extends MulActionSemiHomClass F φ A B, AddMonoidHomClass F A B :

                                                        DistribMulActionSemiHomClass F φ A B states that F is a type of morphisms preserving the additive monoid structure and equivariant with respect to φ. You should extend this class when you extend DistribMulActionSemiHom.

                                                        Instances
                                                          @[reducible, inline]
                                                          abbrev DistribMulActionHomClass (F : Type u_10) (M : outParam (Type u_11)) (A : outParam (Type u_12)) (B : outParam (Type u_13)) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] :

                                                          DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and equivariant with respect to the action of M. It is an abbreviation to DistribMulActionHomClass F (MonoidHom.id M) A B You should extend this class when you extend DistribMulActionHom.

                                                          Equations
                                                          Instances For
                                                            instance DistribMulActionHom.instFunLike {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] :
                                                            FunLike (A →ₑ+[φ] B) A B
                                                            Equations
                                                            def DistribMulActionSemiHomClass.toDistribMulActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {F : Type u_10} [FunLike F A B] [DistribMulActionSemiHomClass F (⇑φ) A B] (f : F) :
                                                            A →ₑ+[φ] B

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

                                                            Equations
                                                            • f = { toFun := (↑f).toFun, map_smul' := , map_zero' := , map_add' := }
                                                            Instances For
                                                              instance DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {F : Type u_10} [FunLike F A B] [DistribMulActionSemiHomClass F (⇑φ) A B] :
                                                              CoeTC F (A →ₑ+[φ] B)

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

                                                              Equations
                                                              • DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom = { coe := DistribMulActionSemiHomClass.toDistribMulActionHom }
                                                              def SMulCommClass.toDistribMulActionHom {M : Type u_13} (N : Type u_11) (A : Type u_12) [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.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem SMulCommClass.toDistribMulActionHom_toFun {M : Type u_13} (N : Type u_11) (A : Type u_12) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) (x✝ : A) :
                                                                @[simp]
                                                                theorem DistribMulActionHom.toFun_eq_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                f.toFun = f
                                                                theorem DistribMulActionHom.coe_fn_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                f = f
                                                                theorem DistribMulActionHom.coe_fn_coe' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                f = f
                                                                theorem DistribMulActionHom.ext {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} :
                                                                (∀ (x : A), f x = g x)f = g
                                                                theorem DistribMulActionHom.congr_fun {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : f = g) (x : A) :
                                                                f x = g x
                                                                theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : f = g) :
                                                                f = g
                                                                theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : f = g) :
                                                                f = g
                                                                theorem DistribMulActionHom.map_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                f 0 = 0
                                                                theorem DistribMulActionHom.map_add {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) (x y : A) :
                                                                f (x + y) = f x + f y
                                                                theorem DistribMulActionHom.map_neg {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (A' : Type u_8) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x : A') :
                                                                f (-x) = -f x
                                                                theorem DistribMulActionHom.map_sub {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (A' : Type u_8) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x y : A') :
                                                                f (x - y) = f x - f y
                                                                theorem DistribMulActionHom.map_smulₑ {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) (m : M) (x : A) :
                                                                f (m x) = φ m f x
                                                                def DistribMulActionHom.id (M : Type u_1) [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] :
                                                                A →+[M] A

                                                                The identity map as an equivariant additive monoid homomorphism.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem DistribMulActionHom.id_apply (M : Type u_1) [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] (x : A) :
                                                                  instance DistribMulActionHom.instZero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :
                                                                  Zero (A →ₑ+[φ] B)
                                                                  Equations
                                                                  • DistribMulActionHom.instZero = { zero := let __src := 0; { toFun := (↑__src).toFun, map_smul' := , map_zero' := , map_add' := } }
                                                                  instance DistribMulActionHom.instOneId {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] :
                                                                  One (A →+[M] A)
                                                                  Equations
                                                                  @[simp]
                                                                  theorem DistribMulActionHom.coe_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :
                                                                  0 = 0
                                                                  @[simp]
                                                                  theorem DistribMulActionHom.coe_one {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] :
                                                                  1 = id
                                                                  theorem DistribMulActionHom.zero_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (a : A) :
                                                                  0 a = 0
                                                                  theorem DistribMulActionHom.one_apply {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] (a : A) :
                                                                  1 a = a
                                                                  instance DistribMulActionHom.instInhabited {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :
                                                                  Equations
                                                                  • DistribMulActionHom.instInhabited = { default := 0 }
                                                                  def DistribMulActionHom.comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [κ : φ.CompTriple ψ χ] :
                                                                  A →ₑ+[χ] C

                                                                  Composition of two equivariant additive monoid homomorphisms.

                                                                  Equations
                                                                  • g.comp f = { toMulActionHom := (↑g).comp f, map_zero' := , map_add' := }
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem DistribMulActionHom.comp_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [φ.CompTriple ψ χ] (x : A) :
                                                                    (g.comp f) x = g (f x)
                                                                    @[simp]
                                                                    theorem DistribMulActionHom.id_comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                    @[simp]
                                                                    theorem DistribMulActionHom.comp_id {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :
                                                                    @[simp]
                                                                    theorem DistribMulActionHom.comp_assoc {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] {Q : Type u_11} {D : Type u_12} [Monoid Q] [AddMonoid D] [DistribMulAction Q D] {η : P →* Q} {θ : M →* Q} {ζ : N →* Q} (h : C →ₑ+[η] D) (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [φ.CompTriple ψ χ] [χ.CompTriple η θ] [ψ.CompTriple η ζ] [φ.CompTriple ζ θ] :
                                                                    h.comp (g.comp f) = (h.comp g).comp f
                                                                    def DistribMulActionHom.inverse {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B₁ : Type u_6} [AddMonoid B₁] [DistribMulAction M B₁] (f : A →+[M] B₁) (g : B₁A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                                                    B₁ →+[M] A

                                                                    The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

                                                                    Equations
                                                                    • f.inverse g h₁ h₂ = { toFun := g, map_smul' := , map_zero' := , map_add' := }
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem DistribMulActionHom.inverse_toFun {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B₁ : Type u_6} [AddMonoid B₁] [DistribMulAction M B₁] (f : A →+[M] B₁) (g : B₁A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : B₁) :
                                                                      (f.inverse g h₁ h₂) a✝ = g a✝
                                                                      theorem DistribMulActionHom.ext_ring {R : Type u_11} [Semiring R] {S : Type u_12} [Semiring S] {N' : Type u_14} [AddMonoid N'] [DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'} (h : f 1 = g 1) :
                                                                      f = g
                                                                      structure MulSemiringActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] extends R →ₑ+[φ] S, R →+* S :
                                                                      Type (max u_10 u_12)

                                                                      Equivariant ring homomorphisms.

                                                                      Instances For

                                                                        Equivariant ring homomorphisms.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          Equivariant ring homomorphisms.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            class MulSemiringActionSemiHomClass (F : Type u_15) {M : outParam (Type u_16)} {N : outParam (Type u_17)} [Monoid M] [Monoid N] (φ : outParam (MN)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction N S] [FunLike F R S] extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S :

                                                                            MulSemiringActionHomClass F φ R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to φ.

                                                                            You should extend this class when you extend MulSemiringActionHom.

                                                                            Instances
                                                                              @[reducible, inline]
                                                                              abbrev MulSemiringActionHomClass (F : Type u_15) {M : outParam (Type u_16)} [Monoid M] (R : outParam (Type u_17)) (S : outParam (Type u_18)) [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction M S] [FunLike F R S] :

                                                                              MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to a DistribMulActionof M on R and S .

                                                                              Equations
                                                                              Instances For
                                                                                instance MulSemiringActionHom.instFunLike {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] :
                                                                                FunLike (R →ₑ+*[φ] S) R S
                                                                                Equations
                                                                                def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {F : Type u_15} [FunLike F R S] [MulSemiringActionSemiHomClass F (⇑φ) R S] (f : F) :

                                                                                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.

                                                                                Equations
                                                                                • f = { toFun := (↑f).toFun, map_smul' := , map_zero' := , map_add' := , map_one' := , map_mul' := }
                                                                                Instances For
                                                                                  instance MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {F : Type u_15} [FunLike F R S] [MulSemiringActionSemiHomClass F (⇑φ) R S] :
                                                                                  CoeTC F (R →ₑ+*[φ] S)

                                                                                  Any type satisfying MulSemiringActionHomClass can be cast into MulSemiringActionHom via MulSemiringActionHomClass.toMulSemiringActionHom.

                                                                                  Equations
                                                                                  • MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }
                                                                                  theorem MulSemiringActionHom.coe_fn_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                  f = f
                                                                                  theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                  f = f
                                                                                  theorem MulSemiringActionHom.ext {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {f g : R →ₑ+*[φ] S} :
                                                                                  (∀ (x : R), f x = g x)f = g
                                                                                  theorem MulSemiringActionHom.map_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                  f 0 = 0
                                                                                  theorem MulSemiringActionHom.map_add {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (x y : R) :
                                                                                  f (x + y) = f x + f y
                                                                                  theorem MulSemiringActionHom.map_neg {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (R' : Type u_11) [Ring R'] [MulSemiringAction M R'] (S' : Type u_13) [Ring S'] [MulSemiringAction N S'] (f : R' →ₑ+*[φ] S') (x : R') :
                                                                                  f (-x) = -f x
                                                                                  theorem MulSemiringActionHom.map_sub {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (R' : Type u_11) [Ring R'] [MulSemiringAction M R'] (S' : Type u_13) [Ring S'] [MulSemiringAction N S'] (f : R' →ₑ+*[φ] S') (x y : R') :
                                                                                  f (x - y) = f x - f y
                                                                                  theorem MulSemiringActionHom.map_one {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                  f 1 = 1
                                                                                  theorem MulSemiringActionHom.map_mul {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (x y : R) :
                                                                                  f (x * y) = f x * f y
                                                                                  theorem MulSemiringActionHom.map_smulₛₗ {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (m : M) (x : R) :
                                                                                  f (m x) = φ m f x
                                                                                  theorem MulSemiringActionHom.map_smul {M : Type u_1} [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [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_1) [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] :
                                                                                  R →+*[M] R

                                                                                  The identity map as an equivariant ring homomorphism.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem MulSemiringActionHom.id_apply (M : Type u_1) [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] (x : R) :
                                                                                    def MulSemiringActionHom.comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {T : Type u_14} [Semiring T] [MulSemiringAction P T] (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [κ : φ.CompTriple ψ χ] :

                                                                                    Composition of two equivariant additive ring homomorphisms.

                                                                                    Equations
                                                                                    • g.comp f = { toDistribMulActionHom := (↑g).comp f, map_one' := , map_mul' := }
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem MulSemiringActionHom.comp_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {T : Type u_14} [Semiring T] [MulSemiringAction P T] (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [φ.CompTriple ψ χ] (x : R) :
                                                                                      (g.comp f) x = g (f x)
                                                                                      @[simp]
                                                                                      theorem MulSemiringActionHom.id_comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                      @[simp]
                                                                                      theorem MulSemiringActionHom.comp_id {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :
                                                                                      def MulSemiringActionHom.inverse' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {φ' : N →* M} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (g : SR) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                                                                      S →ₑ+*[φ'] R

                                                                                      The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

                                                                                      Equations
                                                                                      • f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := , map_zero' := , map_add' := , map_one' := , map_mul' := }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem MulSemiringActionHom.inverse'_toFun {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {φ' : N →* M} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (g : SR) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : S) :
                                                                                        (f.inverse' g k h₁ h₂) a✝ = g a✝
                                                                                        def MulSemiringActionHom.inverse {M : Type u_1} [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S₁ : Type u_15} [Semiring S₁] [MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁R) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                                                                        S₁ →+*[M] R

                                                                                        The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

                                                                                        Equations
                                                                                        • f.inverse g h₁ h₂ = { toFun := g, map_smul' := , map_zero' := , map_add' := , map_one' := , map_mul' := }
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem MulSemiringActionHom.inverse_toFun {M : Type u_1} [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S₁ : Type u_15} [Semiring S₁] [MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁R) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (a✝ : S₁) :
                                                                                          (f.inverse g h₁ h₂) a✝ = g a✝