Documentation

Mathlib.Algebra.Group.Hom.Instances

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 ZeroHom.instNatSMul {M : Type uM} {N : Type uN} [Zero M] [AddMonoid N] :

SMul ℕ (ZeroHom M N)

Equations

instance AddMonoidHom.instNatSMul {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] :

SMul ℕ (M →+ N)

Equations

instance OneHom.instPow {M : Type uM} {N : Type uN} [One M] [Monoid N] :

Pow (OneHom M N) ℕ

Equations

instance MonoidHom.instPow {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] :

Pow (M →* N) ℕ

Equations

@[simp]

theorem OneHom.pow_apply {M : Type uM} {N : Type uN} [One M] [Monoid N] (f : OneHom M N) (n : ℕ) (x : M) :

(f ^ n) x = f x ^ n

@[simp]

theorem ZeroHom.nsmul_apply {M : Type uM} {N : Type uN} [Zero M] [AddMonoid N] (f : ZeroHom M N) (n : ℕ) (x : M) :

(n • f) x = n • f x

@[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 OneHom.instMonoid {M : Type uM} {N : Type uN} [One M] [Monoid N] :

Monoid (OneHom M N)

OneHom M N is a Monoid if N is.

Equations

instance ZeroHom.instAddMonoid {M : Type uM} {N : Type uN} [Zero M] [AddMonoid N] :

AddMonoid (ZeroHom M N)

ZeroHom M N is an AddMonoid if N is.

Equations

instance OneHom.instCommMonoid {M : Type uM} {N : Type uN} [One M] [CommMonoid N] :

CommMonoid (OneHom M N)

OneHom M N is a CommMonoid if N is commutative.

Equations

instance ZeroHom.instAddCommMonoid {M : Type uM} {N : Type uN} [Zero M] [AddCommMonoid N] :

AddCommMonoid (ZeroHom M N)

ZeroHom M N is an AddCommMonoid if N is commutative.

Equations

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

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

instance ZeroHom.instIntSMul {M : Type uM} {N : Type uN} [Zero M] [AddGroup N] :

SMul ℤ (ZeroHom M N)

Equations

instance AddMonoidHom.instIntSMul {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommGroup N] :

SMul ℤ (M →+ N)

Equations

instance OneHom.instIntPow {M : Type uM} {N : Type uN} [One M] [Group N] :

Pow (OneHom M N) ℤ

Equations

instance MonoidHom.instIntPow {M : Type uM} {N : Type uN} [MulOneClass M] [CommGroup N] :

Pow (M →* N) ℤ

Equations

@[simp]

theorem OneHom.zpow_apply {M : Type uM} {N : Type uN} [One M] [Group N] (f : OneHom M N) (z : ℤ) (x : M) :

(f ^ z) x = f x ^ z

@[simp]

theorem ZeroHom.zsmul_apply {M : Type uM} {N : Type uN} [Zero M] [AddGroup N] (f : ZeroHom M N) (z : ℤ) (x : M) :

(z • f) x = z • f x

@[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 OneHom.instGroup {M : Type uM} {N : Type uN} [One M] [Group N] :

Group (OneHom M N)

If G is a group, then so is OneHom M G.

Equations

instance ZeroHom.instAddGroup {M : Type uM} {N : Type uN} [Zero M] [AddGroup N] :

AddGroup (ZeroHom M N)

If G is an additive group, then so is ZeroHom M G.

Equations

instance OneHom.instCommGroup {M : Type uM} {N : Type uN} [One M] [CommGroup N] :

CommGroup (OneHom M N)

If G is a commutative group, then so is OneHom M G.

Equations

instance ZeroHom.instAddCommGroup {M : Type uM} {N : Type uN} [Zero M] [AddCommGroup N] :

AddCommGroup (ZeroHom M N)

If G is an additive commutative group, then so is ZeroHom M G.

Equations

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

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

instance instIsLeftCancelMulOneHom {M : Type uM} {N : Type uN} [One M] [MulOneClass N] [IsLeftCancelMul N] :

IsLeftCancelMul (OneHom M N)

instance instIsLeftCancelAddZeroHom {M : Type uM} {N : Type uN} [Zero M] [AddZeroClass N] [IsLeftCancelAdd N] :

IsLeftCancelAdd (ZeroHom M N)

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 instIsRightCancelMulOneHom {M : Type uM} {N : Type uN} [One M] [MulOneClass N] [IsRightCancelMul N] :

IsRightCancelMul (OneHom M N)

instance instIsRightCancelAddZeroHom {M : Type uM} {N : Type uN} [Zero M] [AddZeroClass N] [IsRightCancelAdd N] :

IsRightCancelAdd (ZeroHom 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 instIsCancelMulOneHom {M : Type uM} {N : Type uN} [One M] [MulOneClass N] [IsCancelMul N] :

IsCancelMul (OneHom M N)

instance instIsCancelAddZeroHom {M : Type uM} {N : Type uN} [Zero M] [AddZeroClass N] [IsCancelAdd N] :

IsCancelAdd (ZeroHom 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

@[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

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

IntCast (AddMonoid.End M)

Equations

@[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

Instances For

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

Instances For

@[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

Instances For

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

Instances For

@[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

@[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

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

Instances For

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

Instances For

@[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

Instances For

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

Instances For

@[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

Instances For

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

Instances For

@[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

@[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

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

Instances For

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

Instances For

@[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

Instances For

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

Instances For

@[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)