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.

instance AddMonoidHom.instNatSMul {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] : SMul ℕ (M →+ N)

Equations

• AddMonoidHom.instNatSMul = { smul := fun (a : ℕ) (f : M →+ N) => { toFun := a • ⇑f, map_zero' := ⋯, map_add' := ⋯ } }

instance MonoidHom.instPow {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] : Pow (M →* N) ℕ

Equations

• MonoidHom.instPow = { pow := fun (f : M →* N) (n : ℕ) => { toFun := ⇑f ^ n, map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem MonoidHom.pow_apply {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] (f : M →* N) (n : ℕ) (x : M) : (f ^ n) x = f x ^ n

@[simp]

theorem AddMonoidHom.nsmul_apply {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) (n : ℕ) (x : M) : (n • f) x = n • f x

instance MonoidHom.instCommMonoid {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] : CommMonoid (M →* N)

(M →* N) is a CommMonoid if N is commutative.

Equations

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

instance AddMonoidHom.instAddCommMonoid {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] : AddCommMonoid (M →+ N)

(M →+ N) is an AddCommMonoid if N is commutative.

Equations

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

instance AddMonoidHom.instIntSMul {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommGroup N] : SMul ℤ (M →+ N)

Equations

• AddMonoidHom.instIntSMul = { smul := fun (a : ℤ) (f : M →+ N) => { toFun := a • ⇑f, map_zero' := ⋯, map_add' := ⋯ } }

instance MonoidHom.instIntPow {M : Type uM} {N : Type uN} [MulOneClass M] [CommGroup N] : Pow (M →* N) ℤ

Equations

• MonoidHom.instIntPow = { pow := fun (f : M →* N) (n : ℤ) => { toFun := ⇑f ^ n, map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem MonoidHom.zpow_apply {M : Type uM} {N : Type uN} [MulOneClass M] [CommGroup N] (f : M →* N) (z : ℤ) (x : M) : (f ^ z) x = f x ^ z

@[simp]

theorem AddMonoidHom.zsmul_apply {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommGroup N] (f : M →+ N) (z : ℤ) (x : M) : (z • f) x = z • f x

instance MonoidHom.instCommGroup {M : Type uM} {N : Type uN} [MulOneClass M] [CommGroup N] : CommGroup (M →* N)

If G is a commutative group, then M →* G is a commutative group too.

Equations

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

instance AddMonoidHom.instAddCommGroup {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommGroup N] : AddCommGroup (M →+ N)

If G is an additive commutative group, then M →+ G is an additive commutative group too.

Equations

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

instance instIsLeftCancelMulMonoidHom {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] [IsLeftCancelMul N] : IsLeftCancelMul (M →* N)

instance instIsLeftCancelAddAddMonoidHom {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] [IsLeftCancelAdd N] : IsLeftCancelAdd (M →+ N)

instance instIsRightCancelMulMonoidHom {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] [IsRightCancelMul N] : IsRightCancelMul (M →* N)

instance instIsRightCancelAddAddMonoidHom {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] [IsRightCancelAdd N] : IsRightCancelAdd (M →+ N)

instance instIsCancelMulMonoidHom {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] [IsCancelMul N] : IsCancelMul (M →* N)

instance instIsCancelAddAddMonoidHom {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] [IsCancelAdd N] : IsCancelAdd (M →+ N)

instance AddMonoid.End.instAddCommMonoid {M : Type uM} [AddCommMonoid M] : AddCommMonoid (AddMonoid.End M)

Equations

• AddMonoid.End.instAddCommMonoid = AddMonoidHom.instAddCommMonoid

@[simp]

theorem AddMonoid.End.zero_apply {M : Type uM} [AddCommMonoid M] (m : M) : 0 m = 0

theorem AddMonoid.End.one_apply {M : Type uM} [AddZeroClass M] (m : M) : 1 m = m

instance AddMonoid.End.instAddCommGroup {M : Type uM} [AddCommGroup M] : AddCommGroup (AddMonoid.End M)

Equations

• AddMonoid.End.instAddCommGroup = AddMonoidHom.instAddCommGroup

instance AddMonoid.End.instIntCast {M : Type uM} [AddCommGroup M] : IntCast (AddMonoid.End M)

Equations

• AddMonoid.End.instIntCast = { intCast := fun (z : ℤ) => z • 1 }

@[simp]

theorem AddMonoid.End.intCast_apply {M : Type uM} [AddCommGroup M] (z : ℤ) (m : M) : ↑z m = z • m

See also AddMonoid.End.intCast_def.

Morphisms of morphisms

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

theorem MonoidHom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} {f g : M →* N →* P} : f = g ↔ ∀ (x : M) (y : N), (f x) y = (g x) y

theorem AddMonoidHom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} {f g : M →+ N →+ P} : f = g ↔ ∀ (x : M) (y : N), (f x) y = (g x) y

def MonoidHom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P} (f : M →* N →* P) : N →* M →* P

flip arguments of f : M →* N →* P

Equations

• f.flip = { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) : N →+ M →+ P

flip arguments of f : M →+ N →+ P

Equations

• f.flip = { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} (f : M →* N →* P) (x : M) (y : N) : (f.flip y) x = (f x) y

@[simp]

theorem AddMonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} (f : M →+ N →+ P) (x : M) (y : N) : (f.flip y) x = (f x) y

theorem MonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} (f : M →* N →* P) (n : N) : (f 1) n = 1

theorem AddMonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} (f : M →+ N →+ P) (n : N) : (f 0) n = 0

