AlgebraicGeometry.IsAffineOpen.isCompact
theorem AlgebraicGeometry.IsAffineOpen.isCompact :
∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace},
AlgebraicGeometry.IsAffineOpen U → IsCompact ↑U
This theorem states that for any scheme `X` and an open subset `U` of the topological space associated with `X`, if `U` is affine open (meaning the open subscheme corresponding to `U` is affine), then `U` is compact. Here, a set is compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set in the filter intersects every neighborhood of this element.
More concisely: For any scheme `X` and an affine open subset `U` of `X`, `U` is compact.
|
AlgebraicGeometry.isAffineOfIso
theorem AlgebraicGeometry.isAffineOfIso :
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] [h : AlgebraicGeometry.IsAffine Y],
AlgebraicGeometry.IsAffine X
This theorem states that for any two schemes `X` and `Y` in algebraic geometry, if there is an isomorphism `f` between `X` and `Y` and `Y` is an affine scheme, then `X` is also an affine scheme. In other words, the property of being an affine scheme is preserved under isomorphism.
More concisely: If `X` and `Y` are schemes in algebraic geometry with an isomorphism between them and `Y` is affine, then `X` is also affine.
|
AlgebraicGeometry.topIsAffineOpen
theorem AlgebraicGeometry.topIsAffineOpen :
∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X], AlgebraicGeometry.IsAffineOpen ⊤
This theorem states that for any algebraic geometry scheme `X` that is affine, the entire topological space of `X` is an affine open subset. In other words, if `X` has the property of being affine, then the whole of `X` (represented by the top element `⊤` of the lattice of open subsets) is an affine open subscheme. This concept is fundamental in the theory of algebraic geometry, particularly in the study of schemes and their affine open subsets.
More concisely: In algebraic geometry, the top element of the lattice of open subsets of an affine scheme is itself an affine open subscheme.
|
AlgebraicGeometry.of_affine_open_cover
theorem AlgebraicGeometry.of_affine_open_cover :
∀ {X : AlgebraicGeometry.Scheme} (V : ↑X.affineOpens) (S : Set ↑X.affineOpens) {P : ↑X.affineOpens → Prop},
(∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), P U → P (X.affineBasicOpen f)) →
(∀ (U : ↑X.affineOpens) (s : Finset ↑(X.presheaf.obj (Opposite.op ↑U))),
Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U) →
⋃ i, ↑↑↑i = Set.univ → (∀ (U : ↑S), P ↑U) → P V
This theorem, known as the "Affine Communication Lemma", states the following property for an Algebraic Geometry scheme `X`. Suppose we have a predicate `P` that applies to the affine open sets of `X` and satisfies the following conditions:
1. If `P` holds for an affine open set `U`, then `P` also holds for the basic open set corresponding to every section on `U`.
2. If `P` holds for all basic open sets in a family that covers an affine open set `U`, then `P` also holds for `U`.
3. There exists an affine open cover of `X`, each element of which satisfies `P`.
Under these conditions, the theorem asserts that `P` holds for every affine open set of `X`. In other words, the predicate `P` is preserved under the operations of taking basic open subsets and taking covers. This theorem is fundamental in the study of properties that are local in the Zariski topology.
More concisely: Given an Algebraic Geometry scheme `X` and a predicate `P` on its affine open sets satisfying conditions 1-3, `P` holds for every affine open set of `X`.
|
AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion
theorem AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion :
∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] (f : X ⟶ Y)
[H : AlgebraicGeometry.IsOpenImmersion f],
AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.Hom.opensRange f)
The theorem `AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion` states that for any two algebraic schemes `X` and `Y`, where `X` is an affine scheme, and a morphism `f` from `X` to `Y` which is an open immersion, the image of the open immersion `f` as an open set in `Y` is an affine open subset. In simpler words, the theorem asserts that the range of an open immersion from an affine scheme is an affine open subset of the codomain scheme.
More concisely: Given an affine scheme X and a morphism f from X to a scheme Y that is an open immersion, the image of f as an open subset in Y is an affine open subset.
|