English
The dpow on the codomain B of a surjective ring homomorphism is defined by extending the original dpow from A through the quotient map, yielding a noncomputable definition that depends on isSubDPIdeal_aux.
Русский
dpow на кодомодуле B для сюръективного гомоморфизма задаётся через продолжение dpow от A по фактор-маршруту; определение не вычислимо и зависит от isSubDPIdeal_aux.
LaTeX
$$$DividedPowers.Quotient.OfSurjective.dpow$$$
Lean4
/-- When `f.ker ⊓ I` is a sub-dp-ideal of `I`, this is the induced divided power structure on
the ideal `I.map f` of the target. -/
noncomputable def dividedPowers : DividedPowers J
where
dpow := dpow hI f
dpow_null n {x}
hx' := by
classical
rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
rintro ⟨⟨a, ha⟩, rfl⟩
exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
dpow_zero {x}
hx := by
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]
dpow_one {x}
hx := by
obtain ⟨a, ha, hax⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]
dpow_mem {n x} hn
hx := by
rw [hIJ] at hx ⊢
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp hx
rw [dpow_apply' hI hIf ha]
exact mem_map_of_mem _ (hI.dpow_mem hn ha)
dpow_add hx
hy := by
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)
rw [← map_add, dpow_apply' hI hIf (I.add_mem ha hb), hI.dpow_add ha hb, map_sum, Finset.sum_congr rfl]
exact fun k _ ↦ by rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]
dpow_mul {n x y}
hy := by
obtain ⟨a, rfl⟩ := hf x
obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)
rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow, dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb,
_root_.map_mul]
mul_dpow
hx := by
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
simp only [dpow_apply' hI hIf ha]
rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]
dpow_comp hn
hx := by
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
simp only [dpow_apply' hI hIf, ha, hI.dpow_mem hn ha]
rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]
