English
If I and J are ideals in A and B connected by a ring equivalence e with I.map e = J, then there is an equivalence between the divided-powers structures on I and J, given by forward and inverse transports along e.
Русский
Если идеалы I и J связаны кольцевым эквивалентом e с I.map e = J, то между структурами делённых степеней на I и на J существует эквивалентность, даваемая прямым и обратным переносами вдоль e.
LaTeX
$$$\\mathrm{DividedPowers}(I) \\cong \\mathrm{DividedPowers}(J)$$$
Lean4
/-- Transfer divided powers under an equivalence (Equiv version) -/
def equiv : DividedPowers I ≃ DividedPowers J
where
toFun := ofRingEquiv h
invFun := ofRingEquiv (show map e.symm J = I by rw [← h]; exact I.map_of_equiv e)
left_inv := fun hI ↦ by ext n a; simp [ofRingEquiv]
right_inv := fun hJ ↦ by ext n b; simp [ofRingEquiv]
