[Merged by Bors] - refactor: Redefine pow in terms of iterate

[YaelDillies]

In the Monoid instances for Function.End α, Equiv.Perm α, Monoid.End α, AddMonoid.End α, α →+* α, replace the default npowRec by a custom one in terms of Nat.iterate. Write the expected coercion lemmas.

As a consequence, I can delete the recently introduced file Algebra.Ring.Hom.IterateHom.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.231388.20Redefine.20pow.20in.20terms.20of.20iterate

---

Rehash of leanprover-community/mathlib3#18077

[kim-em]

@YaelDillies, the original mathlib3 PR is marked as too-late, now. I'm removing forward-port-placeholder and mathlib3-pair. Could you prepare it for review directly to mathlib4, or close?

[kim-em]

Sorry, actually as this PR is empty I'll just close. Just open a new PR if you'd like to bring the material across.

[urkud]

Let me repeat my concern from Lean3 PR:

Note that if we go forward with this refactor, the monoid structure on CategoryTheory.End (GroupCat.of G) will be no longer defeq to Monoid.End.monoid. I don't know whether we ever rely on this defeq.

[YaelDillies]

I don't understand how that's not fixable. Surely it's just a matter of tweaking the pow defeq in Monoid (CategoryTheory.End (GroupCat.of G))?

[urkud]

Monoid (CategoryTheory.End _) is defined uniformly for all categories, you can't fix pow for one category. If you want to be able to do that, then you need to include this data in the definition of Category.

[YaelDillies]

Yeah okay. I must say I don't think it's defeq's job to translate category-theoretic constructs to their group-theoretic equivalents.

The fact that we can do it in simple cases doesn't mean it extends indefinitely and indeed I would rather have a to_additive-like tactic to perform the translation rather than relying on cosmic alignment of definitions.

Right now, this translation sounds like a pretty niche use case anyway?

[urkud]

The issue is not about translation. The issue is that we'll have 2 defeq types (X --> X for some categories) with propeq but not defeq instances about them.

[YaelDillies]

Well they're only defeq because one is a too-transparent type synonym of the other, right? Using that would be defeq abuse.

[urkud]

Could you please open a Zulip discussion? I don't want to merge this PR myself, but if another maintainer rules my objection as invalid/irrelevant, then I won't insist.

[jcommelin]

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.231388.20Redefine.20pow.20in.20terms.20of.20iterate

[jcommelin]

Thanks 🎉

bors merge

[kbuzzard]

Note that the Zulip discussion is not publicly viewable

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style