map_map — Mathlib

English

Composition of maps corresponds to mapping along the composite functor: (P.map F).map G = P.map(F ⋙ G).

Русский

Слияние отображений соответствует отображению вдоль композиции функторов: (P.map F).map G = P.map(F ⋙ G).

LaTeX

$$$(P.map F).map G = P.map (F \\cdot G)$$$

Lean4

@[simp]
theorem map_map (P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) :
    (P.map F).map G = P.map (F ⋙ G) := by
  apply le_antisymm
  · rw [map_le_iff]
    intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩
  · rw [map_le_iff]
    intro X Y f hf
    exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)

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