isDPMorphism_def — Mathlib

English

A ring homomorphism f is a DividedPowers morphism between hI and hJ if its induced ideal map lands in J and it commutes with all divided powers on elements of I.

Русский

Кольцевое гомоморфизм f является морфизмом делённых степеней между hI и hJ, если отображение идеалов принадлежит J и он сохраняет делённые степени на элементах I.

LaTeX

$$$IsDPMorphism\\, hI\\, hJ\\, f \\;\\iff\\; I.map\\ f \\le J \\wedge \\forall\\ n, \\forall a \\in I, hJ.dpow n (f a) = f (hI.dpow n a)$$$

Lean4

theorem isDPMorphism_def (f : A →+* B) :
    IsDPMorphism hI hJ f ↔ I.map f ≤ J ∧ ∀ {n}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a) :=
  ⟨fun h ↦ ⟨h.ideal_comp, h.dpow_comp⟩, fun ⟨h1, h2⟩ ↦ IsDPMorphism.mk h1 h2⟩

Похожие утверждения