Commit 2025-03-13 14:38 ed250483

View on Github →

feat(RingTheory/DividedPowers/DPMorphism): add divided power morphisms (#22318) 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.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DividedPowers/DPMorphism.lean

added theorem DividedPowers.DPMorphism.coe_toRingHom

added theorem DividedPowers.DPMorphism.comp_toRingHom

added def DividedPowers.DPMorphism.fromGens

added theorem DividedPowers.DPMorphism.fromGens_coe

added def DividedPowers.DPMorphism.id

added theorem DividedPowers.DPMorphism.isDPMorphism

added def DividedPowers.DPMorphism.mk'

added theorem DividedPowers.DPMorphism.toRingHom_apply

added structure DividedPowers.DPMorphism

added theorem DividedPowers.IsDPMorphism.comp

added theorem DividedPowers.IsDPMorphism.map_dpow

added theorem DividedPowers.IsDPMorphism.of_comp

added theorem DividedPowers.IsDPMorphism.on_span

added structure DividedPowers.IsDPMorphism

added theorem DividedPowers.dpow_comp_from_gens

added theorem DividedPowers.dpow_eq_from_gens

added def DividedPowers.ideal_from_ringHom

added theorem DividedPowers.isDPMorphism_def

added theorem DividedPowers.isDPMorphism_iff