English
If hI is a dp-structure on I and hIf provides the sub-dp-ideal condition inside ker(f) ∩ I, then for any a ∈ I, dpow(hI,f,n)(f(a)) equals f(hI.dpow(n,a)).
Русский
Пусть hI — DP-структура на I, а hIf задаёт условие суб-DP-идеала внутри ker(f) ∩ I; тогда для любого a ∈ I выполняется dpow(hI,f,n)(f(a)) = f(hI.dpow(n,a)).
LaTeX
$$$\\forall a \\in I:\\ dpow(hI,f,n)(f(a)) = f(hI.dpow(n,a))$$$
Lean4
/-- Divided powers on the codomain `B` of a surjective ring homomorphism `f` are compatible
with `f`. -/
theorem dpow_apply' (hIf : IsSubDPIdeal hI (RingHom.ker f ⊓ I)) {n : ℕ} {a : A} (ha : a ∈ I) :
dpow hI f n (f a) = f (hI.dpow n a) := by
classical
simp only [dpow, Function.extend_def]
have h : ∃ (a_1 : I), f ↑a_1 = f a := by use ⟨a, ha⟩
rw [dif_pos h, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
apply (hI.isSubDPIdeal_inf_iff.mp hIf) (Submodule.coe_mem _) ha
rw [RingHom.mem_ker, map_sub, sub_eq_zero, h.choose_spec]
