English
There is an equivalence between DividedPowers structures on I and J when I maps to J by a RingEquiv; the equivalence is given by ofRingEquiv and its inverse, forming an isomorphism of the divided powers data.
Русский
Существует эквивалентность структур делённых степеней на I и J при соответствии I → J через RingEquiv; эквивалентность задаётся через ofRingEquiv и его обратное отображение.
LaTeX
$$$\\text{Equiv} : \\mathrm{DividedPowers}(I) \\simeq \\mathrm{DividedPowers}(J)$$$
Lean4
theorem isDPMorphism_iff (f : A →+* B) :
IsDPMorphism hI hJ f ↔ I.map f ≤ J ∧ ∀ n ≠ 0, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a) :=
by
rw [isDPMorphism_def, and_congr_right_iff]
refine fun hIJ ↦ ⟨fun H n _ ↦ H, fun H n ↦ ?_⟩
by_cases hn : n = 0
· intro _ ha
rw [hn, hI.dpow_zero ha, hJ.dpow_zero (hIJ (mem_map_of_mem f ha)), map_one]
· exact H n hn
