English
The DPMorphism between divided powers is defined by a ring homomorphism f respecting a generating set S of I, provided f maps I into J and f respects divided powers on S.
Русский
Установление DPMorphism между деленными степенями задаётся кольмовым однородным отображением f, сохраняющим порождённую пару S и отображающим I в J с сохранением делённых степеней на S.
LaTeX
$$def fromGens {f : A →+* B} {S : Set A} (hS : I = span S) (hf : I.map f ≤ J) (h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) : DPMorphism hI hJ$$
Lean4
/-- The `DPMorphism` induced by a ring morphism, given that divided powers are compatible on a
generating set.
See [N. Roby, *Les algèbres à puissances dividées* (Proposition 3)][Roby-1965]. -/
def fromGens {f : A →+* B} {S : Set A} (hS : I = span S) (hf : I.map f ≤ J)
(h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)) : DPMorphism hI hJ
where
toRingHom := f
ideal_comp := hf
dpow_comp {n} x
hx :=
by
have hS' : S ⊆ ideal_from_ringHom hI hJ hf := fun y hy ↦
by
simp only [mem_coe, ideal_from_ringHom, Submodule.mem_mk]
exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩
rw [← span_le, ← hS] at hS'
exact ((hS' hx).2 n).symm
