instLocallyOfFinitePresentationFstScheme

English

If f: X → Z and g: Y → Z with LocallyOfFinitePresentation g, then the pullback fst is LocallyOfFinitePresentation.

Русский

Если g локально конечного типа, то fst-подтягивание по f тоже локально конечного типа.

LaTeX

$$$\text{LocallyOfFinitePresentation}(g) \Rightarrow \text{LocallyOfFinitePresentation}(\text{pullback fst}(f,g)).$$$

Lean4

instance {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [LocallyOfFinitePresentation g] :
    LocallyOfFinitePresentation (Limits.pullback.fst f g) :=
  MorphismProperty.pullback_fst _ _ inferInstance

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