doc-next-gen

Mathlib.Algebra.Group.Hom.Instances

Module docstring

{"# Instances on spaces of monoid and group morphisms

We endow the space of monoid morphisms M →* N with a CommMonoid structure when the target is commutative, through pointwise multiplication, and with a CommGroup structure when the target is a commutative group. We also prove the same instances for additive situations.

Since these structures permit morphisms of morphisms, we also provide some composition-like operations.

Finally, we provide the Ring structure on AddMonoid.End. ","### Morphisms of morphisms

The structures above permit morphisms that themselves produce morphisms, provided the codomain is commutative. "}

MonoidHom.instCommMonoid instance
[MulOneClass M] [CommMonoid N] : CommMonoid (M →* N)
Full source 
/-- `(M →* N)` is a `CommMonoid` if `N` is commutative. -/
@[to_additive "`(M →+ N)` is an `AddCommMonoid` if `N` is commutative."]
instance MonoidHom.instCommMonoid [MulOneClass M] [CommMonoid N] :
    CommMonoid (M →* N) where
  mul := (· * ·)
  mul_assoc := by intros; ext; apply mul_assoc
  one := 1
  one_mul := by intros; ext; apply one_mul
  mul_one := by intros; ext; apply mul_one
  mul_comm := by intros; ext; apply mul_comm
  npow n f :=
    { toFun := fun x => f x ^ n, map_one' := by simp, map_mul' := fun x y => by simp [mul_pow] }
  npow_zero f := by
    ext x
    simp
  npow_succ n f := by
    ext x
    simp [pow_succ]
Commutative Monoid Structure on Monoid Homomorphisms to a Commutative Monoid
Informal description
For any monoid $M$ and commutative monoid $N$, the set of monoid homomorphisms $M \to^* N$ forms a commutative monoid under pointwise multiplication.
MonoidHom.instCommGroup instance
{M G} [MulOneClass M] [CommGroup G] : CommGroup (M →* G)
Full source 
/-- If `G` is a commutative group, then `M →* G` is a commutative group too. -/
@[to_additive "If `G` is an additive commutative group, then `M →+ G` is an additive commutative
      group too."]
instance MonoidHom.instCommGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M →* G) :=
  { MonoidHom.instCommMonoid with
    inv := Inv.inv,
    div := Div.div,
    div_eq_mul_inv := by
      intros
      ext
      apply div_eq_mul_inv,
    inv_mul_cancel := by intros; ext; apply inv_mul_cancel,
    zpow := fun n f =>
      { toFun := fun x => f x ^ n,
        map_one' := by simp,
        map_mul' := fun x y => by simp [mul_zpow] },
    zpow_zero' := fun f => by
      ext x
      simp,
    zpow_succ' := fun n f => by
      ext x
      simp [zpow_add_one],
    zpow_neg' := fun n f => by
      ext x
      simp [zpow_natCast, -Int.natCast_add] }
Commutative Group Structure on Monoid Homomorphisms to a Commutative Group
Informal description
For any monoid $M$ and commutative group $G$, the set of monoid homomorphisms $M \to^* G$ forms a commutative group under pointwise multiplication.
AddMonoid.End.instAddCommMonoid instance
[AddCommMonoid M] : AddCommMonoid (AddMonoid.End M)
Full source 
instance AddMonoid.End.instAddCommMonoid [AddCommMonoid M] : AddCommMonoid (AddMonoid.End M) :=
  AddMonoidHom.instAddCommMonoid
Additive Commutative Monoid Structure on Endomorphisms of an Additive Commutative Monoid
Informal description
For any additive commutative monoid $M$, the space of additive monoid endomorphisms $\text{End}(M)$ forms an additive commutative monoid under pointwise addition.
AddMonoid.End.zero_apply theorem
[AddCommMonoid M] (m : M) : (0 : AddMonoid.End M) m = 0
Full source 
@[simp]
theorem AddMonoid.End.zero_apply [AddCommMonoid M] (m : M) : (0 : AddMonoid.End M) m = 0 :=
  rfl
Zero Endomorphism Acts as Zero on Additive Monoid Elements
Informal description
For any additive commutative monoid $M$ and any element $m \in M$, the zero endomorphism $0 \in \text{End}(M)$ satisfies $0(m) = 0$.
AddMonoid.End.one_apply theorem
[AddZeroClass M] (m : M) : (1 : AddMonoid.End M) m = m
Full source 
theorem AddMonoid.End.one_apply [AddZeroClass M] (m : M) : (1 : AddMonoid.End M) m = m :=
  rfl
Identity Endomorphism Acts as Identity on Additive Monoid Elements
Informal description
For any type $M$ with an additive zero class structure and any element $m \in M$, the identity endomorphism $1$ of the additive monoid $\text{End}(M)$ satisfies $1(m) = m$.
AddMonoid.End.instAddCommGroup instance
[AddCommGroup M] : AddCommGroup (AddMonoid.End M)
Full source 
instance AddMonoid.End.instAddCommGroup [AddCommGroup M] : AddCommGroup (AddMonoid.End M) :=
  AddMonoidHom.instAddCommGroup
Additive Commutative Group Structure on Endomorphisms of an Additive Commutative Group
Informal description
For any additive commutative group $M$, the space of additive monoid endomorphisms $\text{End}(M)$ forms an additive commutative group under pointwise addition.
AddMonoid.End.instIntCast instance
[AddCommGroup M] : IntCast (AddMonoid.End M)
Full source 
instance AddMonoid.End.instIntCast [AddCommGroup M] : IntCast (AddMonoid.End M) :=
  { intCast := fun z => z • (1 : AddMonoid.End M) }
Integer Scalar Multiplication on Additive Monoid Endomorphisms
Informal description
For any additive commutative group $M$, the space of additive monoid endomorphisms $\text{End}(M)$ has a canonical integer scalar multiplication structure.
AddMonoid.End.intCast_apply theorem
[AddCommGroup M] (z : ℤ) (m : M) : (↑z : AddMonoid.End M) m = z • m
Full source 
/-- See also `AddMonoid.End.intCast_def`. -/
@[simp]
theorem AddMonoid.End.intCast_apply [AddCommGroup M] (z : ℤ) (m : M) :
    (↑z : AddMonoid.End M) m = z • m :=
  rfl
Integer Scalar Action on Additive Endomorphisms Equals Scalar Multiplication
Informal description
For any additive commutative group $M$, an integer $z \in \mathbb{Z}$, and an element $m \in M$, the action of the integer scalar $z$ on $m$ via the endomorphism ring $\text{End}(M)$ is equal to the scalar multiplication $z \cdot m$, i.e., $(z : \text{End}(M))(m) = z \cdot m$.
MonoidHom.pow_apply theorem
{M N : Type*} [MulOneClass M] [CommMonoid N] (f : M →* N) (n : ℕ) (x : M) : (f ^ n) x = (f x) ^ n
Full source 
@[to_additive (attr := simp)] lemma MonoidHom.pow_apply {M N : Type*} [MulOneClass M]
    [CommMonoid N] (f : M →* N) (n : ℕ) (x : M) :
    (f ^ n) x = (f x) ^ n :=
  rfl
Power of Monoid Homomorphism Equals Pointwise Power
Informal description
For any monoid $M$ and commutative monoid $N$, given a monoid homomorphism $f \colon M \to N$ and a natural number $n \in \mathbb{N}$, the $n$-th power of $f$ evaluated at $x \in M$ equals the $n$-th power of $f(x)$, i.e., $(f^n)(x) = (f(x))^n$.
MonoidHom.ext_iff₂ theorem
{_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} {f g : M →* N →* P} : f = g ↔ ∀ x y, f x y = g x y
Full source 
@[to_additive]
theorem ext_iff₂ {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} {f g : M →* N →* P} :
    f = g ↔ ∀ x y, f x y = g x y :=
  DFunLike.ext_iff.trans <| forall_congr' fun _ => DFunLike.ext_iff
Extensionality Criterion for Bivariate Monoid Homomorphisms to a Commutative Monoid
Informal description
For any monoids $M$ and $N$ and commutative monoid $P$, two monoid homomorphisms $f, g \colon M \to^* N \to^* P$ are equal if and only if $f(x)(y) = g(x)(y)$ for all $x \in M$ and $y \in N$.
MonoidHom.flip definition
{mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P} (f : M →* N →* P) : N →* M →* P
Full source 
/-- `flip` arguments of `f : M →* N →* P` -/
@[to_additive "`flip` arguments of `f : M →+ N →+ P`"]
def flip {mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P} (f : M →* N →* P) :
    N →* M →* P where
  toFun y :=
    { toFun := fun x => f x y,
      map_one' := by simp [f.map_one, one_apply],
      map_mul' := fun x₁ x₂ => by simp [f.map_mul, mul_apply] }
  map_one' := ext fun x => (f x).map_one
  map_mul' y₁ y₂ := ext fun x => (f x).map_mul y₁ y₂
Flip of monoid homomorphism-valued monoid homomorphism
Informal description
Given monoids $M$ and $N$ and a commutative monoid $P$, the function `flip` transforms a monoid homomorphism $f \colon M \to^* (N \to^* P)$ into a monoid homomorphism $N \to^* (M \to^* P)$. Specifically, for any $f$, the flipped homomorphism $f.\text{flip}$ satisfies $(f.\text{flip} \, y) \, x = f \, x \, y$ for all $x \in M$ and $y \in N$.
MonoidHom.flip_apply theorem
{_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P) (x : M) (y : N) : f.flip y x = f x y
Full source 
@[to_additive (attr := simp)]
theorem flip_apply {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P)
    (x : M) (y : N) : f.flip y x = f x y :=
  rfl
Flip Application Identity for Monoid Homomorphisms
Informal description
For any monoids $M$ and $N$ and commutative monoid $P$, given a monoid homomorphism $f \colon M \to^* (N \to^* P)$, the flipped homomorphism $f.\text{flip} \colon N \to^* (M \to^* P)$ satisfies $(f.\text{flip} \, y) \, x = f \, x \, y$ for all $x \in M$ and $y \in N$.
MonoidHom.map_one₂ theorem
{_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P) (n : N) : f 1 n = 1
Full source 
@[to_additive]
theorem map_one₂ {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P)
    (n : N) : f 1 n = 1 :=
  (flip f n).map_one
Preservation of Identity by Monoid Homomorphism-Valued Homomorphism: $f(1)(n) = 1$
Informal description
For any monoid homomorphism $f \colon M \to^* (N \to^* P)$ where $M$ and $N$ are monoids and $P$ is a commutative monoid, and for any element $n \in N$, the evaluation of $f$ at the identity element $1 \in M$ and $n$ yields the identity element in $P$, i.e., $f(1)(n) = 1$.
MonoidHom.map_mul₂ theorem
{_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) : f (m₁ * m₂) n = f m₁ n * f m₂ n
Full source 
@[to_additive]
theorem map_mul₂ {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P)
    (m₁ m₂ : M) (n : N) : f (m₁ * m₂) n = f m₁ n * f m₂ n :=
  (flip f n).map_mul _ _
Pointwise Multiplicativity of Monoid Homomorphism-Valued Homomorphisms
Informal description
Let $M$ and $N$ be monoids and $P$ be a commutative monoid. For any monoid homomorphism $f \colon M \to^* (N \to^* P)$ and elements $m_1, m_2 \in M$, $n \in N$, we have $f(m_1 \cdot m_2)(n) = f(m_1)(n) \cdot f(m_2)(n)$.
MonoidHom.map_inv₂ theorem
{_ : Group M} {_ : MulOneClass N} {_ : CommGroup P} (f : M →* N →* P) (m : M) (n : N) : f m⁻¹ n = (f m n)⁻¹
Full source 
@[to_additive]
theorem map_inv₂ {_ : Group M} {_ : MulOneClass N} {_ : CommGroup P} (f : M →* N →* P) (m : M)
    (n : N) : f m⁻¹ n = (f m n)⁻¹ :=
  (flip f n).map_inv _
Inverse Preservation for Monoid Homomorphism-Valued Homomorphisms: $f(m^{-1})(n) = (f(m)(n))^{-1}$
Informal description
Let $M$ be a group, $N$ a monoid, and $P$ a commutative group. For any monoid homomorphism $f \colon M \to (N \to^* P)$ and elements $m \in M$, $n \in N$, we have $f(m^{-1})(n) = (f(m)(n))^{-1}$.
MonoidHom.map_div₂ theorem
{_ : Group M} {_ : MulOneClass N} {_ : CommGroup P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) : f (m₁ / m₂) n = f m₁ n / f m₂ n
Full source 
@[to_additive]
theorem map_div₂ {_ : Group M} {_ : MulOneClass N} {_ : CommGroup P} (f : M →* N →* P)
    (m₁ m₂ : M) (n : N) : f (m₁ / m₂) n = f m₁ n / f m₂ n :=
  (flip f n).map_div _ _
Division Preservation for Monoid Homomorphism-Valued Homomorphisms: $f(m_1 / m_2)(n) = f(m_1)(n) / f(m_2)(n)$
Informal description
Let $M$ be a group, $N$ a monoid, and $P$ a commutative group. For any monoid homomorphism $f \colon M \to (N \to^* P)$ and elements $m_1, m_2 \in M$, $n \in N$, the homomorphism $f$ preserves division in the following sense: \[ f(m_1 / m_2)(n) = f(m_1)(n) / f(m_2)(n). \]
MonoidHom.eval definition
[MulOneClass M] [CommMonoid N] : M →* (M →* N) →* N
Full source 
/-- Evaluation of a `MonoidHom` at a point as a monoid homomorphism. See also `MonoidHom.apply`
for the evaluation of any function at a point. -/
@[to_additive (attr := simps!)
      "Evaluation of an `AddMonoidHom` at a point as an additive monoid homomorphism.
      See also `AddMonoidHom.apply` for the evaluation of any function at a point."]
def eval [MulOneClass M] [CommMonoid N] : M →* (M →* N) →* N :=
  (MonoidHom.id (M →* N)).flip
Evaluation of monoid homomorphisms as a monoid homomorphism
Informal description
The evaluation of a monoid homomorphism at a point, viewed as a monoid homomorphism. Specifically, for a monoid $M$ and a commutative monoid $N$, the function `MonoidHom.eval` maps an element $x \in M$ to the monoid homomorphism $(M \to^* N) \to^* N$ that evaluates any homomorphism $f \colon M \to^* N$ at $x$, i.e., $f \mapsto f(x)$. This is constructed by flipping the identity homomorphism on the space of homomorphisms $M \to^* N$.
MonoidHom.compHom' definition
[MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) : (N →* P) →* M →* P
Full source 
/-- The expression `fun g m ↦ g (f m)` as a `MonoidHom`.
Equivalently, `(fun g ↦ MonoidHom.comp g f)` as a `MonoidHom`. -/
@[to_additive (attr := simps!)
      "The expression `fun g m ↦ g (f m)` as an `AddMonoidHom`.
      Equivalently, `(fun g ↦ AddMonoidHom.comp g f)` as an `AddMonoidHom`.

      This also exists in a `LinearMap` version, `LinearMap.lcomp`."]
def compHom' [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) : (N →* P) →* M →* P :=
  flip <| eval.comp f
Pre-composition as a monoid homomorphism between homomorphism spaces
Informal description
Given monoids \( M \), \( N \), and a commutative monoid \( P \), the function `MonoidHom.compHom'` maps a monoid homomorphism \( f \colon M \to^* N \) to the monoid homomorphism \( (N \to^* P) \to^* (M \to^* P) \) defined by pre-composition with \( f \). That is, for any \( g \colon N \to^* P \), the resulting homomorphism is \( g \circ f \). This function itself is a monoid homomorphism, preserving the identity and multiplication of homomorphisms.
MonoidHom.compHom definition
[MulOneClass M] [CommMonoid N] [CommMonoid P] : (N →* P) →* (M →* N) →* M →* P
Full source 
/-- Composition of monoid morphisms (`MonoidHom.comp`) as a monoid morphism.

Note that unlike `MonoidHom.comp_hom'` this requires commutativity of `N`. -/
@[to_additive (attr := simps)
      "Composition of additive monoid morphisms (`AddMonoidHom.comp`) as an additive
      monoid morphism.

      Note that unlike `AddMonoidHom.comp_hom'` this requires commutativity of `N`.

      This also exists in a `LinearMap` version, `LinearMap.llcomp`."]
def compHom [MulOneClass M] [CommMonoid N] [CommMonoid P] :
    (N →* P) →* (M →* N) →* M →* P where
  toFun g := { toFun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g }
  map_one' := by
    ext1 f
    exact one_comp f
  map_mul' g₁ g₂ := by
    ext1 f
    exact mul_comp g₁ g₂ f
Composition as a monoid homomorphism between homomorphism spaces
Informal description
Given monoids \( M \), \( N \), and \( P \) with \( N \) and \( P \) commutative, the function `MonoidHom.compHom` maps a monoid homomorphism \( g \colon N \to^* P \) to the monoid homomorphism \( (M \to^* N) \to^* (M \to^* P) \) defined by composition with \( g \). This function itself is a monoid homomorphism, preserving the identity and multiplication of homomorphisms.
MonoidHom.flipHom definition
{_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} : (M →* N →* P) →* N →* M →* P
Full source 
/-- Flipping arguments of monoid morphisms (`MonoidHom.flip`) as a monoid morphism. -/
@[to_additive (attr := simps)
      "Flipping arguments of additive monoid morphisms (`AddMonoidHom.flip`)
      as an additive monoid morphism."]
def flipHom {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} :
    (M →* N →* P) →* N →* M →* P where
  toFun := MonoidHom.flip
  map_one' := rfl
  map_mul' _ _ := rfl
Flip homomorphism for monoid homomorphisms
Informal description
Given monoids \( M \) and \( N \) and a commutative monoid \( P \), the function `flipHom` is a monoid homomorphism that transforms a monoid homomorphism \( f \colon M \to^* (N \to^* P) \) into a monoid homomorphism \( N \to^* (M \to^* P) \). Specifically, for any \( f \), the flipped homomorphism \( f.\text{flip} \) satisfies \( (f.\text{flip} \, y) \, x = f \, x \, y \) for all \( x \in M \) and \( y \in N \). This function preserves the identity and multiplication of homomorphisms.
MonoidHom.compl₂ definition
[MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) : M →* Q →* P
Full source 
/-- The expression `fun m q ↦ f m (g q)` as a `MonoidHom`.

Note that the expression `fun q n ↦ f (g q) n` is simply `MonoidHom.comp`. -/
@[to_additive
      "The expression `fun m q ↦ f m (g q)` as an `AddMonoidHom`.

      Note that the expression `fun q n ↦ f (g q) n` is simply `AddMonoidHom.comp`.

      This also exists as a `LinearMap` version, `LinearMap.compl₂`"]
def compl₂ [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P)
    (g : Q →* N) : M →* Q →* P :=
  (compHom' g).comp f
Substitution into the second argument of a bivariate monoid homomorphism
Informal description
Given monoids \( M \), \( N \), \( P \), and \( Q \) with \( P \) commutative, the function `MonoidHom.compl₂` takes a monoid homomorphism \( f \colon M \to^* (N \to^* P) \) and a monoid homomorphism \( g \colon Q \to^* N \), and returns the monoid homomorphism \( M \to^* (Q \to^* P) \) defined by \( (m, q) \mapsto f(m, g(q)) \). This operation effectively substitutes \( g \) into the second argument of the bivariate homomorphism \( f \).
MonoidHom.compl₂_apply theorem
[MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) : (compl₂ f g) m q = f m (g q)
Full source 
@[to_additive (attr := simp)]
theorem compl₂_apply [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q]
    (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) : (compl₂ f g) m q = f m (g q) :=
  rfl
Evaluation of Substituted Bivariate Monoid Homomorphism: $(\text{compl}_2(f, g))(m)(q) = f(m)(g(q))$
Informal description
Let $M$, $N$, $P$, and $Q$ be monoids, with $P$ commutative. Given a monoid homomorphism $f \colon M \to (N \to P)$ and a monoid homomorphism $g \colon Q \to N$, the evaluation of the composed homomorphism $\text{compl}_2(f, g) \colon M \to (Q \to P)$ satisfies $(\text{compl}_2(f, g))(m)(q) = f(m)(g(q))$ for all $m \in M$ and $q \in Q$.
MonoidHom.compr₂ definition
[MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) : M →* N →* Q
Full source 
/-- The expression `fun m n ↦ g (f m n)` as a `MonoidHom`. -/
@[to_additive
      "The expression `fun m n ↦ g (f m n)` as an `AddMonoidHom`.

      This also exists as a `LinearMap` version, `LinearMap.compr₂`"]
def compr₂ [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P)
    (g : P →* Q) : M →* N →* Q :=
  (compHom g).comp f
Composition of a bivariate monoid homomorphism with a monoid homomorphism
Informal description
Given monoids \( M \), \( N \), \( P \), and \( Q \) with \( P \) and \( Q \) commutative, the function `MonoidHom.compr₂` takes a monoid homomorphism \( f \colon M \to^* N \to^* P \) and a monoid homomorphism \( g \colon P \to^* Q \), and returns the monoid homomorphism \( M \to^* N \to^* Q \) defined by \( (m, n) \mapsto g(f(m, n)) \). This operation effectively composes \( g \) with the bivariate homomorphism \( f \).
MonoidHom.compr₂_apply theorem
[MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) (m : M) (n : N) : (compr₂ f g) m n = g (f m n)
Full source 
@[to_additive (attr := simp)]
theorem compr₂_apply [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P)
    (g : P →* Q) (m : M) (n : N) : (compr₂ f g) m n = g (f m n) :=
  rfl
Evaluation of Composed Bivariate Monoid Homomorphism
Informal description
Let $M$ and $N$ be monoids, and let $P$ and $Q$ be commutative monoids. Given a monoid homomorphism $f \colon M \to N \to P$ and a monoid homomorphism $g \colon P \to Q$, the composition $\text{compr}_2(f, g) \colon M \to N \to Q$ satisfies $\text{compr}_2(f, g)(m, n) = g(f(m, n))$ for all $m \in M$ and $n \in N$.