mapComp — Mathlib

English

There is a natural isomorphism between pulling back along f ≫ g and the composition of pullbacks: map (f ≫ g) ≅ map g ⋙ map f.

Русский

Существует естественный изоморфизм между протяжением вдоль f ≫ g и композицией протяжений: map(f ≫ g) ≅ map g ⋙ map f.

LaTeX

$$$map(f\\nrightarrow g) : map(f) \\Rightarrow map(g)$$$

Lean4

/-- The natural isomorphism between taking preimages under `f ≫ g`, and the composite
of taking preimages under `g`, then preimages under `f`.
-/
@[simps]
def mapComp (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) ≅ map g ⋙ map f
    where
  hom := { app := fun U => eqToHom (map_comp_obj f g U) }
  inv := { app := fun U => eqToHom (map_comp_obj f g U).symm }

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