exists_germ_injective — Mathlib

English

Same statement as above in the spread-out context: injectivity persists to basic opens inside an affine open.

Русский

Та же формулировка в контексте расслоения: инъективность сохраняется при переходе к базовым открытым внутри аффинного открытого множества.

LaTeX

$$$\text{same as above}$$$

Lean4

theorem exists_germ_injective (X : Scheme.{u}) (x : X) [X.IsGermInjectiveAt x] :
    ∃ (U : X.Opens) (hx : x ∈ U), IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx) :=
  Scheme.IsGermInjectiveAt.cond

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