feat(RingTheory/DividedPowers/DPMorphism): add divided power morphisms

[mariainesdff]

Let A and B be commutative (semi)rings, let I be an ideal of A and let J be an ideal of
B. Given divided power structures on I and J, a ring morphism A →+* B is a divided
power morphism if it is compatible with these divided power structures.

Co-authored-by: AntoineChambert-Loir [email protected]

---

[github-actions]

PR summary c9edd9284e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.DividedPowers.DPMorphism (new file)	1116

---

Declarations diff

+ DPMorphism
+ IsDPMorphism
+ _root_.DividedPowers.ideal_from_ringHom
+ coe_ringHom
+ coe_toRingHom
+ comp_toRingHom
+ dpow_comp_from_gens
+ dpow_eq_from_gens
+ fromGens
+ fromGens_coe
+ id
+ instFunLike
+ instance : Inhabited (DPMorphism hI hI) := ⟨DPMorphism.id hI⟩
+ isDPMorphism
+ isDPMorphism_def
+ isDPMorphism_iff
+ map_dpow
+ mk'
+ of_comp
+ on_span
+ toRingHom_apply
++ comp

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[riccardobrasca]

Can you explain how one is supposed to introduce a divided power morphism? Using IsDPMorphism or the bundled version?

Thanks!

bors d+

[riccardobrasca]

What about making this into a structure with two fields? It seems more natural (and mathematically it is exactly the same).

[mathlib-bors]

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