English
If two DividedPowers structures agree on generators, then they agree on the span closure and the associated map respects dpow on all elements of I.
Русский
Если структуры делённых степеней согласованы на порождающих, то они согласованы на замыке порождений и отображение сохраняет dpow на всех элементах 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
theorem on_span {f : A →+* B} {S : Set A} (hS : I = span S) (hS' : ∀ s ∈ S, f s ∈ J)
(hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) : IsDPMorphism hI hJ f :=
by
suffices h : I.map f ≤ J by
exact ⟨h, fun a ha ↦ by rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]⟩
rw [hS, map_span, span_le]
rintro b ⟨a, has, rfl⟩
exact hS' a has
