mathlib3 documentation

algebraic_geometry.AffineScheme

Affine schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the category of AffineSchemes as the essential image of Spec. We also define predicates about affine schemes and affine open sets.

Main definitions #

algebraic_geometry.AffineScheme: The category of affine schemes.
algebraic_geometry.is_affine: A scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.
algebraic_geometry.Scheme.iso_Spec: The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.
algebraic_geometry.AffineScheme.equiv_CommRing: The equivalence of categories AffineScheme ≌ CommRingᵒᵖ given by AffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme and AffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRing.
algebraic_geometry.is_affine_open: An open subset of a scheme is affine if the open subscheme is affine.
algebraic_geometry.is_affine_open.from_Spec: The immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.category :

category_theory.category algebraic_geometry.AffineScheme

@[nolint]

def algebraic_geometry.AffineScheme :

Type (u_1+1)

The category of affine schemes

Equations

algebraic_geometry.AffineScheme = algebraic_geometry.Scheme.Spec.ess_image_subcategory

Instances for algebraic_geometry.AffineScheme

@[class]

structure algebraic_geometry.is_affine (X : algebraic_geometry.Scheme) :

Prop

affine : category_theory.is_iso (algebraic_geometry.Γ_Spec.adjunction.unit.app X)

A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

Instances of this typeclass

noncomputable def algebraic_geometry.Scheme.iso_Spec (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

X ≅ algebraic_geometry.Scheme.Spec.obj (opposite.op (algebraic_geometry.Scheme.Γ.obj (opposite.op X)))

The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.

Equations

X.iso_Spec = category_theory.as_iso (algebraic_geometry.Γ_Spec.adjunction.unit.app X)

@[simp]

theorem algebraic_geometry.AffineScheme.mk_obj (X : algebraic_geometry.Scheme) (h : algebraic_geometry.is_affine X) :

(algebraic_geometry.AffineScheme.mk X h).obj = X

def algebraic_geometry.AffineScheme.mk (X : algebraic_geometry.Scheme) (h : algebraic_geometry.is_affine X) :

algebraic_geometry.AffineScheme

Construct an affine scheme from a scheme and the information that it is affine. Also see AffineScheme.of for a typclass version.

Equations

algebraic_geometry.AffineScheme.mk X h = {obj := X, property := _}

def algebraic_geometry.AffineScheme.of (X : algebraic_geometry.Scheme) [h : algebraic_geometry.is_affine X] :

algebraic_geometry.AffineScheme

Construct an affine scheme from a scheme. Also see AffineScheme.mk for a non-typeclass version.

Equations

algebraic_geometry.AffineScheme.of X = algebraic_geometry.AffineScheme.mk X h

def algebraic_geometry.AffineScheme.of_hom {X Y : algebraic_geometry.Scheme} [algebraic_geometry.is_affine X] [algebraic_geometry.is_affine Y] (f : X ⟶ Y) :

algebraic_geometry.AffineScheme.of X ⟶ algebraic_geometry.AffineScheme.of Y

Type check a morphism of schemes as a morphism in AffineScheme.

Equations

algebraic_geometry.AffineScheme.of_hom f = f

theorem algebraic_geometry.mem_Spec_ess_image (X : algebraic_geometry.Scheme) :

X ∈ algebraic_geometry.Scheme.Spec.ess_image ↔ algebraic_geometry.is_affine X

@[protected, instance]

def algebraic_geometry.is_affine_AffineScheme (X : algebraic_geometry.AffineScheme) :

algebraic_geometry.is_affine X.obj

@[protected, instance]

def algebraic_geometry.Spec_is_affine (R : CommRing ᵒᵖ) :

algebraic_geometry.is_affine (algebraic_geometry.Scheme.Spec.obj R)

theorem algebraic_geometry.is_affine_of_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] [h : algebraic_geometry.is_affine Y] :

algebraic_geometry.is_affine X

@[protected, instance]

def algebraic_geometry.AffineScheme.Spec.ess_surj :

category_theory.ess_surj algebraic_geometry.AffineScheme.Spec

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.Spec.full :

category_theory.full algebraic_geometry.AffineScheme.Spec

@[protected, instance]

def algebraic_geometry.AffineScheme.Spec.faithful :

category_theory.faithful algebraic_geometry.AffineScheme.Spec

noncomputable def algebraic_geometry.AffineScheme.Spec :

