map_comp — Mathlib

English

For morphisms f: S → S' and g: S' → S'', the map respects composition: map n (f ≫ g) = map n f ≫ map n g.

Русский

Для морфизмов f: S → S' и g: S' → S'', отображение сохраняет композицию: map n (f ≫ g) = map n f ≫ map n g.

LaTeX

$$$\\mathrm{map}\\ n\\ (f \\gg \\ g) = \\mathrm{map}\\ n\\ f \\; \\circ \\; \\mathrm{map}\\ n\\ g$$$

Lean4

@[reassoc, simp]
theorem map_comp {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') : map n (f ≫ g) = map n f ≫ map n g :=
  by
  ext1
  · simp
  · simp

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