of_comp_finiteType — Mathlib

English

If the composition g ∘ f is finitely presented and f is of finite type, then g is finitely presented.

Русский

Если композиция g∘f конечнопредставима и f имеет конечную презентацию как A-маршрут, то и g конечнопредставим.

LaTeX

$$$(g\\circ f)\\text{ FinitePresentation} \\land f\\text{ FiniteType} \\Rightarrow g\\text{ FinitePresentation}$$$

Lean4

theorem of_comp_finiteType (f : A →+* B) {g : B →+* C} (hg : (g.comp f).FinitePresentation) (hf : f.FiniteType) :
    g.FinitePresentation := by
  algebraize [f, g, g.comp f]
  exact Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C

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