quasiCompact_comp — Mathlib

English

If f and g are quasi-compact morphisms, then their composition is quasi-compact.

Русский

Если f и g квази-компактны, то их композиция квази-компактна.

LaTeX

$$$[QuasiCompact(f)] \land [QuasiCompact(g)] \Rightarrow QuasiCompact(f \circ g)$$$

Lean4

instance quasiCompact_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact f] [QuasiCompact g] :
    QuasiCompact (f ≫ g) := by
  constructor
  intro U hU hU'
  rw [Scheme.comp_base, TopCat.coe_comp, Set.preimage_comp]
  apply QuasiCompact.isCompact_preimage
  · exact Continuous.isOpen_preimage (by fun_prop) _ hU
  apply QuasiCompact.isCompact_preimage <;> assumption

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