restrict_restrict — Mathlib

English

If X and Y are schemes over S and f: X ⟶ Y is a morphism with f.IsOver S, then the restriction f.restrict U hU hU' is again over S.

Русский

Пусть X, Y — схемы над S и f: X → Y удовлетворяет f.IsOver S; ограничение f.restrict U hU hU' также является над S.

LaTeX

$$$$\\text{If } [X.Over S], [Y.Over S], \\; f:\\, X\\partialMap Y \\text{ with } f.IsOver S, \\text{ and suitable } U,hU,hU', \\text{ then } (f.restrict U hU hU').IsOver S.$$$$

Lean4

@[simp]
theorem restrict_restrict (f : X.PartialMap Y) (U : X.Opens) (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) (V : X.Opens)
    (hV : Dense (V : Set X)) (hV' : V ≤ U) :
    (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV (hV'.trans hU') := by ext1 <;> simp [restrict_domain]

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