algebraic_geometry.open_immersion.Scheme

@[reducible]

def algebraic_geometry.is_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

Prop

A morphism of Schemes is an open immersion if it is an open immersion as a morphism of LocallyRingedSpaces

@[protected]

def algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme (X : algebraic_geometry.LocallyRingedSpace) (h : ∀ (x : ↥X), ∃ (R : CommRing) (f : algebraic_geometry.Spec.to_LocallyRingedSpace.obj (opposite.op R) ⟶ X), x ∈ set.range ⇑(f.val.base) ∧ algebraic_geometry.LocallyRingedSpace.is_open_immersion f) :

algebraic_geometry.Scheme

To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

Equations

algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme X h = {to_LocallyRingedSpace := X, local_affine := _}

source

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

is_open (set.range ⇑(f.val.base))

source

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

Type (max (u+1) (v+1))

J : Type ?
obj : self.J → algebraic_geometry.Scheme
map : Π (j : self.J), self.obj j ⟶ X
f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → self.J
covers : ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), x ∈ set.range ⇑((self.map (self.f x)).val.base)
is_open : (∀ (x : self.J), algebraic_geometry.is_open_immersion (self.map x)) . "apply_instance"

An open cover of X consists of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.

This is merely a coverage in the Zariski pretopology, and it would be optimal if we could reuse the existing API about pretopologies, However, the definitions of sieves and grothendieck topologies uses Props, so that the actual open sets and immersions are hard to obtain. Also, since such a coverage in the pretopology usually contains a proper class of immersions, it is quite hard to glue them, reason about finite covers, etc.

Instances for algebraic_geometry.Scheme.open_cover

algebraic_geometry.Scheme.open_cover.has_sizeof_inst
algebraic_geometry.Scheme.open_cover.inhabited

source

noncomputable def algebraic_geometry.Scheme.affine_cover (X : algebraic_geometry.Scheme) :

X.open_cover

The affine cover of a scheme.

Equations

X.affine_cover = {J := ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), obj := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.Scheme.Spec.obj (opposite.op (Exists.some _)), map := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), (nonempty.some _).inv ≫ X.to_LocallyRingedSpace.of_restrict _, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), x, covers := _, is_open := _}

source

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.open_cover.inhabited {X : algebraic_geometry.Scheme} :

inhabited X.open_cover

Equations

algebraic_geometry.Scheme.open_cover.inhabited = {default := X.affine_cover}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :

(𝒰.bind f).obj x = (f x.fst).obj x.snd

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :

(𝒰.bind f).J = Σ (i : 𝒰.J), (f i).J

source