CommRing ᵒᵖ ⥤ algebraic_geometry.AffineScheme

The Spec functor into the category of affine schemes.

Equations

algebraic_geometry.AffineScheme.Spec = algebraic_geometry.Scheme.Spec.to_ess_image

Instances for algebraic_geometry.AffineScheme.Spec

@[protected, instance]

def algebraic_geometry.AffineScheme.forget_to_Scheme.faithful :

category_theory.faithful algebraic_geometry.AffineScheme.forget_to_Scheme

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.forget_to_Scheme.full :

category_theory.full algebraic_geometry.AffineScheme.forget_to_Scheme

@[simp]

theorem algebraic_geometry.AffineScheme.forget_to_Scheme_map (x y : category_theory.induced_category algebraic_geometry.Scheme category_theory.full_subcategory.obj) (f : x ⟶ y) :

algebraic_geometry.AffineScheme.forget_to_Scheme.map f = f

noncomputable def algebraic_geometry.AffineScheme.forget_to_Scheme :

algebraic_geometry.AffineScheme ⥤ algebraic_geometry.Scheme

The forgetful functor AffineScheme ⥤ Scheme.

Equations

algebraic_geometry.AffineScheme.forget_to_Scheme = algebraic_geometry.Scheme.Spec.ess_image_inclusion

Instances for algebraic_geometry.AffineScheme.forget_to_Scheme

@[simp]

theorem algebraic_geometry.AffineScheme.forget_to_Scheme_obj (self : category_theory.full_subcategory algebraic_geometry.Scheme.Spec.ess_image) :

algebraic_geometry.AffineScheme.forget_to_Scheme.obj self = self.obj

noncomputable def algebraic_geometry.AffineScheme.Γ :

algebraic_geometry.AffineScheme ᵒᵖ ⥤ CommRing

The global section functor of an affine scheme.

Equations

algebraic_geometry.AffineScheme.Γ = algebraic_geometry.AffineScheme.forget_to_Scheme.op ⋙ algebraic_geometry.Scheme.Γ

Instances for algebraic_geometry.AffineScheme.Γ

algebraic_geometry.AffineScheme.Γ_is_equiv

noncomputable def algebraic_geometry.AffineScheme.equiv_CommRing :

algebraic_geometry.AffineScheme ≌ CommRing ᵒᵖ

The category of affine schemes is equivalent to the category of commutative rings.

Equations

algebraic_geometry.AffineScheme.equiv_CommRing = category_theory.equiv_ess_image_of_reflective.symm

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.Γ_is_equiv :

category_theory.is_equivalence algebraic_geometry.AffineScheme.Γ

Equations

algebraic_geometry.AffineScheme.Γ_is_equiv = algebraic_geometry.AffineScheme.Γ.right_op.op.is_equivalence_trans (category_theory.op_op_equivalence CommRing).functor

@[protected, instance]

def algebraic_geometry.AffineScheme.category_theory.limits.has_colimits :

category_theory.limits.has_colimits algebraic_geometry.AffineScheme

@[protected, instance]

def algebraic_geometry.AffineScheme.category_theory.limits.has_limits :

category_theory.limits.has_limits algebraic_geometry.AffineScheme

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.right_op.category_theory.limits.preserves_limits :

category_theory.limits.preserves_limits algebraic_geometry.AffineScheme.Γ.right_op

Equations

algebraic_geometry.AffineScheme.right_op.category_theory.limits.preserves_limits = category_theory.adjunction.is_equivalence_preserves_limits algebraic_geometry.AffineScheme.Γ.right_op

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.forget_to_Scheme.category_theory.limits.preserves_limits :

category_theory.limits.preserves_limits algebraic_geometry.AffineScheme.forget_to_Scheme

Equations

algebraic_geometry.AffineScheme.forget_to_Scheme.category_theory.limits.preserves_limits = category_theory.limits.preserves_limits_of_nat_iso (category_theory.iso_whisker_right algebraic_geometry.AffineScheme.equiv_CommRing.unit_iso algebraic_geometry.AffineScheme.forget_to_Scheme).symm

def algebraic_geometry.is_affine_open {X : algebraic_geometry.Scheme} (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

Prop

An open subset of a scheme is affine if the open subscheme is affine.

Equations

algebraic_geometry.is_affine_open U = algebraic_geometry.is_affine (X.restrict _)

def algebraic_geometry.Scheme.affine_opens (X : algebraic_geometry.Scheme) :

set (topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))

