AlgebraicGeometry.quasiCompact_stableUnderBaseChange
theorem AlgebraicGeometry.quasiCompact_stableUnderBaseChange :
CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.QuasiCompact
The theorem `AlgebraicGeometry.quasiCompact_stableUnderBaseChange` states that the property of being quasi-compact in algebraic geometry is stable under base change. That means for any categories `X`, `Y`, `Y'`, and `S`, and morphisms `f: X ⟶ S`, `g: Y ⟶ S`, `f': Y' ⟶ Y`, `g': Y' ⟶ X`, if `(f', g')` is a pullback of `(g, f)` and `g` is quasi-compact, then `g'` is also quasi-compact.
More concisely: If `g` is quasi-compact and `(f', g')` is the pullback of `(g, f)`, then `g'` is quasi-compact.
|
AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
theorem AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact :
∀ (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace},
IsCompact U.carrier →
∀ (x f : ↑(X.presheaf.obj (Opposite.op U))),
TopCat.Presheaf.restrictOpen x (X.basicOpen f) ⋯ = 0 → ∃ n, f ^ n * x = 0
This theorem states that given an algebraic geometry scheme `X` and a quasi-compact open subset `U` of `X`, if there exists a section `x : Γ(X, U)` of the presheaf on `X` that is zero on the basic open subset `D(f)` for some `f : Γ(X, U)`, then there exists a positive integer `n` such that `f^n * x = 0`. Here, `Γ(X, U)` denotes the sections over `U` of the structure sheaf of `X`, and `D(f)` is the complement of the zero locus of `f`.
More concisely: Given a quasi-compact open subset `U` of an algebraic geometry scheme `X` and a section `x : Γ(X, U)` in the structure sheaf of `X`, if there exists a function `f : Γ(X, U)` such that `x` is zero on the complement of `D(f)`, then there exists a positive integer `n` with `f^n * x = 0`.
|
AlgebraicGeometry.QuasiCompact.isCompact_preimage
theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage :
∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiCompact f]
(U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑f.val.base ⁻¹' U)
The theorem `AlgebraicGeometry.QuasiCompact.isCompact_preimage` states that for any two schemes `X` and `Y` in algebraic geometry, and any morphism `f` from `X` to `Y` that is quasi-compact, if `U` is a compact open set in `Y`, then the preimage of `U` under `f` is also compact. In more formal mathematical terms, this theorem states that for every open and compact set `U` in the codomain of a quasi-compact morphism `f`, the inverse image of `U` under `f` is compact. This relates to the concept of continuity in topological spaces, where the preimage of open sets are open, and extends it to compactness, a property that is important in many areas of mathematics.
More concisely: If `f: X → Y` is a quasi-compact morphism of schemes and `U ⊆ Y` is compact open, then `f⁻¹(U)` is a compact subset of `X`.
|
AlgebraicGeometry.quasiCompact_respectsIso
theorem AlgebraicGeometry.quasiCompact_respectsIso :
CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.QuasiCompact
The theorem `AlgebraicGeometry.quasiCompact_respectsIso` states that the property of being quasi-compact in algebraic geometry respects isomorphisms. More specifically, if a morphism in a category is quasi-compact, then the composition of this morphism with any isomorphism (either before or after it) is also quasi-compact. This means that the quasi-compactness property is preserved under the composition with isomorphisms.
More concisely: If a morphism in algebraic geometry is quasi-compact and if isomorphism is an isomorphism, then the composition of the morphism with isomorphism is quasi-compact.
|
AlgebraicGeometry.quasiCompact_eq_affineProperty
theorem AlgebraicGeometry.quasiCompact_eq_affineProperty :
@AlgebraicGeometry.QuasiCompact =
AlgebraicGeometry.targetAffineLocally AlgebraicGeometry.QuasiCompact.affineProperty
The theorem `AlgebraicGeometry.quasiCompact_eq_affineProperty` establishes an equivalence between the property of being quasi-compact and having the affine target morphism property. Specifically, it states that a geometric object (or scheme, in algebraic geometry terms) is quasi-compact if and only if for every affine open subset of that object, the restriction of the morphism function on that subset also has the property of being quasi-compact. This theorem is thus about connecting a global property (quasi-compactness of the whole scheme) with a local property (quasi-compactness on every affine open subset).
More concisely: A geometric object is quasi-compact if and only if every its affine open subset is quasi-compact.
|
AlgebraicGeometry.QuasiCompact.affineProperty_isLocal
theorem AlgebraicGeometry.QuasiCompact.affineProperty_isLocal : AlgebraicGeometry.QuasiCompact.affineProperty.IsLocal
This theorem, `AlgebraicGeometry.QuasiCompact.affineProperty_isLocal`, states that the property of being a quasi-compact scheme in algebraic geometry is a local property with respect to the target morphism. Concretely, this means that if we have a scheme `X` and for every point in `X`, its fiber (the inverse image of the point under the morphism) is a quasi-compact space (in the sense of CompactSpace), then the entire scheme `X` is said to be quasi-compact. The theorem's proof, which is not provided, would typically involve showing that this property holds regardless of the specific choice of point in `X`.
More concisely: If each fiber of a morphism of schemes is quasi-compact, then the entire scheme is quasi-compact.
|