instQuasiCompactSndScheme — Mathlib

English

For morphisms f: X → Z and g: Y → Z with [QuasiCompact f], the projection snd in the pullback X ×_Z Y → Y is quasi-compact.

Русский

Для морфизмов f: X → Z и g: Y → Z с условием [QuasiCompact f], проекция snd в пуш-бэк-получении X ×_Z Y → Y квази-компактна.

LaTeX

$$$\\forall f,g\\;[QuasiCompact f],\\; \\QuasiCompact(\\pullback.snd f g)$$$

Lean4

instance (f : X ⟶ Z) (g : Y ⟶ Z) [QuasiCompact f] : QuasiCompact (pullback.snd f g) :=
  MorphismProperty.pullback_snd f g inferInstance

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