feat(RingTheory): adds a few IsLocalHom instances to AlgHom

[BryceT233]

This PR adds a few IsLocalHom instances to AlgHom .

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 4ec5d95aa6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AlgHom.isLocalHom_comp
+ isLocalHom_algHomId

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[BryceT233]

As I may not need these results for my current formalization work, I am marking this PR as a draft for the time being. Thanks!

Update: It turns out I do need the IsLocalHom instances on AlgHom to cleanly state my current formalization. I've removed the ResidueField.map part to keep the PR focused and marked it as ready for review.

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[j-loreaux]

Can you say why you want these to be instances? I know there are reasons for RingHoms, but I'm not sure about AlgHoms. Also, note that we generally write instance foo ... instead of @[instance] theorem foo ....

[BryceT233]

Thanks for the advice! I am trying to design the category of local algebras with a fixed residue field, which will eventually lead to the base category used in deformation theory (see https://stacks.math.columbia.edu/tag/06GC for the definition of a base category). It is still a work-in-progress, but you can view a one-file version of it here: https://github.com/BryceT233/deformation_theory_basics

Since the morphisms in this category are local AlgHoms, I thought it would be better to have IsLocalHom instances directly for AlgHom. I could try to work around this by coercing the AlgHoms to RingHoms, but I'm worried that might not lead to the ideal shape for the definition.

About the style issue, I think I was just copying the existing style from RingHom part of the code above in the same file, usually I used instance too :)

[BryceT233]

I've realized I can use an equivalent definition for local homomorphisms that avoids the need for an IsLocalHom instance. Therefore, I'll go ahead and close this PR