locallyOfFiniteType_of_comp — Mathlib

English

If the composition f ≫ g is locally of finite type, then f is locally of finite type.

Русский

Если композиция f ≫ g локально по конечному типу, то f локально по конечному типу.

LaTeX

$$$LocallyOfFiniteType(f \\circ g) \\Rightarrow LocallyOfFiniteType(f)$$$

Lean4

theorem locallyOfFiniteType_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFiniteType (f ≫ g)] :
    LocallyOfFiniteType f :=
  HasRingHomProperty.of_comp (fun _ _ ↦ RingHom.FiniteType.of_comp_finiteType) ‹_›

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