Documentation

Mathlib.Algebra.Hom.Iterate

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→* M to Monoid.End M and from f^[n] to f^n just to apply a simple lemma.

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

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

Tags #

homomorphism, iterate

source
ink
theorem hom_coe_pow {M : Type u_2} {F : Type u_1} [inst : 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])⇑(f ^ n) = (⇑f^[n])⇑f^[n]).

source
ink
@[simp]
theorem AddMonoidHom.iterate_map_zero {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ) :
(↑f^[n]) 0 = 0
source
ink
@[simp]
theorem MonoidHom.iterate_map_one {M : Type u_1} [inst : MulOneClass M] (f : M →* M) (n : ℕ) :
(↑f^[n]) 1 = 1
source
ink
@[simp]
theorem AddMonoidHom.iterate_map_add {M : Type u_1} [inst : AddZeroClass M] (f : M →+ M) (n : ℕ) (x : M) (y : M) :
(↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
source
ink
@[simp]
theorem MonoidHom.iterate_map_mul {M : Type u_1} [inst : MulOneClass M] (f : M →* M) (n : ℕ) (x : M) (y : M) :
(↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
source
ink
@[simp]
theorem AddMonoidHom.iterate_map_neg {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x : G) :
(↑f^[n]) (-x) = -(↑f^[n]) x
source
ink
@[simp]
theorem MonoidHom.iterate_map_inv {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (x : G) :
(↑f^[n]) x⁻¹ = ((↑f^[n]) x)⁻¹
source
ink
@[simp]
theorem AddMonoidHom.iterate_map_sub {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (x : G) (y : G) :
(↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
source
ink
@[simp]
theorem MonoidHom.iterate_map_div {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (x : G) (y : G) :
(↑f^[n]) (x / y) = (↑f^[n]) x / (↑f^[n]) y
source
ink
theorem MonoidHom.iterate_map_pow {M : Type u_1} [inst : Monoid M] (f : M →* M) (n : ℕ) (a : M) (m : ℕ) :
(↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
source
ink
theorem MonoidHom.iterate_map_zpow {G : Type u_1} [inst : Group G] (f : G →* G) (n : ℕ) (a : G) (m : ℤ) :
(↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
source
ink
theorem MonoidHom.coe_pow {M : Type u_1} [inst : CommMonoid M] (f : Monoid.End M) (n : ℕ) :
↑(f ^ n) = ↑f^[n]
source
ink
theorem Monoid.End.coe_pow {M : Type u_1} [inst : Monoid M] (f : Monoid.End M) (n : ℕ) :
↑(f ^ n) = ↑f^[n]
source
ink
theorem AddMonoidHom.iterate_map_smul {M : Type u_1} [inst : AddMonoid M] (f : M →+ M) (n : ℕ) (m : ℕ) (x : M) :
(↑f^[n]) (m • x) = m • (↑f^[n]) x
source
ink
theorem AddMonoidHom.iterate_map_nsmul {M : Type u_1} [inst : AddMonoid M] (f : M →+ M) (n : ℕ) (m : ℕ) (a : M) :
(↑f^[n]) (m • a) = m • (↑f^[n]) a
source
ink
theorem AddMonoidHom.iterate_map_zsmul {G : Type u_1} [inst : AddGroup G] (f : G →+ G) (n : ℕ) (m : ℤ) (x : G) :
(↑f^[n]) (m • x) = m • (↑f^[n]) x
source
ink
theorem AddMonoid.End.coe_pow {A : Type u_1} [inst : AddMonoid A] (f : AddMonoid.End A) (n : ℕ) :
↑(f ^ n) = ↑f^[n]
source
ink
theorem RingHom.coe_pow {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) :
↑(f ^ n) = ↑f^[n]
source
ink
theorem RingHom.iterate_map_one {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) :
(↑f^[n]) 1 = 1
source
ink
theorem RingHom.iterate_map_zero {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) :
(↑f^[n]) 0 = 0
source
ink
theorem RingHom.iterate_map_add {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) (x : R) (y : R) :
(↑f^[n]) (x + y) = (↑f^[n]) x + (↑f^[n]) y
source
ink
theorem RingHom.iterate_map_mul {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) (x : R) (y : R) :
(↑f^[n]) (x * y) = (↑f^[n]) x * (↑f^[n]) y
source
ink
theorem RingHom.iterate_map_pow {R : Type u_1} [inst : Semiring R] (f : R →+* R) (a : R) (n : ℕ) (m : ℕ) :
(↑f^[n]) (a ^ m) = (↑f^[n]) a ^ m
source
ink
theorem RingHom.iterate_map_smul {R : Type u_1} [inst : Semiring R] (f : R →+* R) (n : ℕ) (m : ℕ) (x : R) :
(↑f^[n]) (m • x) = m • (↑f^[n]) x
source
ink
theorem RingHom.iterate_map_sub {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (x : R) (y : R) :
(↑f^[n]) (x - y) = (↑f^[n]) x - (↑f^[n]) y
source
ink
theorem RingHom.iterate_map_neg {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (x : R) :
(↑f^[n]) (-x) = -(↑f^[n]) x
source
ink
theorem RingHom.iterate_map_zsmul {R : Type u_1} [inst : Ring R] (f : R →+* R) (n : ℕ) (m : ℤ) (x : R) :
(↑f^[n]) (m • x) = m • (↑f^[n]) x
source
ink
@[simp]
theorem vadd_iterate {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] (a : G) (n : ℕ) [inst : AddAction G H] :
(fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
source
ink
@[simp]
theorem smul_iterate {G : Type u_1} {H : Type u_2} [inst : Monoid G] (a : G) (n : ℕ) [inst : MulAction G H] :
(fun x => a • x)^[n] = fun x => a ^ n • x
source
ink
@[simp]
theorem add_left_iterate {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ) :
(fun x => a + x)^[n] = fun x => n • a + x
source
ink
@[simp]
theorem mul_left_iterate {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ) :
(fun x => a * x)^[n] = fun x => a ^ n * x
source
ink
@[simp]
theorem add_right_iterate {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ) :
(fun x => x + a)^[n] = fun x => x + n • a
source
ink
@[simp]
theorem mul_right_iterate {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ) :
(fun x => x * a)^[n] = fun x => x * a ^ n
source
ink
theorem add_right_iterate_apply_zero {G : Type u_1} [inst : AddMonoid G] (a : G) (n : ℕ) :
((fun x => x + a)^[n]) 0 = n • a
source
ink
theorem mul_right_iterate_apply_one {G : Type u_1} [inst : Monoid G] (a : G) (n : ℕ) :
((fun x => x * a)^[n]) 1 = a ^ n
source
ink
@[simp]
theorem nsmul_iterate {G : Type u_1} [inst : AddMonoid G] (n : ℕ) (j : ℕ) :
(fun x => n • x)^[j] = fun x => n ^ j • x
source
ink
@[simp]
theorem pow_iterate {G : Type u_1} [inst : Monoid G] (n : ℕ) (j : ℕ) :
(fun x => x ^ n)^[j] = fun x => x ^ n ^ j
source
ink
@[simp]
theorem zsmul_iterate {G : Type u_1} [inst : AddGroup G] (n : ℤ) (j : ℕ) :
(fun x => n • x)^[j] = fun x => n ^ j • x
source
ink
@[simp]
theorem zpow_iterate {G : Type u_1} [inst : Group G] (n : ℤ) (j : ℕ) :
(fun x => x ^ n)^[j] = fun x => x ^ n ^ j
source
ink
theorem AddSemiconjBy.function_semiconj_add_left {G : Type u_1} [inst : AddSemigroup G] {a : G} {b : G} {c : G} (h : AddSemiconjBy a b c) :
Function.Semiconj (fun x => a + x) (fun x => b + x) fun x => c + x
source
ink
theorem SemiconjBy.function_semiconj_mul_left {G : Type u_1} [inst : Semigroup G] {a : G} {b : G} {c : G} (h : SemiconjBy a b c) :
Function.Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
source
ink
theorem AddCommute.function_commute_add_left {G : Type u_1} [inst : AddSemigroup G] {a : G} {b : G} (h : AddCommute a b) :
Function.Commute (fun x => a + x) fun x => b + x
source
ink
theorem Commute.function_commute_mul_left {G : Type u_1} [inst : Semigroup G] {a : G} {b : G} (h : Commute a b) :
Function.Commute (fun x => a * x) fun x => b * x
source
ink
theorem AddSemiconjBy.function_semiconj_add_right_swap {G : Type u_1} [inst : AddSemigroup G] {a : G} {b : G} {c : G} (h : AddSemiconjBy a b c) :
Function.Semiconj (fun x => x + a) (fun x => x + c) fun x => x + b
source
ink
theorem SemiconjBy.function_semiconj_mul_right_swap {G : Type u_1} [inst : Semigroup G] {a : G} {b : G} {c : G} (h : SemiconjBy a b c) :
Function.Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
source
ink
theorem AddCommute.function_commute_add_right {G : Type u_1} [inst : AddSemigroup G] {a : G} {b : G} (h : AddCommute a b) :
Function.Commute (fun x => x + a) fun x => x + b
source
ink
theorem Commute.function_commute_mul_right {G : Type u_1} [inst : Semigroup G] {a : G} {b : G} (h : Commute a b) :
Function.Commute (fun x => x * a) fun x => x * b