instLocallyOfFinitePresentationSndScheme

English

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

Русский

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

LaTeX

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

Lean4

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

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