theorem MonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) : (f (m₁ * m₂)) n = (f m₁) n * (f m₂) n

theorem AddMonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N) : (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n

theorem MonoidHom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : Group M} {x✝¹ : MulOneClass N} {x✝² : CommGroup P} (f : M →* N →* P) (m : M) (n : N) : (f m⁻¹) n = ((f m) n)⁻¹

theorem AddMonoidHom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddGroup M} {x✝¹ : AddZeroClass N} {x✝² : AddCommGroup P} (f : M →+ N →+ P) (m : M) (n : N) : (f (-m)) n = -(f m) n

theorem MonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : Group M} {x✝¹ : MulOneClass N} {x✝² : CommGroup P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) : (f (m₁ / m₂)) n = (f m₁) n / (f m₂) n

theorem AddMonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddGroup M} {x✝¹ : AddZeroClass N} {x✝² : AddCommGroup P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N) : (f (m₁ - m₂)) n = (f m₁) n - (f m₂) n

def MonoidHom.eval {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] : M →* (M →* N) →* N

Evaluation of a MonoidHom at a point as a monoid homomorphism. See also MonoidHom.apply for the evaluation of any function at a point.

Equations

• MonoidHom.eval = (MonoidHom.id (M →* N)).flip

def AddMonoidHom.eval {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] : M →+ (M →+ N) →+ N

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.

Equations

• AddMonoidHom.eval = (AddMonoidHom.id (M →+ N)).flip

@[simp]

theorem MonoidHom.eval_apply_apply {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] (y : M) (x : M →* N) : (eval y) x = x y

@[simp]

theorem AddMonoidHom.eval_apply_apply {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] (y : M) (x : M →+ N) : (eval y) x = x y

def MonoidHom.compHom' {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) : (N →* P) →* M →* P

The expression fun g m ↦ g (f m) as a MonoidHom. Equivalently, (fun g ↦ MonoidHom.comp g f) as a MonoidHom.

Equations

• f.compHom' = (MonoidHom.eval.comp f).flip

def AddMonoidHom.compHom' {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ N) : (N →+ P) →+ M →+ P

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.

Equations

• f.compHom' = (AddMonoidHom.eval.comp f).flip

@[simp]

theorem MonoidHom.compHom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) (y : N →* P) (x : M) : (f.compHom' y) x = y (f x)

@[simp]

theorem AddMonoidHom.compHom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ N) (y : N →+ P) (x : M) : (f.compHom' y) x = y (f x)

def MonoidHom.compHom {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [CommMonoid N] [CommMonoid P] : (N →* P) →* (M →* N) →* M →* P

Composition of monoid morphisms (MonoidHom.comp) as a monoid morphism.

Note that unlike MonoidHom.comp_hom' this requires commutativity of N.

Equations

• MonoidHom.compHom = { toFun := fun (g : N →* P) => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.compHom {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] : (N →+ P) →+ (M →+ N) →+ M →+ P

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.

Equations

• AddMonoidHom.compHom = { toFun := fun (g : N →+ P) => { toFun := g.comp, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.compHom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (hmn : M →+ N) : (compHom g) hmn = g.comp hmn

@[simp]

theorem MonoidHom.compHom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [CommMonoid N] [CommMonoid P] (g : N →* P) (hmn : M →* N) : (compHom g) hmn = g.comp hmn

def MonoidHom.flipHom {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} : (M →* N →* P) →* N →* M →* P

Flipping arguments of monoid morphisms (MonoidHom.flip) as a monoid morphism.

Equations

• MonoidHom.flipHom = { toFun := MonoidHom.flip, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.flipHom {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} : (M →+ N →+ P) →+ N →+ M →+ P

Flipping arguments of additive monoid morphisms (AddMonoidHom.flip) as an additive monoid morphism.

Equations

• AddMonoidHom.flipHom = { toFun := AddMonoidHom.flip, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : AddZeroClass M} {x✝¹ : AddZeroClass N} {x✝² : AddCommMonoid P} (f : M →+ N →+ P) : flipHom f = f.flip

@[simp]

theorem MonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} {x✝ : MulOneClass M} {x✝¹ : MulOneClass N} {x✝² : CommMonoid P} (f : M →* N →* P) : flipHom f = f.flip

def MonoidHom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) : M →* Q →* P

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.

Equations

• f.compl₂ g = g.compHom'.comp f

def AddMonoidHom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N) : M →+ Q →+ P

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₂

Equations

• f.compl₂ g = g.compHom'.comp f

@[simp]

theorem MonoidHom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) : ((f.compl₂ g) m) q = (f m) (g q)

@[simp]

theorem AddMonoidHom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N) (m : M) (q : Q) : ((f.compl₂ g) m) q = (f m) (g q)

def MonoidHom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) : M →* N →* Q

The expression fun m n ↦ g (f m n) as a MonoidHom.

Equations

• f.compr₂ g = (MonoidHom.compHom g).comp f

def AddMonoidHom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q) : M →+ N →+ Q

The expression fun m n ↦ g (f m n) as an AddMonoidHom.

This also exists as a LinearMap version, LinearMap.compr₂

Equations

• f.compr₂ g = (AddMonoidHom.compHom g).comp f

@[simp]

theorem MonoidHom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) (m : M) (n : N) : ((f.compr₂ g) m) n = g ((f m) n)

@[simp]

theorem AddMonoidHom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q) (m : M) (n : N) : ((f.compr₂ g) m) n = g ((f m) n)