English
Let A and B be commutative semirings with ideals I ⊆ A and J ⊆ B, and e: A ≃+* B be a ring isomorphism such that I maps to J. Then there is a transferred divided-powers structure on J defined by transporting that on I along e: for every n, b ∈ B, the n-th divided power on b is defined as e(h_I.dpow n (e⁻¹(b))).
Русский
Пусть A и B — коммутативные полупрямые колца, I ⊆ A и J ⊆ B — Ideals, и e: A ≃+* B — кольцевой эквивалент. Пусть отображение маппирования идеала I в J. Тогда существует перенесённая структура делённых степеней на J, полученная переносом с I по e: для каждого n и b ∈ B, dpow_J(n)(b) = e(dpow_I(n)(e⁻¹(b))).
LaTeX
$$$(\\text{ofRingEquiv } h\\ h_I).dpow\\,n\\,b = e\\left(h_I.dpow\\,n\\left(e^{-1}\\,b\\right)\\right)$$$
Lean4
/-- Transfer divided powers under an equivalence -/
def ofRingEquiv (hI : DividedPowers I) : DividedPowers J
where
dpow n b := e (hI.dpow n (e.symm b))
dpow_null
hx := by
rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]
rwa [symm_apply_mem_of_equiv_iff, h]
dpow_zero
hx := by
rw [EmbeddingLike.map_eq_one_iff, hI.dpow_zero]
rwa [symm_apply_mem_of_equiv_iff, h]
dpow_one
hx := by
rw [dpow_one, RingEquiv.apply_symm_apply]
rwa [I.symm_apply_mem_of_equiv_iff, h]
dpow_mem hn
hx := by
rw [← h, I.apply_mem_of_equiv_iff]
apply hI.dpow_mem hn
rwa [I.symm_apply_mem_of_equiv_iff, h]
dpow_add hx
hy := by
simp only [map_add]
rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx)) (symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]
simp only [map_sum, map_mul]
dpow_mul
hx := by
simp only [map_mul]
rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
rw [map_mul, map_pow]
simp only [RingEquiv.apply_symm_apply]
mul_dpow
hx := by
rw [← map_mul, hI.mul_dpow, map_mul]
· simp only [map_natCast]
· rwa [symm_apply_mem_of_equiv_iff, h]
dpow_comp hn
hx := by
simp only [RingEquiv.symm_apply_apply]
rw [hI.dpow_comp hn]
· simp only [map_mul, map_natCast]
· rwa [symm_apply_mem_of_equiv_iff, h]
