of_comp — Mathlib

English

If the composite g ∘ f is surjective on stalks, then g is surjective on stalks.

Русский

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

LaTeX

$$$ (g \\circ f).SurjectiveOnStalks \\Rightarrow g.SurjectiveOnStalks $$$

Lean4

theorem of_comp (hg : SurjectiveOnStalks (g.comp f)) : SurjectiveOnStalks g :=
  by
  intro I hI
  have := hg I hI
  rw [Localization.localRingHom_comp (I.comap (g.comp f)) (I.comap g) _ _ rfl _ rfl, RingHom.coe_comp] at this
  exact this.of_comp

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