AlgebraicGeometry.is_localization_basicOpen_of_qcqs
theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs :
∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace},
IsCompact U.carrier →
IsQuasiSeparated U.carrier →
∀ (f : ↑(X.presheaf.obj (Opposite.op U))),
IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
In the field of algebraic geometry, the **Qcqs lemma** (as introduced by R. Vakil in "The rising sea") establishes a key relationship between certain topological spaces and their localizations. Specifically, the theorem states that for any scheme `X` and any open subset `U` of `X` (as represented in the category of topological spaces), if the carrier of `U` is both compact and quasi-separated (abbreviated as qcqs), then for any section `f` of the structure sheaf of `X` over `U`, the space of global sections of `X` localized at the basic open set defined by `f` is isomorphic to the localization of the space of global sections of `X` over `U` at `f`. The localization here is with respect to the submonoid of `R` generated by `f`.
More concisely: For any scheme `X` and open subset `U` with compact and quasi-separated carrier, the space of global sections of `X` localized at the basic open set defined by a section `f` of the structure sheaf over `U` is isomorphic to the localization of the space of global sections of `X` over `U` at `f`.
|
AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact
theorem AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact :
∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiSeparated f],
AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)
The theorem `AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact` states that for any two algebraic geometry schemes `X` and `Y`, and for a morphism `f` from `X` to `Y`, if the morphism `f` is quasi-separated, then the diagonal morphism of the pullback of `f` is quasi-compact. The diagonal morphism of the pullback is defined as the morphism from `X` to the object `Δ_{X/Y}` in the category `C`. A morphism is called quasi-separated if it satisfies certain conditions related to the intersection of the inverse images of open sets in `Y`. The concept of a morphism being quasi-compact relates to the property that the inverse image of any quasi-compact open subset under the morphism is again quasi-compact.
More concisely: If `f` is a quasi-separated morphism from scheme `X` to `Y`, then the diagonal morphism of `f`'s pullback is quasi-compact.
|
AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact
theorem AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact :
@AlgebraicGeometry.QuasiSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.QuasiCompact := by
sorry
The theorem `AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact` states that a scheme in algebraic geometry is quasi-separated if and only if the property of being quasi-compact is preserved under taking the diagonal morphism in the category theory sense. Here, the diagonal morphism refers to the morphism induced by the pullback of a given morphism with itself.
More concisely: A scheme is quasi-separated if and only if the diagonal morphism is quasi-compact in the category of schemes.
|