comp_app — Mathlib

English

For morphisms f:X→Y, g:Y→Z and open U, the app of the composition equals the composition of apps with the appropriate pullback: (f ≫ g).app U = g.app U ≫ f.app (−).

Русский

Для морфизмов f:X→Y, g:Y→Z и открытого U отображение композиции равно композиции отображений: (f ≫ g).app U = g.app U ≫ f.app (−).

LaTeX

$$$(f \\gg g).app U = g.app U \\gg f.app _$$$

Lean4

@[simp, reassoc] -- reassoc lemma does not need `simp`

theorem comp_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (f ≫ g).app U = g.app U ≫ f.app _ :=
  rfl

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