English
For a commutative ring A and ideals I, J, the sub-dp-ideal relation J ⊓ I is equivalent to the statement that for all n, a, b ∈ I with a − b ∈ J, one has hI.dpow n a − hI.dpow n b ∈ J.
Русский
Пусть A — коммутативное кольцо, I, J — идеалы. Тогда J ⊓ I является sub-dp-идеалом I эквивалентно тому, что для всех n, a, b ∈ I с a−b ∈ J выполняется hI.dpow n a − hI.dpow n b ∈ J.
LaTeX
$$IsSubDPIdeal hI (J ⊓ I) iff ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a − b ∈ J → hI.dpow n a − hI.dpow n b ∈ J$$
Lean4
/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if the divided powers have
some compatibility mod `J`. (The necessity was proved as a sanity check.) -/
theorem isSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} :
IsSubDPIdeal hI (J ⊓ I) ↔
∀ {n : ℕ} {a b : A} (_ : a ∈ I) (_ : b ∈ I) (_ : a - b ∈ J), hI.dpow n a - hI.dpow n b ∈ J :=
by
refine ⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩
· have hab' : a - b ∈ I := I.sub_mem ha hb
rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_add_one, sum_insert notMem_range_self, tsub_self,
hI.dpow_zero hab', mul_one, add_sub_cancel_left]
exact
J.sum_mem
(fun i hi ↦
SemilatticeInf.inf_le_left J I
((J ⊓ I).smul_mem _ (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))
· refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
exact hIJ ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)
