English
If two DividedPowers structures on I agree on a generating set S, then the two structures are equal.
Русский
Если две структуры делённых степеней на I совпадают на порождающем наборе S, то эти структуры равны.
LaTeX
$$theorem dpow_eq_from_gens {S : Set A} (hS : I = span S) (hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a) : hI' = hI$$
Lean4
/-- If two divided power structures on the ideal `I` agree on a generating set, then they are
equal.
See [N. Roby, *Les algèbres à puissances dividées* (Corollary to Proposition 3)][Roby-1965]. -/
theorem dpow_eq_from_gens {S : Set A} (hS : I = span S) (hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a) :
hI' = hI := by
ext n a
by_cases ha : a ∈ I
· refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha
· intro s hs
simp only [RingHom.id_apply, hS]
exact subset_span hs
· intro m b hb
simpa only [RingHom.id_apply] using (hdp b hb)
· rw [hI.dpow_null ha, hI'.dpow_null ha]
