locallyOfFiniteType_comp — Mathlib

English

Let f: X → Y and g: Y → Z be morphisms of schemes. If f and g are locally of finite type, then their composition f ∘ g is locally of finite type.

Русский

Пусть f: X → Y и g: Y → Z — морфизмы схем. Если f и g локально конечного типа, то их композиция f ∘ g локально конечного типа.

LaTeX

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

Lean4

instance locallyOfFiniteType_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : LocallyOfFiniteType f]
    [hg : LocallyOfFiniteType g] : LocallyOfFiniteType (f ≫ g) :=
  MorphismProperty.comp_mem _ f g hf hg

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