locallyOfFiniteType_isStableUnderBaseChange

English

LocallyOfFiniteType is stable under base change: if g: Y → S is locally of finite type, then the pullback fst: X ×_S Y → Y is locally of finite type.

Русский

Локально конечный тип устойчив к базовым изменениям: если g: Y → S локально константен по типу, то проекция на основание после базового изменения локально конечного типа.

LaTeX

$$$LocallyOfFiniteType(g) \\Rightarrow LocallyOfFiniteType( pullback.fst f g )$$$

Lean4

instance locallyOfFiniteType_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @LocallyOfFiniteType :=
  HasRingHomProperty.isStableUnderBaseChange RingHom.finiteType_isStableUnderBaseChange

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