comp — Mathlib

English

If g is a DividedPowers morphism from hJ to hK and f is from hI to hJ, then the composition g ∘ f is a DividedPowers morphism from hI to hK.

Русский

Если g — морфизм делённых степеней от hJ к hK, а f — от hI к hJ, то композиция g ∘ f — морфизм делённых степеней от hI к hK.

LaTeX

$$$IsDPMorphism\\, hI\\, hK\\, (g\\circ f)$$$

Lean4

theorem comp {f : A →+* B} {g : B →+* C} (hg : IsDPMorphism hJ hK g) (hf : IsDPMorphism hI hJ f) :
    IsDPMorphism hI hK (g.comp f) :=
  by
  refine ⟨le_trans (map_map f g ▸ map_mono hf.1) hg.1, fun a ha ↦ ?_⟩
  simp only [RingHom.coe_comp, Function.comp_apply]
  rw [← hf.2 a ha, hg.2]
  exact hf.1 (mem_map_of_mem f ha)

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