isFinitelyPresentable — Mathlib

English

If S is a finitely presented R-algebra, then S (viewed as an object of Under R) is finitely presentable.

Русский

Если S — конечно порожденная по отношению к R алгебра, то S как объект в категории Under R является конечнопредставимым.

LaTeX

$$$\text{IsFinitelyPresentable}(S)$$$

Lean4

/-- If `S` is a finitely presented `R`-algebra, `S : Under R` is finitely presentable. -/
theorem isFinitelyPresentable (S : Under R) (hS : S.hom.hom.FinitePresentation) : IsFinitelyPresentable.{u} S :=
  by
  rw [isFinitelyPresentable_iff_preservesFilteredColimits]
  exact preservesFilteredColimits_coyoneda R S hS

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