English
If generated by S and if f maps S into J and respects dpow on S, then f is a DividedPowers morphism on the whole I generated by S.
Русский
Если I = span S и f отправляет S в J и сохраняет dpow на элементы S, то f является морфизмом делённых степеней на весь I.
LaTeX
$$theorem on_span {f : A →+* B} {S : Set A} (hS : I = span S) (hS' : ∀ s ∈ S, f s ∈ J)\n (hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) : IsDPMorphism hI hJ f$$
Lean4
/-- Given a ring homomorphism `A → B` and ideals `I ⊆ A` and `J ⊆ B` such that `I.map f ≤ J`,
this is the `A`-ideal on which `f (hI.dpow n x) = hJ.dpow n (f x)`.
See [N. Roby, *Les algèbres à puissances dividées* (Proposition 2)][Roby-1965]. -/
def _root_.DividedPowers.ideal_from_ringHom {f : A →+* B} (hf : I.map f ≤ J) : Ideal A
where
carrier := {x ∈ I | ∀ n : ℕ, f (hI.dpow n (x : A)) = hJ.dpow n (f (x : A))}
add_mem' := fun hx hy ↦ by
simp only [mem_setOf_eq, map_add] at hx hy ⊢
refine ⟨I.add_mem hx.1 hy.1, fun n ↦ ?_⟩
rw [hI.dpow_add hx.1 hy.1, map_sum, hJ.dpow_add (hf (mem_map_of_mem f hx.1)) (hf (mem_map_of_mem f hy.1))]
apply congr_arg
ext k
rw [map_mul, hx.2, hy.2]
zero_mem' := by
simp only [mem_setOf_eq, Submodule.zero_mem, map_zero, true_and]
intro n
induction n with
| zero => rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]
| succ n => rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
smul_mem' := fun r x hx ↦ by
refine ⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩
rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow, hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
