instIsMultiplicativeScheme — Mathlib

English

If f and g both have SurjectiveOnStalks, then their composition f ≫ g also has SurjectiveOnStalks.

Русский

Если оба морфизма f и g обладают суръективностью по пикам, то и их композиция сохраняет это свойство.

LaTeX

$$If SurjectiveOnStalks f and SurjectiveOnStalks g, then SurjectiveOnStalks (f ≫ g)$$

Lean4

instance : MorphismProperty.IsMultiplicative @SurjectiveOnStalks
    where
  id_mem _ := inferInstance
  comp_mem {X Y Z} f g hf
    hg := by
    refine ⟨fun x ↦ ?_⟩
    rw [Scheme.stalkMap_comp]
    exact (hf.surj_on_stalks x).comp (hg.surj_on_stalks (f.base x))

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