mathlib documentation

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 monoid_hom.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 *_hom.map_* lemmas under names *_hom.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_2} [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 monoid_hom.iterate_map_one {M : Type u_1} [mul_one_class M] (f : M →* M) (n : ) :
f^[n] 1 = 1
@[simp]
theorem add_monoid_hom.iterate_map_zero {M : Type u_1} [add_zero_class M] (f : M →+ M) (n : ) :
f^[n] 0 = 0
@[simp]
theorem add_monoid_hom.iterate_map_add {M : Type u_1} [add_zero_class M] (f : M →+ M) (n : ) (x y : M) :
f^[n] (x + y) = f^[n] x + f^[n] y
@[simp]
theorem monoid_hom.iterate_map_mul {M : Type u_1} [mul_one_class M] (f : M →* M) (n : ) (x y : M) :
f^[n] (x * y) = f^[n] x * f^[n] y
@[simp]
theorem add_monoid_hom.iterate_map_neg {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (x : G) :
f^[n] (-x) = -f^[n] x
@[simp]
theorem monoid_hom.iterate_map_inv {G : Type u_3} [group G] (f : G →* G) (n : ) (x : G) :
@[simp]
theorem add_monoid_hom.iterate_map_sub {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (x y : G) :
f^[n] (x - y) = f^[n] x - f^[n] y
@[simp]
theorem monoid_hom.iterate_map_div {G : Type u_3} [group G] (f : G →* G) (n : ) (x y : G) :
f^[n] (x / y) = f^[n] x / f^[n] y
theorem monoid_hom.iterate_map_pow {M : Type u_1} [monoid M] (f : M →* M) (n : ) (a : M) (m : ) :
f^[n] (a ^ m) = f^[n] a ^ m
theorem monoid_hom.iterate_map_zpow {G : Type u_3} [group G] (f : G →* G) (n : ) (a : G) (m : ) :
f^[n] (a ^ m) = f^[n] a ^ m
theorem monoid_hom.coe_pow {M : Type u_1} [comm_monoid M] (f : monoid.End M) (n : ) :
(f ^ n) = (f^[n])
theorem monoid.End.coe_pow {M : Type u_1} [monoid M] (f : monoid.End M) (n : ) :
(f ^ n) = (f^[n])
theorem add_monoid_hom.iterate_map_smul {M : Type u_1} [add_monoid M] (f : M →+ M) (n m : ) (x : M) :
f^[n] (m x) = m f^[n] x
theorem add_monoid_hom.iterate_map_nsmul {M : Type u_1} [add_monoid M] (f : M →+ M) (n : ) (a : M) (m : ) :
f^[n] (m a) = m f^[n] a
theorem add_monoid_hom.iterate_map_zsmul {G : Type u_3} [add_group G] (f : G →+ G) (n : ) (m : ) (x : G) :
f^[n] (m x) = m f^[n] x
theorem add_monoid.End.coe_pow {A : Type u_1} [add_monoid A] (f : add_monoid.End A) (n : ) :
(f ^ n) = (f^[n])
theorem ring_hom.coe_pow {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
(f ^ n) = (f^[n])
theorem ring_hom.iterate_map_one {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
f^[n] 1 = 1
theorem ring_hom.iterate_map_zero {R : Type u_5} [semiring R] (f : R →+* R) (n : ) :
f^[n] 0 = 0
theorem ring_hom.iterate_map_add {R : Type u_5} [semiring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x + y) = f^[n] x + f^[n] y
theorem ring_hom.iterate_map_mul {R : Type u_5} [semiring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x * y) = f^[n] x * f^[n] y
theorem ring_hom.iterate_map_pow {R : Type u_5} [semiring R] (f : R →+* R) (a : R) (n m : ) :
f^[n] (a ^ m) = f^[n] a ^ m
theorem ring_hom.iterate_map_smul {R : Type u_5} [semiring R] (f : R →+* R) (n m : ) (x : R) :
f^[n] (m x) = m f^[n] x
theorem ring_hom.iterate_map_sub {R : Type u_5} [ring R] (f : R →+* R) (n : ) (x y : R) :
f^[n] (x - y) = f^[n] x - f^[n] y
theorem ring_hom.iterate_map_neg {R : Type u_5} [ring R] (f : R →+* R) (n : ) (x : R) :
f^[n] (-x) = -f^[n] x
theorem ring_hom.iterate_map_zsmul {R : Type u_5} [ring R] (f : R →+* R) (n : ) (m : ) (x : R) :
f^[n] (m x) = m f^[n] x
theorem equiv.perm.coe_pow {α : Type u_1} (f : equiv.perm α) (n : ) :
(f ^ n) = (f^[n])
@[simp]
theorem smul_iterate {G : Type u_3} {H : Type u_4} [monoid G] (a : G) (n : ) [mul_action G H] :
@[simp]
theorem vadd_iterate {G : Type u_3} {H : Type u_4} [add_monoid G] (a : G) (n : ) [add_action G H] :
@[simp]
theorem mul_left_iterate {G : Type u_3} [monoid G] (a : G) (n : ) :
@[simp]
theorem add_left_iterate {G : Type u_3} [add_monoid G] (a : G) (n : ) :
@[simp]
theorem mul_right_iterate {G : Type u_3} [monoid G] (a : G) (n : ) :
(λ (_x : G), _x * a)^[n] = λ (_x : G), _x * a ^ n
@[simp]
theorem add_right_iterate {G : Type u_3} [add_monoid G] (a : G) (n : ) :
(λ (_x : G), _x + a)^[n] = λ (_x : G), _x + n a
theorem mul_right_iterate_apply_one {G : Type u_3} [monoid G] (a : G) (n : ) :
(λ (_x : G), _x * a)^[n] 1 = a ^ n
theorem add_right_iterate_apply_zero {G : Type u_3} [add_monoid G] (a : G) (n : ) :
(λ (_x : G), _x + a)^[n] 0 = n a
theorem commute.function_commute_mul_left {G : Type u_3} [semigroup G] {a b : G} (h : commute a b) :
theorem add_semiconj_by.function_semiconj_add_right_swap {G : Type u_3} [add_semigroup G] {a b c : G} (h : add_semiconj_by a b c) :
function.semiconj (λ (_x : G), _x + a) (λ (_x : G), _x + c) (λ (_x : G), _x + b)
theorem semiconj_by.function_semiconj_mul_right_swap {G : Type u_3} [semigroup G] {a b c : G} (h : semiconj_by a b c) :
function.semiconj (λ (_x : G), _x * a) (λ (_x : G), _x * c) (λ (_x : G), _x * b)
theorem add_commute.function_commute_add_right {G : Type u_3} [add_semigroup G] {a b : G} (h : add_commute a b) :
function.commute (λ (_x : G), _x + a) (λ (_x : G), _x + b)
theorem commute.function_commute_mul_right {G : Type u_3} [semigroup G] {a b : G} (h : commute a b) :
function.commute (λ (_x : G), _x * a) (λ (_x : G), _x * b)