comp — Mathlib

English

For affine X, Y, a morphism f: X → Y is surjective on stalks if and only if the induced ring map on global sections is surjective on stalks.

Русский

При аффинности X, Y морфизм f: X→Y сюръективен по пикам тогда и только тогда, когда соответствующий гомоморфизм колец (на глобальных сечениях) сюръективен по пикам.

LaTeX

$$iff_of_isAffine: SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (f.app ⊤).hom$$

Lean4

instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [SurjectiveOnStalks f] [SurjectiveOnStalks g] :
    SurjectiveOnStalks (f ≫ g) :=
  MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

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