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.

theorem AddMonoidHom.addCommMonoid.proof_6 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) : (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) 0 f = 0

theorem AddMonoidHom.addCommMonoid.proof_8 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] : ∀ (a b : M →+ N), a + b = b + a

theorem AddMonoidHom.addCommMonoid.proof_4 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (n : ℕ) (f : M →+ N) : n • ↑f 0 = 0

theorem AddMonoidHom.addCommMonoid.proof_5 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (n : ℕ) (f : M →+ N) (x : M) (y : M) : n • ↑f (x + y) = n • ↑f x + n • ↑f y

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

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

theorem AddMonoidHom.addCommMonoid.proof_7 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (n : ℕ) (f : M →+ N) : (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) (n + 1) f = f + (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) n f

theorem AddMonoidHom.addCommMonoid.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] : ∀ (a : M →+ N), 0 + a = a

theorem AddMonoidHom.addCommMonoid.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] : ∀ (a b c : M →+ N), a + b + c = a + (b + c)

theorem AddMonoidHom.addCommMonoid.proof_3 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] : ∀ (a : M →+ N), a + 0 = a

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

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

instance AddMonoidHom.addCommGroup {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] : AddCommGroup (M →+ G)

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

theorem AddMonoidHom.addCommGroup.proof_8 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (a : M →+ G) (b : M →+ G) : a + b = b + a

theorem AddMonoidHom.addCommGroup.proof_1 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] : ∀ (a b : M →+ G), a - b = a + -b

theorem AddMonoidHom.addCommGroup.proof_2 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ℤ) (f : M →+ G) : n • ↑f 0 = 0

theorem AddMonoidHom.addCommGroup.proof_7 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] : ∀ (a : M →+ G), -a + a = 0

theorem AddMonoidHom.addCommGroup.proof_5 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ℕ) (f : M →+ G) : (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) (Int.ofNat (Nat.succ n)) f = f + (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) (Int.ofNat n) f

theorem AddMonoidHom.addCommGroup.proof_4 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) : (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) 0 f = 0

theorem AddMonoidHom.addCommGroup.proof_3 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ℤ) (f : M →+ G) (x : M) (y : M) : n • ↑f (x + y) = n • ↑f x + n • ↑f y

theorem AddMonoidHom.addCommGroup.proof_6 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ℕ) (f : M →+ G) : (fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) (Int.negSucc n) f = -(fun n f => { toZeroHom := { toFun := fun x => n • ↑f x, map_zero' := (_ : n • ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), n • ↑f (x + y) = n • ↑f x + n • ↑f y) }) (↑(Nat.succ n)) f

instance MonoidHom.commGroup {M : Type u_1} {G : Type u_2} [MulOneClass M] [CommGroup G] : CommGroup (M →* G)

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

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

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

@[simp]

theorem AddMonoid.End.natCast_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) (m : M) : ↑↑n m = n • m

See also AddMonoid.End.natCast_def.

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

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

@[simp]

theorem AddMonoid.End.int_cast_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 AddMonoidHom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} {f g : M →+ N →+ P}, f = g ↔ ∀ (x_3 : M) (y : N), ↑(↑f x_3) y = ↑(↑g x_3) y

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

theorem AddMonoidHom.flip.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y : N) (x₁ : M) (x₂ : M) : ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y

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

theorem AddMonoidHom.flip.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y : N) : ↑(↑f 0) y = 0

theorem AddMonoidHom.flip.proof_4 {M : Type u_1} {N : Type u_3} {P : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y₁ : N) (y₂ : N) : ZeroHom.toFun { toFun := fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }, map_zero' := (_ : (fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }) 0 = 0) } (y₁ + y₂) = ZeroHom.toFun { toFun := fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }, map_zero' := (_ : (fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }) 0 = 0) } y₁ + ZeroHom.toFun { toFun := fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }, map_zero' := (_ : (fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }) 0 = 0) } y₂

theorem AddMonoidHom.flip.proof_3 {M : Type u_1} {N : Type u_3} {P : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) : (fun y => { toZeroHom := { toFun := fun x => ↑(↑f x) y, map_zero' := (_ : ↑(↑f 0) y = 0) }, map_add' := (_ : ∀ (x₁ x₂ : M), ↑(↑f (x₁ + x₂)) y = ↑(↑f x₁) y + ↑(↑f x₂) y) }) 0 = 0

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

@[simp]

theorem AddMonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (x_3 : M) (y : N), ↑(↑(AddMonoidHom.flip f) y) x_3 = ↑(↑f x_3) y

@[simp]

theorem MonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (x_3 : M) (y : N), ↑(↑(MonoidHom.flip f) y) x_3 = ↑(↑f x_3) y

theorem AddMonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (n : N), ↑(↑f 0) n = 0

theorem MonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (n : N), ↑(↑f 1) n = 1

theorem AddMonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), ↑(↑f (m₁ + m₂)) n = ↑(↑f m₁) n + ↑(↑f m₂) n

theorem MonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), ↑(↑f (m₁ * m₂)) n = ↑(↑f m₁) n * ↑(↑f m₂) n

theorem AddMonoidHom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m : M) (n : N), ↑(↑f (-m)) n = -↑(↑f m) n

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

theorem AddMonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), ↑(↑f (m₁ - m₂)) n = ↑(↑f m₁) n - ↑(↑f m₂) n

