respectsLeft_isOpenImmersion — Mathlib

English

If P is local at the source, then P respects left composition with open immersions; that is, for any open immersion i and any morphism f, P f implies P (i ≫ f).

Русский

Если P локально по источнику, то P сохраняется при левой композиции с открытыми вложениями: для любого открытого вложения i и морфизма f выполняется, что P(f) ⇒ P(i ≫ f).

LaTeX

$$$\forall {P : \mathrm{MorphismProperty}(\mathrm{Scheme})} [\mathrm{IsZariskiLocalAtSource} P],\\ \forall X,Y : \mathrm{Scheme}, \forall f : X \to Y, \forall UX : \mathrm{Scheme}, \forall i : UX \to X, [\mathrm{IsOpenImmersion} i],\\ P f \Rightarrow P (i \circ f).$$$$

Lean4

/-- If `P` is local at the source, then it respects composition on the left with open immersions. -/
instance respectsLeft_isOpenImmersion {P : MorphismProperty Scheme} [IsZariskiLocalAtSource P] :
    P.RespectsLeft @IsOpenImmersion where precomp i _ _ hf := IsZariskiLocalAtSource.comp hf i

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