English
If J = I.map f and f, g are ring homomorphisms with IsDPMorphism properties, then g ∘ f is a DividedPowers morphism from I to K.
Русский
Если J = I.map f и f, g кольцевые гомоморфизмы с соответствующими свойствами, то композиция g∘f сохраняет структуру делённых степеней между I и K.
LaTeX
$$theorem of_comp (f : A →+* B) (g : B →+* C) (heq : J = I.map f) (hf : IsDPMorphism hI hJ f)\n (hh : IsDPMorphism hI hK (g.comp f)) : IsDPMorphism hJ hK g$$
Lean4
theorem of_comp (f : A →+* B) (g : B →+* C) (heq : J = I.map f) (hf : IsDPMorphism hI hJ f)
(hh : IsDPMorphism hI hK (g.comp f)) : IsDPMorphism hJ hK g :=
by
apply on_span _ _ heq
· rintro b ⟨a, ha, rfl⟩
rw [← RingHom.comp_apply]
exact hh.1 (mem_map_of_mem _ ha)
· rintro n b ⟨a, ha, rfl⟩
rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]
