instLocallyOfFiniteTypeFstScheme — Mathlib

English

If g: Y → S is locally of finite type, then pullback fst f g: X ×_S Y → Y is locally of finite type.

Русский

Если g: Y → S локально по конечному типу, то локальная неизменяемая проекция fst в базовом изменении по f: X → S также локальна по конечному типу.

LaTeX

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

Lean4

instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType g] : LocallyOfFiniteType (pullback.fst f g) :=
  MorphismProperty.pullback_fst f g inferInstance

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