Iterates of monoid and ring homomorphisms

Iterate of a monoid/ring homomorphism is a monoid/ring homomorphism but it has a wrong type, so Lean can't apply lemmas like MonoidHom.map_one to f^[n] 1. Though it is possible to define a monoid structure on the endomorphisms, quite often we do not want to convert from M →* M to Monoid.End M and from f^[n] to f^n just to apply a simple lemma.

So, we restate standard map_* lemmas under names iterate_map_*.

We also prove formulas for iterates of add/mul left/right.

Tags

homomorphism, iterate

theorem hom_coe_pow {M : Type u_1} {F : Type u_5} [Monoid F] (c : F → M → M) (h1 : c 1 = id) (hmul : ∀ (f g : F), c (f * g) = c f ∘ c g) (f : F) (n : ℕ) : c (f ^ n) = (c f)^[n]

An auxiliary lemma that can be used to prove ⇑(f ^ n) = ⇑f^[n].

@[simp]

theorem iterate_map_add {M : Type u_5} {F : Type u_6} [Add M] [FunLike F M M] [AddHomClass F M M] (f : F) (n : ℕ) (x : M) (y : M) : (⇑f)^[n] (x + y) = (⇑f)^[n] x + (⇑f)^[n] y

@[simp]

theorem iterate_map_mul {M : Type u_5} {F : Type u_6} [Mul M] [FunLike F M M] [MulHomClass F M M] (f : F) (n : ℕ) (x : M) (y : M) : (⇑f)^[n] (x * y) = (⇑f)^[n] x * (⇑f)^[n] y

@[simp]

theorem iterate_map_zero {M : Type u_5} {F : Type u_6} [Zero M] [FunLike F M M] [ZeroHomClass F M M] (f : F) (n : ℕ) : (⇑f)^[n] 0 = 0

@[simp]

theorem iterate_map_one {M : Type u_5} {F : Type u_6} [One M] [FunLike F M M] [OneHomClass F M M] (f : F) (n : ℕ) : (⇑f)^[n] 1 = 1

@[simp]

theorem iterate_map_neg {M : Type u_5} {F : Type u_6} [AddGroup M] [FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ) (x : M) : (⇑f)^[n] (-x) = -(⇑f)^[n] x

@[simp]

theorem iterate_map_inv {M : Type u_5} {F : Type u_6} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) : (⇑f)^[n] x⁻¹ = ((⇑f)^[n] x)⁻¹

@[simp]

