English
For f: X → Y and g: Y → Z, precomposing two successive restrictions equals the restriction of the composite morphism: f followed by g restricted to appropriate opens.
Русский
Для f: X → Y и g: Y → Z композиция двух последовательных ограничений равна ограничению композиции: ограничение f затем ограничение g на подходящих открытиях.
LaTeX
$$$f.resLE U V e \;\circ g.resLE W U e' = (f\,\nabla\,g).resLE W V (e\,\.trans\,((Opens.map f.base).map (homOfLE e')).le)$$$
Lean4
@[reassoc]
theorem resLE_comp_resLE {Z : Scheme.{u}} (g : Y ⟶ Z) {W : Z.Opens} (e') :
f.resLE U V e ≫ g.resLE W U e' = (f ≫ g).resLE W V (e.trans ((Opens.map f.base).map (homOfLE e')).le) := by
simp [← cancel_mono W.ι]