noncomputable def algebraic_geometry.Scheme.open_cover.bind {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :

X.open_cover

Given an open cover { Uᵢ } of X, and for each Uᵢ an open cover, we may combine these open covers to form an open cover of X.

Equations

𝒰.bind f = {J := Σ (i : 𝒰.J), (f i).J, obj := λ (x : Σ (i : 𝒰.J), (f i).J), (f x.fst).obj x.snd, map := λ (x : Σ (i : 𝒰.J), (f i).J), (f x.fst).map x.snd ≫ 𝒰.map x.fst, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), ⟨𝒰.f x, (f (𝒰.f x)).f (Exists.some _)⟩, covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.bind_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :

(𝒰.bind f).map x = (f x.fst).map x.snd ≫ 𝒰.map x.fst

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_is_iso_map {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (_x : punit) :

(algebraic_geometry.Scheme.open_cover_of_is_iso f).map _x = f

source

@[simp]

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

(algebraic_geometry.Scheme.open_cover_of_is_iso f).J = punit

source

def algebraic_geometry.Scheme.open_cover_of_is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

Y.open_cover

An isomorphism X ⟶ Y is an open cover of Y.

Equations

algebraic_geometry.Scheme.open_cover_of_is_iso f = {J := punit, obj := λ (_x : punit), X, map := λ (_x : punit), f, f := λ (_x : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), punit.star, covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_is_iso_obj {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (_x : punit) :

(algebraic_geometry.Scheme.open_cover_of_is_iso f).obj _x = X

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) (i : J) :

(𝒰.copy J obj map e₁ e₂ e₂_1).map i = map i

source

def algebraic_geometry.Scheme.open_cover.copy {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) :

X.open_cover

We construct an open cover from another, by providing the needed fields and showing that the provided fields are isomorphic with the original open cover.

Equations

𝒰.copy J obj map e₁ e₂ e₂_1 = {J := J, obj := obj, map := map, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), ⇑(e₁.symm) (𝒰.f x), covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) :

(𝒰.copy J obj map e₁ e₂ e₂_1).J = J

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.copy_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J → algebraic_geometry.Scheme) (map : Π (i : J), obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : Π (i : J), obj i ≅ 𝒰.obj (⇑e₁ i)) (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (⇑e₁ i)) (ᾰ : J) :

(𝒰.copy J obj map e₁ e₂ e₂_1).obj ᾰ = obj ᾰ

source

noncomputable def algebraic_geometry.Scheme.open_cover.pushforward_iso {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] :

Y.open_cover

The pushforward of an open cover along an isomorphism.

Equations

𝒰.pushforward_iso f = ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).copy 𝒰.J (λ (_x : 𝒰.J), ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).obj (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x)) (λ (_x : 𝒰.J), ((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).map (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x)) ((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) (λ (_x : 𝒰.J), category_theory.iso.refl (((algebraic_geometry.Scheme.open_cover_of_is_iso f).bind (λ (_x : (algebraic_geometry.Scheme.open_cover_of_is_iso f).J), 𝒰)).obj (⇑((equiv.punit_prod 𝒰.J).symm.trans (equiv.sigma_equiv_prod punit 𝒰.J).symm) _x))) _

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_map {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] (_x : 𝒰.J) :

(𝒰.pushforward_iso f).map _x = 𝒰.map _x ≫ f

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_obj {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] (_x : 𝒰.J) :

(𝒰.pushforward_iso f).obj _x = 𝒰.obj _x

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pushforward_iso_J {X Y : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : X ⟶ Y) [category_theory.is_iso f] :

(𝒰.pushforward_iso f).J = 𝒰.J

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_f {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(𝒰.add f).f x = option.some (𝒰.f x)

source

def algebraic_geometry.Scheme.open_cover.add {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] :

X.open_cover

Adding an open immersion into an open cover gives another open cover.

Equations

𝒰.add f = {J := option 𝒰.J, obj := λ (i : option 𝒰.J), option.rec Y 𝒰.obj i, map := λ (i : option 𝒰.J), option.rec f 𝒰.map i, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), option.some (𝒰.f x), covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (i : option 𝒰.J) :

(𝒰.add f).map i = option.rec f 𝒰.map i

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] :

(𝒰.add f).J = option 𝒰.J

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.add_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Y ⟶ X) [algebraic_geometry.is_open_immersion f] (i : option 𝒰.J) :

(𝒰.add f).obj i = option.rec Y 𝒰.obj i

source

@[protected, instance]

def algebraic_geometry.Scheme.val_base_is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso f.val.base

source

@[protected, instance]

def algebraic_geometry.Scheme.basic_open_is_open_immersion {R : CommRing} (f : ↥R) :

algebraic_geometry.is_open_immersion (algebraic_geometry.Scheme.Spec.map (CommRing.of_hom (algebra_map ↥R (localization.away f))).op)

source

noncomputable def algebraic_geometry.Scheme.affine_basis_cover_of_affine (R : CommRing) :

(algebraic_geometry.Scheme.Spec.obj (opposite.op R)).open_cover

The basic open sets form an affine open cover of Spec R.

Equations

algebraic_geometry.Scheme.affine_basis_cover_of_affine R = {J := ↥R, obj := λ (r : ↥R), algebraic_geometry.Scheme.Spec.obj (opposite.op (CommRing.of (localization.away r))), map := λ (r : ↥R), algebraic_geometry.Scheme.Spec.map (quiver.hom.op (algebra_map ↥R (localization.away r))), f := λ (x : ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), 1, covers := _, is_open := _}

source

noncomputable def algebraic_geometry.Scheme.affine_basis_cover (X : algebraic_geometry.Scheme) :

X.open_cover

We may bind the basic open sets of an open affine cover to form a affine cover that is also a basis.

Equations

X.affine_basis_cover = X.affine_cover.bind (λ (x : X.affine_cover.J), algebraic_geometry.Scheme.affine_basis_cover_of_affine (Exists.some _))

source

noncomputable def algebraic_geometry.Scheme.affine_basis_cover_ring (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

CommRing

The coordinate ring of a component in the affine_basis_cover.

Equations

X.affine_basis_cover_ring i = CommRing.of (localization.away i.snd)

source

theorem algebraic_geometry.Scheme.affine_basis_cover_obj (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

X.affine_basis_cover.obj i = algebraic_geometry.Scheme.Spec.obj (opposite.op (X.affine_basis_cover_ring i))

source

theorem algebraic_geometry.Scheme.affine_basis_cover_map_range (X : algebraic_geometry.Scheme) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (r : ↥(Exists.some _)) :

set.range ⇑((X.affine_basis_cover.map ⟨x, r⟩).val.base) = ⇑((X.affine_cover.map x).val.base) '' (prime_spectrum.basic_open r).carrier

source

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

topological_space.is_topological_basis {x : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) | ∃ (a : X.affine_basis_cover.J), x = set.range ⇑((X.affine_basis_cover.map a).val.base)}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.finite_subcover_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (x : ↥(_.some)) :

𝒰.finite_subcover.obj x = 𝒰.obj (𝒰.f x.val)

source

noncomputable def algebraic_geometry.Scheme.open_cover.finite_subcover {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

X.open_cover

Every open cover of a quasi-compact scheme can be refined into a finite subcover.

Equations

𝒰.finite_subcover = let t : finset ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) := _.some in {J := ↥t, obj := λ (x : ↥t), 𝒰.obj (𝒰.f x.val), map := λ (x : ↥t), 𝒰.map (𝒰.f x.val), f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), Exists.some _, covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.finite_subcover_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (x : ↥(_.some)) :

𝒰.finite_subcover.map x = 𝒰.map (𝒰.f x.val)

source

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.J.fintype {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

fintype 𝒰.finite_subcover.J

Equations

algebraic_geometry.Scheme.J.fintype 𝒰 = id (finset.subtype.fintype _.some)

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme) (f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.Scheme

If X ⟶ Y is an open immersion, and Y is a scheme, then so is X.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f = algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme (algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y.to_LocallyRingedSpace f) _

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_to_LocallyRingedSpace {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme) (f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f).to_LocallyRingedSpace = algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace Y.to_LocallyRingedSpace f

source

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme) (f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f ⟶ Y

If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a Scheme, we can upgrade it into a morphism of Schemes.

Equations

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom Y f = algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom Y.to_LocallyRingedSpace f

source

@[simp]

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom_val {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme) (f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

(algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom Y f).val = f

source

@[protected, instance]

def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom_is_open_immersion {X : algebraic_geometry.PresheafedSpace CommRing} (Y : algebraic_geometry.Scheme) (f : X ⟶ Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) [H : algebraic_geometry.PresheafedSpace.is_open_immersion f] :

algebraic_geometry.is_open_immersion (algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom Y f)

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.Scheme_eq_of_LocallyRingedSpace_eq {X Y : algebraic_geometry.Scheme} (H : X.to_LocallyRingedSpace = Y.to_LocallyRingedSpace) :

X = Y

source

theorem algebraic_geometry.PresheafedSpace.is_open_immersion.Scheme_to_Scheme {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [algebraic_geometry.is_open_immersion f] :

algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y f.val = X

source

def algebraic_geometry.Scheme.restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

algebraic_geometry.Scheme

The restriction of a Scheme along an open embedding.

Equations

X.restrict h = {to_LocallyRingedSpace := {to_SheafedSpace := {to_PresheafedSpace := X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.restrict h, is_sheaf := _}, local_ring := _}, local_affine := _}

Instances for algebraic_geometry.Scheme.restrict

algebraic_geometry.Scheme.restrict.is_integral

source

@[simp]

theorem algebraic_geometry.Scheme.of_restrict_val_base {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

(X.of_restrict h).val.base = f

source

@[simp]

theorem algebraic_geometry.Scheme.of_restrict_val_c_app {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) (V : (topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) :

(X.of_restrict h).val.c.app V = X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (_.adjunction.counit.app (opposite.unop V)).op

source

def algebraic_geometry.Scheme.of_restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

X.restrict h ⟶ X

The canonical map from the restriction to the supspace.

Equations

X.of_restrict h = X.to_LocallyRingedSpace.of_restrict h

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.of_restrict {U : Top} (X : algebraic_geometry.Scheme) {f : U ⟶ Top.of ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : open_embedding ⇑f) :

algebraic_geometry.is_open_immersion (X.of_restrict h)

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.of_is_iso {Y Z : algebraic_geometry.Scheme} (g : Y ⟶ Z) [category_theory.is_iso g] :

algebraic_geometry.is_open_immersion g

source

theorem algebraic_geometry.is_open_immersion.to_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [h : algebraic_geometry.is_open_immersion f] [category_theory.epi f.val.base] :

category_theory.is_iso f

source

theorem algebraic_geometry.is_open_immersion.of_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (hf : open_embedding ⇑(f.val.base)) [∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)] :

algebraic_geometry.is_open_immersion f

source

theorem algebraic_geometry.is_open_immersion.iff_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

algebraic_geometry.is_open_immersion f ↔ open_embedding ⇑(f.val.base) ∧ ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)

source

theorem algebraic_geometry.is_iso_iff_is_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

category_theory.is_iso f ↔ algebraic_geometry.is_open_immersion f ∧ category_theory.epi f.val.base

source

theorem algebraic_geometry.is_iso_iff_stalk_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

category_theory.is_iso f ↔ category_theory.is_iso f.val.base ∧ ∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)), category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map f.val x)

source

noncomputable def algebraic_geometry.is_open_immersion.iso_restrict {X Z : algebraic_geometry.Scheme} (f : X ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

X ≅ Z.restrict _

A open immersion induces an isomorphism from the domain onto the image

Equations

algebraic_geometry.is_open_immersion.iso_restrict f = {hom := (algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict H).hom, inv := (algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict H).inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.mono {X Z : algebraic_geometry.Scheme} (f : X ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.mono f

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.forget_map_is_open_immersion {X Z : algebraic_geometry.Scheme} (f : X ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.map f)

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_left' {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan ((category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inl) ((category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inr))

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_limit_cospan_forget_of_right' {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_limit (category_theory.limits.cospan ((category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inl) ((category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).map category_theory.limits.walking_cospan.hom.inr))

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_creates_pullback_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.creates_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

Equations

algebraic_geometry.is_open_immersion.forget_creates_pullback_of_left f g = category_theory.creates_limit_of_fully_faithful_of_iso (algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y category_theory.limits.pullback.snd.val) (category_theory.eq_to_iso _ ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan f g ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)).symm)

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_creates_pullback_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.creates_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

Equations

algebraic_geometry.is_open_immersion.forget_creates_pullback_of_right f g = category_theory.creates_limit_of_fully_faithful_of_iso (algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme Y category_theory.limits.pullback.fst.val) (category_theory.eq_to_iso _ ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.limits.diagram_iso_cospan (category_theory.limits.cospan g f ⋙ algebraic_geometry.Scheme.forget_to_LocallyRingedSpace)).symm)

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_preserves_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

Equations

algebraic_geometry.is_open_immersion.forget_preserves_of_left f g = category_theory.preserves_limit_of_creates_limit_and_has_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_preserves_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

Equations

algebraic_geometry.is_open_immersion.forget_preserves_of_right f g = category_theory.limits.preserves_pullback_symmetry algebraic_geometry.Scheme.forget_to_LocallyRingedSpace f g

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_pullback_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_pullback f g

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.has_pullback_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.has_pullback g f

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.pullback_snd_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

algebraic_geometry.is_open_immersion category_theory.limits.pullback.snd

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.pullback_fst_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

algebraic_geometry.is_open_immersion category_theory.limits.pullback.fst

source

@[protected, instance]

def algebraic_geometry.is_open_immersion.pullback_to_base {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_open_immersion g] :

algebraic_geometry.is_open_immersion (category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan f g) algebraic_geometry.Scheme.forget_to_Top

Equations

algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_left f g = category_theory.limits.comp_preserves_limit algebraic_geometry.Scheme.forget_to_LocallyRingedSpace algebraic_geometry.LocallyRingedSpace.forget_to_Top

source

@[protected, instance]

noncomputable def algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

category_theory.limits.preserves_limit (category_theory.limits.cospan g f) algebraic_geometry.Scheme.forget_to_Top

Equations

algebraic_geometry.is_open_immersion.forget_to_Top_preserves_of_right f g = category_theory.limits.preserves_pullback_symmetry algebraic_geometry.Scheme.forget_to_Top f g

source

theorem algebraic_geometry.is_open_immersion.range_pullback_snd_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑(category_theory.limits.pullback.snd.val.base) = ↑((topological_space.opens.map g.val.base).obj {carrier := set.range ⇑(f.val.base), is_open' := _})

source

theorem algebraic_geometry.is_open_immersion.range_pullback_fst_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑(category_theory.limits.pullback.fst.val.base) = ↑((topological_space.opens.map g.val.base).obj {carrier := set.range ⇑(f.val.base), is_open' := _})

source

theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_left {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑((category_theory.limits.pullback.fst ≫ f).val.base) = set.range ⇑(f.val.base) ∩ set.range ⇑(g.val.base)

source

theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_right {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] :

set.range ⇑((category_theory.limits.pullback.fst ≫ g).val.base) = set.range ⇑(g.val.base) ∩ set.range ⇑(f.val.base)

source

noncomputable def algebraic_geometry.is_open_immersion.lift {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) :

Y ⟶ X

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Equations

algebraic_geometry.is_open_immersion.lift f g H' = algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift f g H'

source

@[simp]

theorem algebraic_geometry.is_open_immersion.lift_fac {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) :

algebraic_geometry.is_open_immersion.lift f g H' ≫ f = g

source

@[simp]

theorem algebraic_geometry.is_open_immersion.lift_fac_assoc {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) {X' : algebraic_geometry.Scheme} (f' : Z ⟶ X') :

algebraic_geometry.is_open_immersion.lift f g H' ≫ f ≫ f' = g ≫ f'

source

theorem algebraic_geometry.is_open_immersion.lift_uniq {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] (H' : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) (l : Y ⟶ X) (hl : l ≫ f = g) :

l = algebraic_geometry.is_open_immersion.lift f g H'

source

@[simp]

theorem algebraic_geometry.is_open_immersion.iso_of_range_eq_inv {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_open_immersion g] (e : set.range ⇑(f.val.base) = set.range ⇑(g.val.base)) :

(algebraic_geometry.is_open_immersion.iso_of_range_eq f g e).inv = algebraic_geometry.is_open_immersion.lift f g _

source

@[simp]

theorem algebraic_geometry.is_open_immersion.iso_of_range_eq_hom {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_open_immersion g] (e : set.range ⇑(f.val.base) = set.range ⇑(g.val.base)) :

(algebraic_geometry.is_open_immersion.iso_of_range_eq f g e).hom = algebraic_geometry.is_open_immersion.lift g f _

source

noncomputable def algebraic_geometry.is_open_immersion.iso_of_range_eq {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_open_immersion g] (e : set.range ⇑(f.val.base) = set.range ⇑(g.val.base)) :

X ≅ Y

Two open immersions with equal range are isomorphic.

Equations

algebraic_geometry.is_open_immersion.iso_of_range_eq f g e = {hom := algebraic_geometry.is_open_immersion.lift g f _, inv := algebraic_geometry.is_open_immersion.lift f g _, hom_inv_id' := _, inv_hom_id' := _}

source

@[reducible]

def algebraic_geometry.Scheme.hom.opens_functor {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] :

topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) ⥤ topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

The functor opens X ⥤ opens Y associated with an open immersion f : X ⟶ Y.

source

The isomorphism Γ(X, U) ⟶ Γ(Y, f(U)) induced by an open immersion f : X ⟶ Y.

Equations

algebraic_geometry.Scheme.hom.inv_app f U = algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app H U

source

theorem algebraic_geometry.is_open_immersion.app_eq_inv_app_app_of_comp_eq_aux {X Y U : algebraic_geometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = f ≫ g) [h : algebraic_geometry.is_open_immersion g] (V : topological_space.opens ↥(U.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(topological_space.opens.map f.val.base).obj V = (topological_space.opens.map fg.val.base).obj ((algebraic_geometry.Scheme.hom.opens_functor g).obj V)

source

theorem algebraic_geometry.is_open_immersion.app_eq_inv_app_app_of_comp_eq {X Y U : algebraic_geometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = f ≫ g) [h : algebraic_geometry.is_open_immersion g] (V : topological_space.opens ↥(U.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

The fg argument is to avoid nasty stuff about dependent types.

source

theorem algebraic_geometry.is_open_immersion.lift_app {X Y U : algebraic_geometry.Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [h : algebraic_geometry.is_open_immersion f] (H : set.range ⇑(g.val.base) ⊆ set.range ⇑(f.val.base)) (V : topological_space.opens ↥(U.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

source

theorem algebraic_geometry.Scheme.image_basic_open {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)} (r : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

(algebraic_geometry.Scheme.hom.opens_functor f).obj (X.basic_open r) = Y.basic_open (⇑(algebraic_geometry.Scheme.hom.inv_app f U) r)

source

@[simp]

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

↑(algebraic_geometry.Scheme.hom.opens_range f) = set.range ⇑(f.val.base)

source

def algebraic_geometry.Scheme.hom.opens_range {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] :

topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

The image of an open immersion as an open set.

Equations

algebraic_geometry.Scheme.hom.opens_range f = {carrier := set.range ⇑(f.val.base), is_open' := _}

source

@[simp]

theorem algebraic_geometry.Scheme.restrict_functor_map_left (X : algebraic_geometry.Scheme) (U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (i : U ⟶ V) :

(X.restrict_functor.map i).left = algebraic_geometry.is_open_immersion.lift (X.of_restrict _) (X.of_restrict _) _

source

@[simp]

theorem algebraic_geometry.Scheme.restrict_functor_obj_hom (X : algebraic_geometry.Scheme) (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(X.restrict_functor.obj U).hom = X.of_restrict _

source

@[simp]

theorem algebraic_geometry.Scheme.restrict_functor_obj_left (X : algebraic_geometry.Scheme) (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(X.restrict_functor.obj U).left = X.restrict _

source

noncomputable def algebraic_geometry.Scheme.restrict_functor (X : algebraic_geometry.Scheme) :

topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) ⥤ category_theory.over X

The functor taking open subsets of X to open subschemes of X.

Equations

X.restrict_functor = {obj := λ (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), category_theory.over.mk (X.of_restrict _), map := λ (U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (i : U ⟶ V), category_theory.over.hom_mk (algebraic_geometry.is_open_immersion.lift (X.of_restrict _) (X.of_restrict _) _) _, map_id' := _, map_comp' := _}

source

theorem algebraic_geometry.Scheme.restrict_functor_map_of_restrict_assoc (X : algebraic_geometry.Scheme) {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (i : U ⟶ V) {X' : algebraic_geometry.Scheme} (f' : X ⟶ X') :

(X.restrict_functor.map i).left ≫ X.of_restrict _ ≫ f' = X.of_restrict _ ≫ f'

source

theorem algebraic_geometry.Scheme.restrict_functor_map_of_restrict (X : algebraic_geometry.Scheme) {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (i : U ⟶ V) :

(X.restrict_functor.map i).left ≫ X.of_restrict _ = X.of_restrict _

source

theorem algebraic_geometry.Scheme.restrict_functor_map_app_aux (X : algebraic_geometry.Scheme) {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (i : U ⟶ V) (W : topological_space.opens ↥V) :

_.functor.obj ((topological_space.opens.map (X.restrict_functor.map i).left.val.base).obj W) ≤ _.functor.obj W

source

theorem algebraic_geometry.Scheme.restrict_functor_map_app (X : algebraic_geometry.Scheme) {U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (i : U ⟶ V) (W : topological_space.opens ↥V) :

(X.restrict_functor.map i).left.val.c.app (opposite.op W) = X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op

source

noncomputable def algebraic_geometry.Scheme.restrict_functor_Γ (X : algebraic_geometry.Scheme) :

X.restrict_functor.op ⋙ (category_theory.over.forget X).op ⋙ algebraic_geometry.Scheme.Γ ≅ X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf

The functor that restricts to open subschemes and then takes global section is isomorphic to the structure sheaf.

Equations

X.restrict_functor_Γ = category_theory.nat_iso.of_components (λ (U : (topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ), category_theory.functor.map_iso X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf (category_theory.eq_to_iso _).symm.op) _

source

@[reducible]

noncomputable def algebraic_geometry.Scheme.restrict_map_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

X.restrict _ ≅ Y.restrict _

The restriction of an isomorphism onto an open set.

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pullback_cover_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {W : algebraic_geometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) :

(𝒰.pullback_cover f).map x = category_theory.limits.pullback.fst

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pullback_cover_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {W : algebraic_geometry.Scheme} (f : W ⟶ X) :

(𝒰.pullback_cover f).J = 𝒰.J

source

noncomputable def algebraic_geometry.Scheme.open_cover.pullback_cover {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {W : algebraic_geometry.Scheme} (f : W ⟶ X) :

W.open_cover

Given an open cover on X, we may pull them back along a morphism W ⟶ X to obtain an open cover of W.

Equations

𝒰.pullback_cover f = {J := 𝒰.J, obj := λ (x : 𝒰.J), category_theory.limits.pullback f (𝒰.map x), map := λ (x : 𝒰.J), category_theory.limits.pullback.fst, f := λ (x : ↥(W.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), 𝒰.f (⇑(f.val.base) x), covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pullback_cover_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {W : algebraic_geometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) :

(𝒰.pullback_cover f).obj x = category_theory.limits.pullback f (𝒰.map x)

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.pullback_cover_f {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {W : algebraic_geometry.Scheme} (f : W ⟶ X) (x : ↥(W.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(𝒰.pullback_cover f).f x = 𝒰.f (⇑(f.val.base) x)

source

theorem algebraic_geometry.Scheme.open_cover.Union_range {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

(⋃ (i : 𝒰.J), set.range ⇑((𝒰.map i).val.base)) = set.univ

source

theorem algebraic_geometry.Scheme.open_cover.supr_opens_range {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

(⨆ (i : 𝒰.J), algebraic_geometry.Scheme.hom.opens_range (𝒰.map i)) = ⊤

source

theorem algebraic_geometry.Scheme.open_cover.compact_space {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) [finite 𝒰.J] [H : ∀ (i : 𝒰.J), compact_space ↥((𝒰.obj i).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

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

source

noncomputable def algebraic_geometry.Scheme.open_cover.inter {X : algebraic_geometry.Scheme} (𝒰₁ : X.open_cover) (𝒰₂ : X.open_cover) :

X.open_cover

Given open covers { Uᵢ } and { Uⱼ }, we may form the open cover { Uᵢ ∩ Uⱼ }.

Equations

𝒰₁.inter 𝒰₂ = {J := 𝒰₁.J × 𝒰₂.J, obj := λ (ij : 𝒰₁.J × 𝒰₂.J), category_theory.limits.pullback (𝒰₁.map ij.fst) (𝒰₂.map ij.snd), map := λ (ij : 𝒰₁.J × 𝒰₂.J), category_theory.limits.pullback.fst ≫ 𝒰₁.map ij.fst, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), (𝒰₁.f x, 𝒰₂.f x), covers := _, is_open := _}

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_supr_eq_top_obj {s : Type u_1} (X : algebraic_geometry.Scheme) (U : s → topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : (⨆ (i : s), U i) = ⊤) (i : s) :

(X.open_cover_of_supr_eq_top U hU).obj i = X.restrict _

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_supr_eq_top_J {s : Type u_1} (X : algebraic_geometry.Scheme) (U : s → topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : (⨆ (i : s), U i) = ⊤) :

(X.open_cover_of_supr_eq_top U hU).J = s

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover_of_supr_eq_top_map {s : Type u_1} (X : algebraic_geometry.Scheme) (U : s → topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : (⨆ (i : s), U i) = ⊤) (i : s) :

(X.open_cover_of_supr_eq_top U hU).map i = X.of_restrict _

source

noncomputable def algebraic_geometry.Scheme.open_cover_of_supr_eq_top {s : Type u_1} (X : algebraic_geometry.Scheme) (U : s → topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : (⨆ (i : s), U i) = ⊤) :

X.open_cover

If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

Equations

X.open_cover_of_supr_eq_top U hU = {J := s, obj := λ (i : s), X.restrict _, map := λ (i : s), X.of_restrict _, f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), _.some, covers := _, is_open := _}

source

noncomputable def algebraic_geometry.pullback_restrict_iso_restrict {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

category_theory.limits.pullback f (Y.of_restrict _) ≅ X.restrict _

Given a morphism f : X ⟶ Y and an open set U ⊆ Y, we have X ×[Y] U ≅ X |_{f ⁻¹ U}

Equations

algebraic_geometry.pullback_restrict_iso_restrict f U = algebraic_geometry.is_open_immersion.iso_of_range_eq category_theory.limits.pullback.fst (X.of_restrict _) _

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_inv_fst_assoc {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) {X' : algebraic_geometry.Scheme} (f' : X ⟶ X') :

(algebraic_geometry.pullback_restrict_iso_restrict f U).inv ≫ category_theory.limits.pullback.fst ≫ f' = X.of_restrict _ ≫ f'

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_inv_fst {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(algebraic_geometry.pullback_restrict_iso_restrict f U).inv ≫ category_theory.limits.pullback.fst = X.of_restrict _

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_restrict {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(algebraic_geometry.pullback_restrict_iso_restrict f U).hom ≫ X.of_restrict _ = category_theory.limits.pullback.fst

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_restrict_assoc {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) {X' : algebraic_geometry.Scheme} (f' : X ⟶ X') :

(algebraic_geometry.pullback_restrict_iso_restrict f U).hom ≫ X.of_restrict _ ≫ f' = category_theory.limits.pullback.fst ≫ f'

source

noncomputable def algebraic_geometry.morphism_restrict {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

X.restrict _ ⟶ Y.restrict _

The restriction of a morphism X ⟶ Y onto X |_{f ⁻¹ U} ⟶ Y |_ U.

Equations

f ∣_ U = (algebraic_geometry.pullback_restrict_iso_restrict f U).inv ≫ category_theory.limits.pullback.snd

Instances for algebraic_geometry.morphism_restrict

algebraic_geometry.morphism_restrict.category_theory.is_iso

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_morphism_restrict_assoc {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) {X' : algebraic_geometry.Scheme} (f' : Y.restrict _ ⟶ X') :

(algebraic_geometry.pullback_restrict_iso_restrict f U).hom ≫ f ∣_ U ≫ f' = category_theory.limits.pullback.snd ≫ f'

source

@[simp]

theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_morphism_restrict {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(algebraic_geometry.pullback_restrict_iso_restrict f U).hom ≫ f ∣_ U = category_theory.limits.pullback.snd

source

@[simp]

theorem algebraic_geometry.morphism_restrict_ι_assoc {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) {X' : algebraic_geometry.Scheme} (f' : Y ⟶ X') :

f ∣_ U ≫ Y.of_restrict _ ≫ f' = X.of_restrict _ ≫ f ≫ f'

source

@[simp]

theorem algebraic_geometry.morphism_restrict_ι {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

f ∣_ U ≫ Y.of_restrict _ = X.of_restrict _ ≫ f

source

theorem algebraic_geometry.is_pullback_morphism_restrict {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

category_theory.is_pullback (f ∣_ U) (X.of_restrict _) (Y.of_restrict _) f

source

theorem algebraic_geometry.morphism_restrict_comp {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : topological_space.opens ↥(Z.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

(f ≫ g) ∣_ U = f ∣_ (topological_space.opens.map g.val.base).obj U ≫ g ∣_ U

source

@[protected, instance]

def algebraic_geometry.morphism_restrict.category_theory.is_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

category_theory.is_iso (f ∣_ U)

source

theorem algebraic_geometry.morphism_restrict_base_coe {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (x : ↥↑((X.restrict _).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)) :

↑(⇑((f ∣_ U).val.base) x) = ⇑(f.val.base) x.val

source

theorem algebraic_geometry.morphism_restrict_val_base {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

⇑((f ∣_ U).val.base) = U.carrier.restrict_preimage ⇑(f.val.base)

source

theorem algebraic_geometry.image_morphism_restrict_preimage {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (V : topological_space.opens ↥U) :

_.functor.obj ((topological_space.opens.map (f ∣_ U).val.base).obj V) = (topological_space.opens.map f.val.base).obj (_.functor.obj V)

source

theorem algebraic_geometry.morphism_restrict_c_app {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (V : topological_space.opens ↥U) :

(f ∣_ U).val.c.app (opposite.op V) = f.val.c.app (opposite.op (_.functor.obj V)) ≫ X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op

source

noncomputable def algebraic_geometry.morphism_restrict_opens_range {X Y U : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [hg : algebraic_geometry.is_open_immersion g] :

category_theory.arrow.mk (f ∣_ algebraic_geometry.Scheme.hom.opens_range g) ≅ category_theory.arrow.mk category_theory.limits.pullback.snd

Restricting a morphism onto the the image of an open immersion is isomorphic to the base change along the immersion.

Equations

algebraic_geometry.morphism_restrict_opens_range f g = let V : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) := algebraic_geometry.Scheme.hom.opens_range g, e : U ≅ Y.restrict _ := algebraic_geometry.is_open_immersion.iso_of_range_eq g (Y.of_restrict _) _, t : category_theory.limits.pullback f g ⟶ category_theory.limits.pullback f (Y.of_restrict _) := category_theory.limits.pullback.map f g f (Y.of_restrict _) (𝟙 X) e.hom (𝟙 Y) _ _ in (category_theory.arrow.iso_mk (category_theory.as_iso t ≪≫ algebraic_geometry.pullback_restrict_iso_restrict f V) e _).symm

source

noncomputable def algebraic_geometry.morphism_restrict_eq {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) {U V : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (e : U = V) :

category_theory.arrow.mk (f ∣_ U) ≅ category_theory.arrow.mk (f ∣_ V)

The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.

Equations