Iterates of monoid homomorphisms #
Iterate of a monoid homomorphism is a monoid 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
SemiconjBy.function_semiconj_mul_left
{G : Type u_2}
[Semigroup G]
{a b 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
AddSemiconjBy.function_semiconj_add_left
{G : Type u_2}
[AddSemigroup G]
{a b 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
Commute.function_commute_mul_left
{G : Type u_2}
[Semigroup G]
{a b : G}
(h : Commute a b)
:
Function.Commute (fun (x : G) => a * x) fun (x : G) => b * x
theorem
AddCommute.function_commute_add_left
{G : Type u_2}
[AddSemigroup G]
{a b : G}
(h : AddCommute a b)
:
Function.Commute (fun (x : G) => a + x) fun (x : G) => b + x
theorem
SemiconjBy.function_semiconj_mul_right_swap
{G : Type u_2}
[Semigroup G]
{a b 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
AddSemiconjBy.function_semiconj_add_right_swap
{G : Type u_2}
[AddSemigroup G]
{a b 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
Commute.function_commute_mul_right
{G : Type u_2}
[Semigroup G]
{a b : G}
(h : Commute a b)
:
Function.Commute (fun (x : G) => x * a) fun (x : G) => x * b
theorem
AddCommute.function_commute_add_right
{G : Type u_2}
[AddSemigroup G]
{a b : G}
(h : AddCommute a b)
:
Function.Commute (fun (x : G) => x + a) fun (x : G) => x + b