[Merged by Bors] - feat(algebra/module/linear_map): Add linear_map.iterate

[Ruben-VandeVelde]

Co-authored-by: Alex J. Best alex.j.best@gmail.com

---

Extracted from #1822.

[eric-wieser]

How reasonable is it to define this as (\lam g, g.comp f)^[n]?

[Ruben-VandeVelde]

I pushed what I think you meant; I don't feel strongly either way.

[eric-wieser]

Sorry for being unclear, I meant

def iterate (n : ℕ) (f : M →ₗ[R] M) : M →ₗ[R] M :=
(λ g, linear_map.comp g f)^[n] linear_map.id

or perhaps

def iterate (n : ℕ) (f : M →ₗ[R] M) : M →ₗ[R] M :=
f.comp^[n] linear_map.id

[eric-wieser]

But your new version has the nice benefit of making iterate_to_fun a rfl lemma

[Ruben-VandeVelde]

Oh, I see. I have no preference

[eric-wieser]

Suggested change

	@[simp] lemma iterate_to_fun : ∀ n, (iterate f n).to_fun = nat.iterate f.to_fun n
	@[simp] lemma iterate_to_fun : ∀ n, iterate f n = (⇑f)^[n]

[Ruben-VandeVelde]

This seems to have needed more changes; reverted until I can look more closely.

[semorrison]

For comparison, this is what I had written in a branch:

namespace linear_map

universes u v

def iterate {R : Type u} [semiring R]
   {M : Type v} [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) : ℕ → (M →ₗ[R] M)
| 0 := linear_map.id
| (n+1) := (iterate n).comp f

@[simp] lemma iterate_apply {R : Type u} [semiring R]
   {M : Type v} [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) (n : ℕ) (m : M) :
  f.iterate n m = ((f : M → M)^[n] m) :=
begin
  induction n with n ih generalizing m,
  { refl, },
  { apply ih, },
end

instance {R : Type u} [semiring R] {M : Type v} [add_comm_monoid M] [semimodule R M] :
  has_pow (M →ₗ[R] M) ℕ :=
{ pow := λ f n, f.iterate n, }

@[simp] lemma pow_apply {R : Type u} [semiring R]
   {M : Type v} [add_comm_monoid M] [semimodule R M] (f : M →ₗ[R] M) (n : ℕ) (m : M) :
  (f^n) m = ((f : M → M)^[n] m) :=
iterate_apply f n m

end linear_map

[semorrison]

I've realised that we already have a instance : monoid (M →ₗ[R] M) in src/linear_algebra/basic.lean.

Perhaps we don't actually need this PR?

iterate_surj and friends are worth saving, however.

[semorrison]

I changed some names: lemmas that conclude injective should actually have _injective in the name.

[semorrison]

bors merge

[eric-wieser]

bors r-, there's a line length issue

[bors]

Canceled.

[bors]

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests