Documentation

Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Quasi-compact morphisms #

A morphism of schemes is quasi-compact if the preimages of quasi-compact open sets are quasi-compact.

It suffices to check that preimages of affine open sets are compact (quasiCompact_iff_forall_affine).

theorem AlgebraicGeometry.quasiCompact_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :
AlgebraicGeometry.QuasiCompact f ∀ (U : Set Y.toPresheafedSpace), IsOpen UIsCompact UIsCompact (f.val.base ⁻¹' U)

A morphism is "quasi-compact" if the underlying map of topological spaces is, i.e. if the preimages of quasi-compact open sets are quasi-compact.

  • isCompact_preimage : ∀ (U : Set Y.toPresheafedSpace), IsOpen UIsCompact UIsCompact (f.val.base ⁻¹' U)

    Preimage of compact open set under a quasi-compact morphism between schemes is compact.

Instances
    theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} [self : AlgebraicGeometry.QuasiCompact f] (U : Set Y.toPresheafedSpace) :
    IsOpen UIsCompact UIsCompact (f.val.base ⁻¹' U)

    Preimage of compact open set under a quasi-compact morphism between schemes is compact.

    theorem AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union {X : AlgebraicGeometry.Scheme} (U : Set X.toPresheafedSpace) :
    IsCompact U IsOpen U ∃ (s : Set X.affineOpens), s.Finite U = is, i
    theorem AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (U : Set X.toPresheafedSpace) :
    IsCompact U IsOpen U ∃ (s : Set (X.presheaf.obj (Opposite.op ))), s.Finite U = is, (X.basicOpen i)
    theorem AlgebraicGeometry.isCompact_basicOpen (X : AlgebraicGeometry.Scheme) {U : X.Opens} (hU : IsCompact U) (f : (X.presheaf.obj (Opposite.op U))) :
    IsCompact (X.basicOpen f)
    theorem AlgebraicGeometry.compact_open_induction_on {X : AlgebraicGeometry.Scheme} {P : X.OpensProp} (S : X.Opens) (hS : IsCompact S.carrier) (h₁ : P ) (h₂ : ∀ (S : X.Opens), IsCompact S.carrier∀ (U : X.affineOpens), P SP (S U)) :
    P S
    theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : AlgebraicGeometry.Scheme) {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : (X.presheaf.obj (Opposite.op U))) (f : (X.presheaf.obj (Opposite.op U))) (H : TopCat.Presheaf.restrictOpen x (X.basicOpen f) = 0) :
    ∃ (n : ), f ^ n * x = 0
    theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : AlgebraicGeometry.Scheme) {U : X.Opens} (hU : IsCompact U.carrier) (x : (X.presheaf.obj (Opposite.op U))) (f : (X.presheaf.obj (Opposite.op U))) (H : TopCat.Presheaf.restrictOpen x (X.basicOpen f) = 0) :
    ∃ (n : ), f ^ n * x = 0

    If x : Γ(X, U) is zero on D(f) for some f : Γ(X, U), and U is quasi-compact, then f ^ n * x = 0 for some n.

    theorem AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : IsCompact U) (f : (X.presheaf.obj (Opposite.op U))) :
    IsNilpotent f X.basicOpen f =

    A section over a compact open of a scheme is nilpotent if and only if its associated basic open is empty.

    theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : IsCompact U) (s : Set (X.presheaf.obj (Opposite.op U))) :
    X.zeroLocus s = s (nilradical (X.presheaf.obj (Opposite.op U)))

    The zero locus of a set of sections over a compact open of a scheme is X if and only if s is contained in the nilradical of Γ(X, U).