map_comp — Mathlib

English

Composition compatibility: map of a composition equals composition of maps.

Русский

Согласование композиции: map(f ≫ g) = (map f) . map g.

LaTeX

$$map (f ≫ g) = (map f).map g$$

Lean4

@[simp]
theorem map_comp (I : X.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z) : I.map (f ≫ g) = (I.map f).map g :=
  by
  apply le_antisymm
  · rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]; exact comap_map_le _ _
  · rw [le_map_iff_comap_le, comap_comp]
    exact (comap_mono _ (comap_map_le _ _)).trans (comap_map_le _ _)

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