comp_surjective — Mathlib

English

If f is FP and g is surjective with FG kernel, then g ∘ f is FP.

Русский

Если f FP и g сюръективен с FG ядром, то g∘f FP.

LaTeX

$$$f.FinitePresentation \\to g.FinitePresentation \\Rightarrow (g\\circ f).FinitePresentation$$$

Lean4

theorem comp_surjective {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.FinitePresentation) (hg : Surjective g)
    (hker : (RingHom.ker g.toRingHom).FG) : (g.comp f).FinitePresentation :=
  RingHom.FinitePresentation.comp_surjective hf hg hker

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