comp_surjective — Mathlib

English

Let R be a commutative ring and A, B, C be commutative R-algebras. If f: A → B is of finite type and g: B → C is surjective, then the composition g ∘ f: A → C is of finite type.

Русский

Пусть R — коммутативное кольцо, A, B, C — коммутативные R-алгебры. Если f: A → B является конечного типа, а g: B → C — сюръективный гомоморфизм, то композиция g ∘ f: A → C тоже конечного типа.

LaTeX

$$$\\mathrm{FiniteType}(f) \\wedge \\mathrm{Surjective}(g) \\Rightarrow \\mathrm{FiniteType}(g \\circ f)$$$

Lean4

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

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