Lean4
/-- The ideal of `A` in which the two divided power structures `hI` and `hI'` coincide. -/
-- TODO : prove that this is the largest ideal which is a sub-dp-ideal in both `hI` and `hI'`.
def dpEqualizer : Ideal A where
carrier := {a ∈ I | ∀ n : ℕ, hI.dpow n a = hI'.dpow n a}
add_mem' {a b} ha
hb := by
apply And.intro (I.add_mem ha.1 hb.1) (fun n ↦ ?_)
rw [hI.dpow_add ha.1 hb.1, hI'.dpow_add ha.1 hb.1]
exact Finset.sum_congr rfl (fun k _ ↦ by rw [ha.2, hb.2])
zero_mem' := by
apply And.intro I.zero_mem (fun n ↦ ?_)
by_cases hn : n = 0
· rw [hn, hI.dpow_zero (zero_mem I), hI'.dpow_zero (zero_mem I)]
· rw [hI.dpow_eval_zero hn, hI'.dpow_eval_zero hn]
smul_mem' a x
hx := by
rw [Algebra.id.smul_eq_mul]
exact ⟨I.mul_mem_left a hx.1, (fun n ↦ by rw [hI.dpow_mul hx.1, hI'.dpow_mul hx.1, hx.2])⟩
