comp — Mathlib

English

If hg and hf are surjective-on-stalks, then their composition is surjective-on-stalks: (g ∘ f).SurjectiveOnStalks.

Русский

Если g и f сюръективны на стэках, то композиция g ∘ f также сюръективна на стэках.

LaTeX

$$$\\text{If } g.SurjectiveOnStalks \\text{ and } f.SurjectiveOnStalks,\\ (g \\circ f).SurjectiveOnStalks$$$

Lean4

theorem comp (hg : SurjectiveOnStalks g) (hf : SurjectiveOnStalks f) : SurjectiveOnStalks (g.comp f) :=
  by
  intro I hI
  have := (hg I hI).comp (hf _ (hI.comap g))
  rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this

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