theorem iterate_map_sub {M : Type u_5} {F : Type u_6} [AddGroup M] [FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (y : M) : (⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y

@[simp]

theorem iterate_map_div {M : Type u_5} {F : Type u_6} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (y : M) : (⇑f)^[n] (x / y) = (⇑f)^[n] x / (⇑f)^[n] y

@[simp]

theorem iterate_map_nsmul {M : Type u_5} {F : Type u_6} [AddMonoid M] [FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℕ) : (⇑f)^[n] (k • x) = k • (⇑f)^[n] x

@[simp]

theorem iterate_map_pow {M : Type u_5} {F : Type u_6} [Monoid M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℕ) : (⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k

@[simp]

theorem iterate_map_zsmul {M : Type u_5} {F : Type u_6} [AddGroup M] [FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℤ) : (⇑f)^[n] (k • x) = k • (⇑f)^[n] x

@[simp]

theorem iterate_map_zpow {M : Type u_5} {F : Type u_6} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) (k : ℤ) : (⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k

theorem MonoidHom.coe_pow {M : Type u_5} [CommMonoid M] (f : Monoid.End M) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem Monoid.End.coe_pow {M : Type u_5} [Monoid M] (f : Monoid.End M) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem AddMonoid.End.coe_pow {A : Type u_5} [AddMonoid A] (f : AddMonoid.End A) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem RingHom.coe_pow {R : Type u_5} [Semiring R] (f : R →+* R) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

@[simp]

theorem vadd_iterate {G : Type u_3} {H : Type u_4} [AddMonoid G] (a : G) (n : ℕ) [AddAction G H] : (fun (x : H) => a +ᵥ x)^[n] = fun (x : H) => n • a +ᵥ x

@[simp]

theorem smul_iterate {G : Type u_3} {H : Type u_4} [Monoid G] (a : G) (n : ℕ) [MulAction G H] : (fun (x : H) => a • x)^[n] = fun (x : H) => a ^ n • x

theorem vadd_iterate_apply {G : Type u_3} {H : Type u_4} [AddMonoid G] (a : G) (n : ℕ) [AddAction G H] {b : H} : (fun (x : H) => a +ᵥ x)^[n] b = n • a +ᵥ b

theorem smul_iterate_apply {G : Type u_3} {H : Type u_4} [Monoid G] (a : G) (n : ℕ) [MulAction G H] {b : H} : (fun (x : H) => a • x)^[n] b = a ^ n • b

@[simp]

theorem add_left_iterate {G : Type u_3} [AddMonoid G] (a : G) (n : ℕ) : (fun (x : G) => a + x)^[n] = fun (x : G) => n • a + x

@[simp]

theorem mul_left_iterate {G : Type u_3} [Monoid G] (a : G) (n : ℕ) : (fun (x : G) => a * x)^[n] = fun (x : G) => a ^ n * x

@[simp]

theorem add_right_iterate {G : Type u_3} [AddMonoid G] (a : G) (n : ℕ) : (fun (x : G) => x + a)^[n] = fun (x : G) => x + n • a

@[simp]

theorem mul_right_iterate {G : Type u_3} [Monoid G] (a : G) (n : ℕ) : (fun (x : G) => x * a)^[n] = fun (x : G) => x * a ^ n

theorem add_right_iterate_apply_zero {G : Type u_3} [AddMonoid G] (a : G) (n : ℕ) : (fun (x : G) => x + a)^[n] 0 = n • a

theorem mul_right_iterate_apply_one {G : Type u_3} [Monoid G] (a : G) (n : ℕ) : (fun (x : G) => x * a)^[n] 1 = a ^ n

@[simp]

theorem nsmul_iterate {G : Type u_3} [AddMonoid G] (n : ℕ) (j : ℕ) : (fun (x : G) => n • x)^[j] = fun (x : G) => n ^ j • x

@[simp]

theorem pow_iterate {G : Type u_3} [Monoid G] (n : ℕ) (j : ℕ) : (fun (x : G) => x ^ n)^[j] = fun (x : G) => x ^ n ^ j

@[simp]

theorem zsmul_iterate {G : Type u_3} [AddGroup G] (n : ℤ) (j : ℕ) : (fun (x : G) => n • x)^[j] = fun (x : G) => n ^ j • x

@[simp]

theorem zpow_iterate {G : Type u_3} [Group G] (n : ℤ) (j : ℕ) : (fun (x : G) => x ^ n)^[j] = fun (x : G) => x ^ n ^ j

theorem AddSemiconjBy.function_semiconj_add_left {G : Type u_3} [AddSemigroup G] {a : G} {b : G} {c : G} (h : AddSemiconjBy a b c) : Function.Semiconj (fun (x : G) => a + x) (fun (x : G) => b + x) fun (x : G) => c + x

theorem SemiconjBy.function_semiconj_mul_left {G : Type u_3} [Semigroup G] {a : G} {b : G} {c : G} (h : SemiconjBy a b c) : Function.Semiconj (fun (x : G) => a * x) (fun (x : G) => b * x) fun (x : G) => c * x

theorem AddCommute.function_commute_add_left {G : Type u_3} [AddSemigroup G] {a : G} {b : G} (h : AddCommute a b) : Function.Commute (fun (x : G) => a + x) fun (x : G) => b + x

theorem Commute.function_commute_mul_left {G : Type u_3} [Semigroup G] {a : G} {b : G} (h : Commute a b) : Function.Commute (fun (x : G) => a * x) fun (x : G) => b * x

theorem AddSemiconjBy.function_semiconj_add_right_swap {G : Type u_3} [AddSemigroup G] {a : G} {b : G} {c : G} (h : AddSemiconjBy a b c) : Function.Semiconj (fun (x : G) => x + a) (fun (x : G) => x + c) fun (x : G) => x + b

theorem SemiconjBy.function_semiconj_mul_right_swap {G : Type u_3} [Semigroup G] {a : G} {b : G} {c : G} (h : SemiconjBy a b c) : Function.Semiconj (fun (x : G) => x * a) (fun (x : G) => x * c) fun (x : G) => x * b

theorem AddCommute.function_commute_add_right {G : Type u_3} [AddSemigroup G] {a : G} {b : G} (h : AddCommute a b) : Function.Commute (fun (x : G) => x + a) fun (x : G) => x + b

theorem Commute.function_commute_mul_right {G : Type u_3} [Semigroup G] {a : G} {b : G} (h : Commute a b) : Function.Commute (fun (x : G) => x * a) fun (x : G) => x * b