The set of affine opens as a subset of opens X.carrier.

Equations

X.affine_opens = {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) | algebraic_geometry.is_affine_open U}

theorem algebraic_geometry.range_is_affine_open_of_open_immersion {X Y : algebraic_geometry.Scheme} [algebraic_geometry.is_affine X] (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] :

algebraic_geometry.is_affine_open (algebraic_geometry.Scheme.hom.opens_range f)

theorem algebraic_geometry.top_is_affine_open (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

algebraic_geometry.is_affine_open ⊤

@[protected, instance]

def algebraic_geometry.Scheme.affine_cover_is_affine (X : algebraic_geometry.Scheme) (i : X.affine_cover.J) :

algebraic_geometry.is_affine (X.affine_cover.obj i)

@[protected, instance]

def algebraic_geometry.Scheme.affine_basis_cover_is_affine (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

algebraic_geometry.is_affine (X.affine_basis_cover.obj i)

theorem algebraic_geometry.is_basis_affine_open (X : algebraic_geometry.Scheme) :

topological_space.opens.is_basis X.affine_opens

noncomputable def algebraic_geometry.is_affine_open.from_Spec {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) ⟶ X

The open immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

Equations

hU.from_Spec = algebraic_geometry.Scheme.Spec.map (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom algebraic_geometry.is_affine_open.from_Spec._proof_2).op).op ≫ (X.restrict algebraic_geometry.is_affine_open.from_Spec._proof_3).iso_Spec.inv ≫ X.of_restrict algebraic_geometry.is_affine_open.from_Spec._proof_4

@[protected, instance]

def algebraic_geometry.is_affine_open.is_open_immersion_from_Spec {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

algebraic_geometry.is_open_immersion hU.from_Spec

theorem algebraic_geometry.is_affine_open.from_Spec_range {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

set.range ⇑(hU.from_Spec.val.base) = ↑U

theorem algebraic_geometry.is_affine_open.from_Spec_image_top {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

_.functor.obj ⊤ = U

theorem algebraic_geometry.is_affine_open.is_compact {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

is_compact ↑U

theorem algebraic_geometry.is_affine_open.image_is_open_immersion {X Y : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] :

algebraic_geometry.is_affine_open ((algebraic_geometry.Scheme.hom.opens_functor f).obj U)

theorem algebraic_geometry.is_affine_open_iff_of_is_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

algebraic_geometry.is_affine_open ((algebraic_geometry.PresheafedSpace.is_open_immersion.open_functor H).obj U) ↔ algebraic_geometry.is_affine_open U

@[protected, instance]

def algebraic_geometry.Scheme.quasi_compact_of_affine (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

theorem algebraic_geometry.is_affine_open.from_Spec_base_preimage {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

(topological_space.opens.map hU.from_Spec.val.base).obj U = ⊤

theorem algebraic_geometry.is_affine_open.basic_open_is_affine {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

algebraic_geometry.is_affine_open (X.basic_open f)

theorem algebraic_geometry.Scheme.map_prime_spectrum_basic_open_of_affine (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] (f : ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op X))) :

(topological_space.opens.map X.iso_Spec.hom.val.base).obj (prime_spectrum.basic_open f) = X.basic_open f

theorem algebraic_geometry.is_basis_basic_open (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

topological_space.opens.is_basis (set.range X.basic_open)

theorem algebraic_geometry.is_affine_open.exists_basic_open_le {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) {V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (x : ↥V) (h : ↑x ∈ U) :

∃ (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))), X.basic_open f ≤ V ∧ ↑x ∈ X.basic_open f

@[protected, instance]

Equations

algebraic_geometry.obj.algebra f = ring_hom.to_algebra (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op)

theorem algebraic_geometry.is_affine_open.opens_map_from_Spec_basic_open {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

noncomputable def algebraic_geometry.basic_open_sections_to_affine {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

The canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(Spec_Γ_identity.inv f)) This is an isomorphism, as witnessed by an is_iso instance.

Equations

Instances for algebraic_geometry.basic_open_sections_to_affine

algebraic_geometry.basic_open_sections_to_affine.category_theory.is_iso

@[protected, instance]

def algebraic_geometry.basic_open_sections_to_affine.category_theory.is_iso {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

category_theory.is_iso (algebraic_geometry.basic_open_sections_to_affine hU f)

@[protected, instance]

theorem algebraic_geometry.is_localization_of_eq_basic_open {X : algebraic_geometry.Scheme} {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (i : V ⟶ U) (hU : algebraic_geometry.is_affine_open U) (r : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (e : V = X.basic_open r) :

is_localization.away r ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op V))

@[protected, instance]

def algebraic_geometry.Γ_restrict_algebra {X : algebraic_geometry.Scheme} {Y : Top} {f : Y ⟶ X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier} (hf : open_embedding ⇑f) :

algebra ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op X)) ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op (X.restrict hf)))

Equations

algebraic_geometry.Γ_restrict_algebra hf = ring_hom.to_algebra (algebraic_geometry.Scheme.Γ.map (X.of_restrict hf).op)

@[protected, instance]

def algebraic_geometry.Γ_restrict_is_localization (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] (r : ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op X))) :

is_localization.away r ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op (X.restrict _)))

