English
If a ring homomorphism f maps I into K and hI along with hK,hK' define divided-power structures with isomorphisms (IsDPMorphism) from hI to hK and hK', then the image f(I) lies inside the equalizer of hK and hK'.
Русский
Пусть колебательный гомоморфизм f отображает I в K и существуют структуры разделённых степеней hI, hK, hK' с отображениями IsDPMorphism; тогда образ f(I) лежит внутри равновесия dpEqualizer(hK,hK').
LaTeX
$$$Ideal.map f I \\le dpEqualizer(hK,hK')$$$
Lean4
theorem le_equalizer_of_isDPMorphism {B : Type*} [CommSemiring B] (f : A →+* B) {K : Ideal B}
(hI_le_K : Ideal.map f I ≤ K) (hK hK' : DividedPowers K) (hIK : IsDPMorphism hI hK f)
(hIK' : IsDPMorphism hI hK' f) : Ideal.map f I ≤ dpEqualizer hK hK' :=
by
rw [Ideal.map, span_le]
rintro b ⟨a, ha, rfl⟩
exact ⟨hI_le_K (mem_map_of_mem f ha), fun n ↦ by rw [hIK.2 a ha, hIK'.2 a ha]⟩
