quasiCompact_isStableUnderBaseChange

English

Quasi-compactness is stable under base change: the base change of a quasi-compact morphism along any morphism is quasi-compact.

Русский

Квази-компактность стабилизируется при базовом изменении: база-модификация квази-компактного морфизма сохраняет квази-компактность.

LaTeX

$$$\\text{QuasiCompact}$ is stable under base change$$

Lean4

instance quasiCompact_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @QuasiCompact :=
  by
  letI := HasAffineProperty.isLocal_affineProperty @QuasiCompact
  apply HasAffineProperty.isStableUnderBaseChange
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g h
  let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
  have : Finite 𝒰.I₀ := by dsimp [𝒰]; infer_instance
  have : ∀ i, CompactSpace (𝒰.X i) := by intro i; dsimp [𝒰]; infer_instance
  exact 𝒰.compactSpace

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