resLE_comp_resLE — Mathlib

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.ι]

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