mathlib3 documentation

algebra.hom.iterate

Iterates of monoid and ring homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :

⇑f^[n] x⁻¹ = (⇑f^[n] x)⁻¹

@[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

@[simp]

theorem smul_iterate {G : Type u_3} {H : Type u_4} [monoid G] (a : G) (n : ℕ) [mul_action G H] :

has_smul.smul a^[n] = has_smul.smul (a ^ n)

@[simp]

theorem vadd_iterate {G : Type u_3} {H : Type u_4} [add_monoid G] (a : G) (n : ℕ) [add_action G H] :

has_vadd.vadd a^[n] = has_vadd.vadd (n • a)

@[simp]

theorem mul_left_iterate {G : Type u_3} [monoid G] (a : G) (n : ℕ) :

has_mul.mul a^[n] = has_mul.mul (a ^ n)

@[simp]

theorem add_left_iterate {G : Type u_3} [add_monoid G] (a : G) (n : ℕ) :

has_add.add a^[n] = has_add.add (n • a)

@[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

@[simp]

theorem pow_iterate {G : Type u_3} [monoid G] (n j : ℕ) :

(λ (x : G), x ^ n)^[j] = λ (x : G), x ^ n ^ j

@[simp]

theorem nsmul_iterate {G : Type u_3} [add_monoid G] (n j : ℕ) :

(λ (x : G), n • x)^[j] = λ (x : G), n ^ j • x

@[simp]

theorem zpow_iterate {G : Type u_3} [group G] (n : ℤ) (j : ℕ) :

(λ (x : G), x ^ n)^[j] = λ (x : G), x ^ n ^ j

@[simp]

theorem zsmul_iterate {G : Type u_3} [add_group G] (n : ℤ) (j : ℕ) :

(λ (x : G), n • x)^[j] = λ (x : G), n ^ j • x

theorem semiconj_by.function_semiconj_mul_left {G : Type u_3} [semigroup G] {a b c : G} (h : semiconj_by a b c) :

function.semiconj (has_mul.mul a) (has_mul.mul b) (has_mul.mul c)

theorem add_semiconj_by.function_semiconj_add_left {G : Type u_3} [add_semigroup G] {a b c : G} (h : add_semiconj_by a b c) :

function.semiconj (has_add.add a) (has_add.add b) (has_add.add c)

theorem commute.function_commute_mul_left {G : Type u_3} [semigroup G] {a b : G} (h : commute a b) :

function.commute (has_mul.mul a) (has_mul.mul b)

theorem add_commute.function_commute_add_left {G : Type u_3} [add_semigroup G] {a b : G} (h : add_commute a b) :

function.commute (has_add.add a) (has_add.add 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)