theorem MonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), ↑(↑f (m₁ / m₂)) n = ↑(↑f m₁) n / ↑(↑f m₂) n

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.

@[simp]

theorem MonoidHom.eval_apply_apply {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] (y : M) (x : M →* N) : ↑(↑MonoidHom.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) : ↑(↑AddMonoidHom.eval y) x = ↑x y

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.

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.

@[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) : ↑(↑(AddMonoidHom.compHom' f) y) x = ↑y (↑f x)

@[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) : ↑(↑(MonoidHom.compHom' f) y) x = ↑y (↑f x)

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.

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.

theorem AddMonoidHom.compHom.proof_2 {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] : (fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }) 0 = 0

theorem AddMonoidHom.compHom.proof_1 {M : Type u_1} {N : Type u_3} {P : Type u_2} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) : AddMonoidHom.comp g 0 = 0

theorem AddMonoidHom.compHom.proof_3 {M : Type u_3} {N : Type u_2} {P : Type u_1} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g₁ : N →+ P) (g₂ : N →+ P) : ZeroHom.toFun { toFun := fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }, map_zero' := (_ : (fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }) 0 = 0) } (g₁ + g₂) = ZeroHom.toFun { toFun := fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }, map_zero' := (_ : (fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }) 0 = 0) } g₁ + ZeroHom.toFun { toFun := fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }, map_zero' := (_ : (fun g => { toZeroHom := { toFun := AddMonoidHom.comp g, map_zero' := (_ : AddMonoidHom.comp g 0 = 0) }, map_add' := (_ : ∀ (f₁ f₂ : M →+ N), AddMonoidHom.comp g (f₁ + f₂) = AddMonoidHom.comp g f₁ + AddMonoidHom.comp g f₂) }) 0 = 0) } g₂

@[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) : ↑(↑AddMonoidHom.compHom g) hmn = AddMonoidHom.comp g 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) : ↑(↑MonoidHom.compHom g) hmn = MonoidHom.comp g hmn

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.

theorem AddMonoidHom.flipHom.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}, AddMonoidHom.flip 0 = AddMonoidHom.flip 0

theorem AddMonoidHom.flipHom.proof_2 {M : Type u_3} {N : Type u_1} {P : Type u_2} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (x_3 x_4 : M →+ N →+ P), ZeroHom.toFun { toFun := AddMonoidHom.flip, map_zero' := (_ : AddMonoidHom.flip 0 = AddMonoidHom.flip 0) } (x_3 + x_4) = ZeroHom.toFun { toFun := AddMonoidHom.flip, map_zero' := (_ : AddMonoidHom.flip 0 = AddMonoidHom.flip 0) } (x_3 + x_4)

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

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

@[simp]

theorem MonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P), ↑MonoidHom.flipHom f = MonoidHom.flip f

@[simp]

theorem AddMonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} : ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P), ↑AddMonoidHom.flipHom f = AddMonoidHom.flip f

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

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

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₂

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.

@[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) : ↑(↑(AddMonoidHom.compl₂ f g) m) q = ↑(↑f m) (↑g q)

@[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) : ↑(↑(MonoidHom.compl₂ f g) m) q = ↑(↑f m) (↑g q)

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₂

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.

@[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) : ↑(↑(AddMonoidHom.compr₂ f g) m) n = ↑g (↑(↑f m) n)

@[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) : ↑(↑(MonoidHom.compr₂ f g) m) n = ↑g (↑(↑f m) n)

Miscellaneous definitions

Due to the fact this file imports Algebra.GroupPower.Basic, it is not possible to import it in some of the lower-level files like Algebra.Ring.Basic. The following lemmas should be rehomed if the import structure permits them to be.

def AddMonoidHom.mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R

Multiplication of an element of a (semi)ring is an AddMonoidHom in both arguments.

This is a more-strongly bundled version of AddMonoidHom.mulLeft and AddMonoidHom.mulRight.

Stronger versions of this exists for algebras as LinearMap.mul, NonUnitalAlgHom.mul and Algebra.lmul.

theorem AddMonoidHom.mul_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : R) (y : R) : ↑(↑AddMonoidHom.mul x) y = x * y

@[simp]

theorem AddMonoidHom.coe_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ↑AddMonoidHom.mul = AddMonoidHom.mulLeft

@[simp]

theorem AddMonoidHom.coe_flip_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ↑(AddMonoidHom.flip AddMonoidHom.mul) = AddMonoidHom.mulRight

theorem AddMonoidHom.map_mul_iff {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →+ S) : (∀ (x y : R), ↑f (x * y) = ↑f x * ↑f y) ↔ AddMonoidHom.compr₂ AddMonoidHom.mul f = AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul f) f

An AddMonoidHom preserves multiplication if pre- and post- composition with AddMonoidHom.mul are equivalent. By converting the statement into an equality of AddMonoidHoms, this lemma allows various specialized ext lemmas about →+ to then be applied.

@[simp]

theorem AddMonoid.End.mulLeft_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : ∀ (x : R), ↑(↑AddMonoid.End.mulLeft r) x = r * x

def AddMonoid.End.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The left multiplication map: (a, b) ↦ a * b. See also AddMonoidHom.mulLeft.

@[simp]

theorem AddMonoid.End.mulRight_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (y : R) (x : R) : ↑(↑AddMonoid.End.mulRight y) x = x * y

def AddMonoid.End.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The right multiplication map: (a, b) ↦ b * a. See also AddMonoidHom.mulRight.