map_comp — Mathlib

English

For f: X→Y and g: Y→Z, map(f ≫ g) = map(g) ∘ map(f) on Subobjects.

Русский

Для f: X→Y и g: Y→Z, map(f ≫ g) = map(g) ∘ map(f) на подобъектах.

LaTeX

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

Lean4

theorem map_comp (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] (x : Subobject X) :
    (map (f ≫ g)).obj x = (map g).obj ((map f).obj x) :=
  by
  induction x using Quotient.inductionOn' with
  | _ t
  exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩

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