English
When there is a surjective quotient map f: A → B and a sub-DP-ideal on I whose quotient aligns with J = I.map f, an induced divided-power structure on J exists.
Русский
Пусть есть сюръективная карта факторизации f: A → B и подDP-идеал на I, чьё quotient-образование согласуется с J = I.map f; тогда существует индуцированная структура DP на J.
LaTeX
$$$DividedPowers.J$$$
Lean4
/-- The definition of divided powers on the codomain `B` of a surjective ring homomorphism
from a ring `A` with divided powers `hI`. This definition is tagged as noncomputable
because it makes use of `Function.extend`, but under the hypothesis
`IsSubDPIdeal hI (RingHom.ker f ⊓ I)`, `dividedPowers_unique` proves that no choices are
involved. -/
noncomputable def dpow : ℕ → B → B := fun n ↦ Function.extend (fun a ↦ f a : I → B) (fun a ↦ f (hI.dpow n a) : I → B) 0
