English
If there exists a dp-structure on I and one on I.map(f) through a quotient by J, together with a dp-morphism relating them, then J ∩ I forms a sub-DP-ideal of I.
Русский
При наличии dp-структуры на I и dp-структуры на образ I через фактор-морфизм по J с dp-морфизмом между ними, пересечение J ∩ I образует подDP-идеал I.
LaTeX
$$$J \\cap I \\text{ is a subDPIdeal } I$$$
Lean4
/-- If there is a divided power structure on `I⬝(A/J)` such that the quotient map is
a dp-morphism, then `J ⊓ I` is a sub-dp-ideal of `I`. -/
def subDPIdeal_inf_of_quot {A : Type*} [CommRing A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A}
{hJ : DividedPowers (I.map (Ideal.Quotient.mk J))} {φ : DPMorphism hI hJ} (hφ : φ.toRingHom = Ideal.Quotient.mk J) :
SubDPIdeal hI where
carrier := J ⊓ I
isSubideal := by simp only [inf_le_right]
dpow_mem := fun _ hn a ⟨haJ, haI⟩ ↦ by
refine ⟨?_, hI.dpow_mem hn haI⟩
rw [SetLike.mem_coe, ← Quotient.eq_zero_iff_mem, ← hφ, ← φ.dpow_comp a haI]
suffices ha0 : φ.toRingHom a = 0 by rw [ha0, hJ.dpow_eval_zero hn]
rw [hφ, Quotient.eq_zero_iff_mem]
exact haJ
