Additional lemmas about monoid and group homomorphisms

def nsmulAddMonoidHom {α : Type u_1} [AddCommMonoid α] (n : ℕ) : α →+ α

Multiplication by a natural n on a commutative additive monoid, considered as a morphism of additive monoids.

Equations

• nsmulAddMonoidHom n = { toFun := fun (x : α) => n • x, map_zero' := ⋯, map_add' := ⋯ }

theorem nsmulAddMonoidHom.proof_1 {α : Type u_1} [AddCommMonoid α] (n : ℕ) : n • 0 = 0

@[simp]

theorem nsmulAddMonoidHom_apply {α : Type u_1} [AddCommMonoid α] (n : ℕ) : ∀ (x : α), (nsmulAddMonoidHom n) x = n • x

@[simp]

theorem powMonoidHom_apply {α : Type u_1} [CommMonoid α] (n : ℕ) : ∀ (x : α), (powMonoidHom n) x = x ^ n

def powMonoidHom {α : Type u_1} [CommMonoid α] (n : ℕ) : α →* α

The nth power map on a commutative monoid for a natural n, considered as a morphism of monoids.

Equations

• powMonoidHom n = { toFun := fun (x : α) => x ^ n, map_one' := ⋯, map_mul' := ⋯ }

theorem zsmulAddGroupHom.proof_1 {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : n • 0 = 0

def zsmulAddGroupHom {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : α →+ α

Multiplication by an integer n on a commutative additive group, considered as an additive group homomorphism.

Equations

• zsmulAddGroupHom n = { toFun := fun (x : α) => n • x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem zpowGroupHom_apply {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) : ∀ (x : α), (zpowGroupHom n) x = x ^ n

@[simp]

theorem zsmulAddGroupHom_apply {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : ∀ (x : α), (zsmulAddGroupHom n) x = n • x

def zpowGroupHom {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) : α →* α

The n-th power map (for an integer n) on a commutative group, considered as a group homomorphism.

Equations

• zpowGroupHom n = { toFun := fun (x : α) => x ^ n, map_one' := ⋯, map_mul' := ⋯ }

def negAddMonoidHom {α : Type u_1} [SubtractionCommMonoid α] : α →+ α

Negation on a commutative additive group, considered as an additive monoid homomorphism.

Equations

• negAddMonoidHom = { toFun := Neg.neg, map_zero' := ⋯, map_add' := ⋯ }

theorem negAddMonoidHom.proof_1 {α : Type u_1} [SubtractionCommMonoid α] : -0 = 0

def invMonoidHom {α : Type u_1} [DivisionCommMonoid α] : α →* α

Inversion on a commutative group, considered as a monoid homomorphism.

Equations

• invMonoidHom = { toFun := Inv.inv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem coe_invMonoidHom {α : Type u_1} [DivisionCommMonoid α] : ⇑invMonoidHom = Inv.inv

@[simp]

theorem invMonoidHom_apply {α : Type u_1} [DivisionCommMonoid α] (a : α) : invMonoidHom a = a⁻¹

theorem AddHom.instAdd.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [AddCommSemigroup N] (f : AddHom M N) (g : AddHom M N) (x : M) (y : M) : f (x + y) + g (x + y) = f x + g x + (f y + g y)

instance AddHom.instAdd {M : Type u_2} {N : Type u_3} [Add M] [AddCommSemigroup N] : Add (AddHom M N)

Given two additive morphisms f, g to an additive commutative semigroup, f + g is the additive morphism sending x to f x + g x.

Equations

• AddHom.instAdd = { add := fun (f g : AddHom M N) => { toFun := fun (m : M) => f m + g m, map_add' := ⋯ } }

instance MulHom.instMul {M : Type u_2} {N : Type u_3} [Mul M] [CommSemigroup N] : Mul (M →ₙ* N)

Given two mul morphisms f, g to a commutative semigroup, f * g is the mul morphism sending x to f x * g x.

Equations

• MulHom.instMul = { mul := fun (f g : M →ₙ* N) => { toFun := fun (m : M) => f m * g m, map_mul' := ⋯ } }

@[simp]

theorem AddHom.add_apply {M : Type u_8} {N : Type u_9} [Add M] [AddCommSemigroup N] (f : AddHom M N) (g : AddHom M N) (x : M) : (f + g) x = f x + g x

@[simp]

theorem MulHom.mul_apply {M : Type u_8} {N : Type u_9} [Mul M] [CommSemigroup N] (f : M →ₙ* N) (g : M →ₙ* N) (x : M) : (f * g) x = f x * g x

theorem AddHom.add_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Add M] [Add N] [AddCommSemigroup P] (g₁ : AddHom N P) (g₂ : AddHom N P) (f : AddHom M N) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

theorem MulHom.mul_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Mul M] [Mul N] [CommSemigroup P] (g₁ : N →ₙ* P) (g₂ : N →ₙ* P) (f : M →ₙ* N) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

theorem AddHom.comp_add {M : Type u_2} {N : Type u_3} {P : Type u_4} [Add M] [AddCommSemigroup N] [AddCommSemigroup P] (g : AddHom N P) (f₁ : AddHom M N) (f₂ : AddHom M N) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

theorem MulHom.comp_mul {M : Type u_2} {N : Type u_3} {P : Type u_4} [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ : M →ₙ* N) (f₂ : M →ₙ* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

theorem injective_iff_map_eq_zero {F : Type u_7} {G : Type u_8} {H : Type u_9} [AddGroup G] [AddZeroClass H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see injective_iff_map_eq_zero'.

theorem injective_iff_map_eq_one {F : Type u_7} {G : Type u_8} {H : Type u_9} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) : Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see injective_iff_map_eq_one'.

theorem injective_iff_map_eq_zero' {F : Type u_7} {G : Type u_8} {H : Type u_9} [AddGroup G] [AddZeroClass H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 ↔ a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see injective_iff_map_eq_zero.

theorem injective_iff_map_eq_one' {F : Type u_7} {G : Type u_8} {H : Type u_9} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) : Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 ↔ a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see injective_iff_map_eq_one.

def AddMonoidHom.ofMapAddNeg {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) : G →+ H

Makes an additive group homomorphism from a proof that the map preserves the operation fun a b => a + -b. See also AddMonoidHom.ofMapSub for a version using fun a b => a - b.

Equations

• AddMonoidHom.ofMapAddNeg f map_div = AddMonoidHom.mk' f ⋯

theorem AddMonoidHom.ofMapAddNeg.proof_1 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) (x : G) (y : G) : f (x + y) = f x + f y

def MonoidHom.ofMapMulInv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) : G →* H

Makes a group homomorphism from a proof that the map preserves right division fun x y => x * y⁻¹. See also MonoidHom.of_map_div for a version using fun x y => x / y.

Equations

• MonoidHom.ofMapMulInv f map_div = MonoidHom.mk' f ⋯

@[simp]

theorem AddMonoidHom.coe_of_map_add_neg {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) : ⇑(AddMonoidHom.ofMapAddNeg f map_div) = f

@[simp]

theorem MonoidHom.coe_of_map_mul_inv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) : ⇑(MonoidHom.ofMapMulInv f map_div) = f

theorem AddMonoidHom.ofMapSub.proof_1 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) (a : G) (a : G) : f (a✝ + -a) = f a✝ + -f a

def AddMonoidHom.ofMapSub {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) : G →+ H

Define a morphism of additive groups given a map which respects difference.

Equations

• AddMonoidHom.ofMapSub f hf = AddMonoidHom.ofMapAddNeg f ⋯

def MonoidHom.ofMapDiv {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) : G →* H

Define a morphism of additive groups given a map which respects ratios.

Equations

• MonoidHom.ofMapDiv f hf = MonoidHom.ofMapMulInv f ⋯

@[simp]

theorem AddMonoidHom.coe_of_map_sub {G : Type u_5} [AddGroup G] {H : Type u_8} [AddGroup H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) : ⇑(AddMonoidHom.ofMapSub f hf) = f

@[simp]

theorem MonoidHom.coe_of_map_div {G : Type u_5} [Group G] {H : Type u_8} [Group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) : ⇑(MonoidHom.ofMapDiv f hf) = f

theorem AddMonoidHom.add.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) (g : M →+ N) (x : M) (y : M) : f (x + y) + g (x + y) = f x + g x + (f y + g y)

theorem AddMonoidHom.add.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) (g : M →+ N) : f 0 + g 0 = 0

instance AddMonoidHom.add {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] : Add (M →+ N)

Given two additive monoid morphisms f, g to an additive commutative monoid, f + g is the additive monoid morphism sending x to f x + g x.

Equations

• AddMonoidHom.add = { add := fun (f g : M →+ N) => { toFun := fun (m : M) => f m + g m, map_zero' := ⋯, map_add' := ⋯ } }

instance MonoidHom.mul {M : Type u_2} {N : Type u_3} [MulOneClass M] [CommMonoid N] : Mul (M →* N)

Given two monoid morphisms f, g to a commutative monoid, f * g is the monoid morphism sending x to f x * g x.

Equations

• MonoidHom.mul = { mul := fun (f g : M →* N) => { toFun := fun (m : M) => f m * g m, map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem AddMonoidHom.add_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) (g : M →+ N) (x : M) : (f + g) x = f x + g x

@[simp]

theorem MonoidHom.mul_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [CommMonoid N] (f : M →* N) (g : M →* N) (x : M) : (f * g) x = f x * g x

theorem AddMonoidHom.add_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddZeroClass M] [AddCommMonoid N] [AddZeroClass P] (g₁ : M →+ N) (g₂ : M →+ N) (f : P →+ M) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

theorem MonoidHom.mul_comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [MulOneClass M] [CommMonoid N] [MulOneClass P] (g₁ : M →* N) (g₂ : M →* N) (f : P →* M) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f

theorem AddMonoidHom.comp_add {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f₁ : M →+ N) (f₂ : M →+ N) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

theorem MonoidHom.comp_mul {M : Type u_2} {N : Type u_3} {P : Type u_4} [MulOneClass M] [CommMonoid N] [CommMonoid P] (g : N →* P) (f₁ : M →* N) (f₂ : M →* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

theorem AddMonoidHom.instNeg.proof_1 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) (a : M) (b : M) : (fun (g : M) => -f g) (a + b) = (fun (g : M) => -f g) a + (fun (g : M) => -f g) b

instance AddMonoidHom.instNeg {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] : Neg (M →+ G)

If f is an additive monoid homomorphism to an additive commutative group, then -f is the homomorphism sending x to -(f x).

Equations

• AddMonoidHom.instNeg = { neg := fun (f : M →+ G) => AddMonoidHom.mk' (fun (g : M) => -f g) ⋯ }

instance MonoidHom.instInv {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] : Inv (M →* G)

If f is a monoid homomorphism to a commutative group, then f⁻¹ is the homomorphism sending x to (f x)⁻¹.

Equations

• MonoidHom.instInv = { inv := fun (f : M →* G) => MonoidHom.mk' (fun (g : M) => (f g)⁻¹) ⋯ }

@[simp]

theorem AddMonoidHom.neg_apply {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) (x : M) : (-f) x = -f x

@[simp]

theorem MonoidHom.inv_apply {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] (f : M →* G) (x : M) : f⁻¹ x = (f x)⁻¹

@[simp]

theorem AddMonoidHom.neg_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommGroup G] (φ : N →+ G) (ψ : M →+ N) : (-φ).comp ψ = -φ.comp ψ

@[simp]

theorem MonoidHom.inv_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [MulOneClass M] [MulOneClass N] [CommGroup G] (φ : N →* G) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹

@[simp]

theorem AddMonoidHom.comp_neg {M : Type u_2} {G : Type u_5} {H : Type u_6} [AddZeroClass M] [AddCommGroup G] [AddCommGroup H] (φ : G →+ H) (ψ : M →+ G) : φ.comp (-ψ) = -φ.comp ψ

@[simp]

theorem MonoidHom.comp_inv {M : Type u_2} {G : Type u_5} {H : Type u_6} [MulOneClass M] [CommGroup G] [CommGroup H] (φ : G →* H) (ψ : M →* G) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

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

instance AddMonoidHom.instSub {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] : Sub (M →+ G)

If f and g are monoid homomorphisms to an additive commutative group, then f - g is the homomorphism sending x to (f x) - (g x).

Equations

• AddMonoidHom.instSub = { sub := fun (f g : M →+ G) => AddMonoidHom.mk' (fun (x : M) => f x - g x) ⋯ }

instance MonoidHom.instDiv {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] : Div (M →* G)

If f and g are monoid homomorphisms to a commutative group, then f / g is the homomorphism sending x to (f x) / (g x).

Equations

• MonoidHom.instDiv = { div := fun (f g : M →* G) => MonoidHom.mk' (fun (x : M) => f x / g x) ⋯ }

@[simp]

theorem AddMonoidHom.sub_apply {M : Type u_2} {G : Type u_5} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) (g : M →+ G) (x : M) : (f - g) x = f x - g x

@[simp]

theorem MonoidHom.div_apply {M : Type u_2} {G : Type u_5} [MulOneClass M] [CommGroup G] (f : M →* G) (g : M →* G) (x : M) : (f / g) x = f x / g x

@[simp]

theorem AddMonoidHom.sub_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommGroup G] (f : N →+ G) (g : N →+ G) (h : M →+ N) : (f - g).comp h = f.comp h - g.comp h

@[simp]

theorem MonoidHom.div_comp {M : Type u_2} {N : Type u_3} {G : Type u_5} [MulOneClass M] [MulOneClass N] [CommGroup G] (f : N →* G) (g : N →* G) (h : M →* N) : (f / g).comp h = f.comp h / g.comp h

@[simp]

theorem AddMonoidHom.comp_sub {M : Type u_2} {G : Type u_5} {H : Type u_6} [AddZeroClass M] [AddCommGroup G] [AddCommGroup H] (f : G →+ H) (g : M →+ G) (h : M →+ G) : f.comp (g - h) = f.comp g - f.comp h

@[simp]

theorem MonoidHom.comp_div {M : Type u_2} {G : Type u_5} {H : Type u_6} [MulOneClass M] [CommGroup G] [CommGroup H] (f : G →* H) (g : M →* G) (h : M →* G) : f.comp (g / h) = f.comp g / f.comp h