theorem algebraic_geometry.basic_open_basic_open_is_basic_open {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (g : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.basic_open f)))) :

∃ (f' : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))), X.basic_open f' = X.basic_open g

theorem algebraic_geometry.exists_basic_open_le_affine_inter {X : algebraic_geometry.Scheme} {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (hV : algebraic_geometry.is_affine_open V) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hx : x ∈ U ⊓ V) :

∃ (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (g : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op V))), X.basic_open f = X.basic_open g ∧ x ∈ X.basic_open f

noncomputable def algebraic_geometry.is_affine_open.prime_ideal_of {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (x : ↥U) :

prime_spectrum ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))

The prime ideal of 𝒪ₓ(U) corresponding to a point x : U.

Equations

hU.prime_ideal_of x = ⇑((algebraic_geometry.Scheme.Spec.map (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom algebraic_geometry.is_affine_open.prime_ideal_of._proof_2).op).op).val.base) (⇑((X.restrict algebraic_geometry.is_affine_open.prime_ideal_of._proof_3).iso_Spec.hom.val.base) x)

theorem algebraic_geometry.is_affine_open.from_Spec_prime_ideal_of {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (x : ↥U) :

⇑(hU.from_Spec.val.base) (hU.prime_ideal_of x) = x.val

theorem algebraic_geometry.is_affine_open.is_localization_stalk_aux {X : algebraic_geometry.Scheme} (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) [algebraic_geometry.is_affine (X.restrict _)] :

@[simp]

theorem algebraic_geometry.Scheme.affine_basic_open_coe (X : algebraic_geometry.Scheme) {U : ↥(X.affine_opens)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ↑U))) :

↑(X.affine_basic_open f) = X.basic_open f

def algebraic_geometry.Scheme.affine_basic_open (X : algebraic_geometry.Scheme) {U : ↥(X.affine_opens)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ↑U))) :

↥(X.affine_opens)

The basic open set of a section f on an an affine open as an X.affine_opens.

Equations

X.affine_basic_open f = ⟨X.basic_open f, _⟩

theorem algebraic_geometry.is_affine_open.basic_open_union_eq_self_iff {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (s : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

(⨆ (f : ↥s), X.basic_open ↑f) = U ↔ ideal.span s = ⊤

theorem algebraic_geometry.is_affine_open.self_le_basic_open_union_iff {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) (s : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

(U ≤ ⨆ (f : ↥s), X.basic_open ↑f) ↔ ideal.span s = ⊤

theorem algebraic_geometry.of_affine_open_cover {X : algebraic_geometry.Scheme} (V : ↥(X.affine_opens)) (S : set ↥(X.affine_opens)) {P : ↥(X.affine_opens) → Prop} (hP₁ : ∀ (U : ↥(X.affine_opens)) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U.val))), P U → P (X.affine_basic_open f)) (hP₂ : ∀ (U : ↥(X.affine_opens)) (s : finset ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ↑U))), ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affine_basic_open f.val)) → P U) (hS : (⋃ (i : ↥S), ↑i) = set.univ) (hS' : ∀ (U : ↥S), P ↑U) :

P V

Let P be a predicate on the affine open sets of X satisfying

If P holds on U, then P holds on the basic open set of every section on U.
If P holds for a family of basic open sets covering U, then P holds for U.
There exists an affine open cover of X each satisfying P.

Then P holds for every affine open of X.

This is also known as the Affine communication lemma in The rising sea.