Open immersions of schemes

@[inline, reducible]

abbrev AlgebraicGeometry.IsOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

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

Equations

• AlgebraicGeometry.IsOpenImmersion f = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f

instance AlgebraicGeometry.IsOpenImmersion.comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme (X : AlgebraicGeometry.LocallyRingedSpace) (h : ∀ (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)), ∃ (R : CommRingCat) (f : AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R) ⟶ X), x ∈ Set.range ⇑f.val.base ∧ AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f) : AlgebraicGeometry.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

• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme X h = { toLocallyRingedSpace := X, local_affine := ⋯ }

theorem AlgebraicGeometry.IsOpenImmersion.isOpen_range {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : IsOpen (Set.range ⇑f.val.base)

@[deprecated AlgebraicGeometry.IsOpenImmersion.isOpen_range]

theorem AlgebraicGeometry.IsOpenImmersion.open_range {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : IsOpen (Set.range ⇑f.val.base)

Alias of AlgebraicGeometry.IsOpenImmersion.isOpen_range.

structure AlgebraicGeometry.Scheme.OpenCover (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) (v + 1))

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.

• J : Type v

  index set of an open cover of a scheme X

• obj : self.J → AlgebraicGeometry.Scheme

  the subschemes of an open cover

• map : (j : self.J) → self.obj j ⟶ X

  the embedding of subschemes to X

• f : ↑↑X.toPresheafedSpace → self.J

  given a point of x : X, f x is the index of the subscheme which contains x

• Covers : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(self.map (self.f x)).val.base

  the subschemes covers X

• IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

  the embedding of subschemes are open immersions

def AlgebraicGeometry.Scheme.affineCover (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.OpenCover X

The affine cover of a scheme.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instInhabitedOpenCover {X : AlgebraicGeometry.Scheme} : Inhabited (AlgebraicGeometry.Scheme.OpenCover X)

Equations

• AlgebraicGeometry.Scheme.instInhabitedOpenCover = { default := AlgebraicGeometry.Scheme.affineCover X }

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (𝒰.obj x)) (x : (i : 𝒰.J) × (f i).J) : (AlgebraicGeometry.Scheme.OpenCover.bind 𝒰 f).map x = CategoryTheory.CategoryStruct.comp ((f x.fst).map x.snd) (𝒰.map x.fst)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (𝒰.obj x)) (x : (i : 𝒰.J) × (f i).J) : (AlgebraicGeometry.Scheme.OpenCover.bind 𝒰 f).obj x = (f x.fst).obj x.snd

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_J {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (𝒰.obj x)) : (AlgebraicGeometry.Scheme.OpenCover.bind 𝒰 f).J = ((i : 𝒰.J) × (f i).J)

def AlgebraicGeometry.Scheme.OpenCover.bind {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (𝒰.obj x)) : AlgebraicGeometry.Scheme.OpenCover X

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : PUnit.{v + 1} ), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).map x = f

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (AlgebraicGeometry.Scheme.openCoverOfIsIso f).J = PUnit.{v + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : PUnit.{v + 1} ), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).obj x = X

def AlgebraicGeometry.Scheme.openCoverOfIsIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.OpenCover Y

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_J {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : (AlgebraicGeometry.Scheme.OpenCover.copy 𝒰 J obj map e₁ e₂✝ e₂).J = J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : ∀ (a : J), (AlgebraicGeometry.Scheme.OpenCover.copy 𝒰 J obj map e₁ e₂✝ e₂).obj a = obj a

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) (i : J) : (AlgebraicGeometry.Scheme.OpenCover.copy 𝒰 J obj map e₁ e₂✝ e₂).map i = map i

def AlgebraicGeometry.Scheme.OpenCover.copy {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : AlgebraicGeometry.Scheme.OpenCover X

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

• AlgebraicGeometry.Scheme.OpenCover.copy 𝒰 J obj map e₁ e₂✝ e₂ = { J := J, obj := obj, map := map, f := fun (x : ↑↑X.toPresheafedSpace) => e₁.symm (𝒰.f x), Covers := ⋯, IsOpen := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : (AlgebraicGeometry.Scheme.OpenCover.pushforwardIso 𝒰 f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : 𝒰.J), (AlgebraicGeometry.Scheme.OpenCover.pushforwardIso 𝒰 f).map x = CategoryTheory.CategoryStruct.comp (𝒰.map x) f

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : 𝒰.J), (AlgebraicGeometry.Scheme.OpenCover.pushforwardIso 𝒰 f).obj x = 𝒰.obj x

def AlgebraicGeometry.Scheme.OpenCover.pushforwardIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.OpenCover Y

The pushforward of an open cover along an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_J {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] : (AlgebraicGeometry.Scheme.OpenCover.add 𝒰 f).J = Option 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.add 𝒰 f).obj i = Option.rec Y 𝒰.obj i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_f {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace) : (AlgebraicGeometry.Scheme.OpenCover.add 𝒰 f).f x = some (𝒰.f x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.add 𝒰 f).map i = Option.rec f 𝒰.map i

def AlgebraicGeometry.Scheme.OpenCover.add {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.Scheme.OpenCover X

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

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.val_base_isIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.val.base

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.Scheme.basic_open_isOpenImmersion {R : CommRingCat} (f : ↑R) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))).op)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine (R : CommRingCat) : AlgebraicGeometry.Scheme.OpenCover (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R))

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

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.affineBasisCover (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.OpenCover X

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

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.affineBasisCoverRing (X : AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.Scheme.affineBasisCover X).J) : CommRingCat

The coordinate ring of a component in the affine_basis_cover.

Equations

• AlgebraicGeometry.Scheme.affineBasisCoverRing X i = CommRingCat.of (Localization.Away i.snd)

theorem AlgebraicGeometry.Scheme.affineBasisCover_obj (X : AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.Scheme.affineBasisCover X).J) : (AlgebraicGeometry.Scheme.affineBasisCover X).obj i = AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (AlgebraicGeometry.Scheme.affineBasisCoverRing X i))

theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) (r : ↑(Exists.choose ⋯)) : Set.range ⇑((AlgebraicGeometry.Scheme.affineBasisCover X).map { fst := x, snd := r }).val.base = ⇑((AlgebraicGeometry.Scheme.affineCover X).map x).val.base '' (PrimeSpectrum.basicOpen r).carrier

theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis (X : AlgebraicGeometry.Scheme) : TopologicalSpace.IsTopologicalBasis {x : Set ↑↑X.toPresheafedSpace | ∃ (a : (AlgebraicGeometry.Scheme.affineBasisCover X).J), x = Set.range ⇑((AlgebraicGeometry.Scheme.affineBasisCover X).map a).val.base}

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [H : CompactSpace ↑↑X.toPresheafedSpace] (x : { x : ↑↑X.toPresheafedSpace // x ∈ Exists.choose ⋯ }) : (AlgebraicGeometry.Scheme.OpenCover.finiteSubcover 𝒰).map x = 𝒰.map (𝒰.f ↑x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [H : CompactSpace ↑↑X.toPresheafedSpace] (x : { x : ↑↑X.toPresheafedSpace // x ∈ Exists.choose ⋯ }) : (AlgebraicGeometry.Scheme.OpenCover.finiteSubcover 𝒰).obj x = 𝒰.obj (𝒰.f ↑x)

def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [H : CompactSpace ↑↑X.toPresheafedSpace] : AlgebraicGeometry.Scheme.OpenCover X

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

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [H : CompactSpace ↑↑X.toPresheafedSpace] : Fintype (AlgebraicGeometry.Scheme.OpenCover.finiteSubcover 𝒰).J

Equations

• AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover 𝒰 = id inferInstance

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : AlgebraicGeometry.Scheme

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f).toLocallyRingedSpace = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y.toLocallyRingedSpace f

def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme 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

• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y.toLocallyRingedSpace f

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_val {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f).val = f

instance AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f)

Equations

• ⋯ = H

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace) : X = Y

theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f.val = X

theorem AlgebraicGeometry.Scheme.restrict_carrier {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : ↑(AlgebraicGeometry.Scheme.restrict X h).toPresheafedSpace = U

@[simp]

theorem AlgebraicGeometry.Scheme.restrict_presheaf_obj {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X✝.toPresheafedSpace} (h : OpenEmbedding ⇑f) (X : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (AlgebraicGeometry.Scheme.restrict X✝ h).presheaf.obj X = X✝.presheaf.obj (Opposite.op ((IsOpenMap.functor ⋯).obj X.unop))

@[simp]

theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : ∀ {X_1 Y : (TopologicalSpace.Opens ↑U)ᵒᵖ} (f_1 : X_1 ⟶ Y), (AlgebraicGeometry.Scheme.restrict X h).presheaf.map f_1 = X.presheaf.map ((IsOpenMap.functor ⋯).map f_1.unop).op

def AlgebraicGeometry.Scheme.restrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : AlgebraicGeometry.Scheme

The restriction of a Scheme along an open embedding.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : (AlgebraicGeometry.Scheme.restrict X h).toPresheafedSpace = AlgebraicGeometry.PresheafedSpace.restrict X.toPresheafedSpace h

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_val_base {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : (AlgebraicGeometry.Scheme.ofRestrict X h).val.base = f

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) (V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Scheme.ofRestrict X h).val.c.app V = X.presheaf.map ((IsOpenMap.adjunction ⋯).counit.app V.unop).op

def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : AlgebraicGeometry.Scheme.restrict X h ⟶ X

The canonical map from the restriction to the subspace.

Equations

• AlgebraicGeometry.Scheme.ofRestrict X h = AlgebraicGeometry.LocallyRingedSpace.ofRestrict X.toLocallyRingedSpace h

instance AlgebraicGeometry.IsOpenImmersion.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : OpenEmbedding ⇑f) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.ofRestrict X h)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.of_isIso {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [CategoryTheory.IsIso g] : AlgebraicGeometry.IsOpenImmersion g

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsOpenImmersion.to_iso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsOpenImmersion f] [CategoryTheory.Epi f.val.base] : CategoryTheory.IsIso f

theorem AlgebraicGeometry.IsOpenImmersion.of_stalk_iso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (hf : OpenEmbedding ⇑f.val.base) [∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)] : AlgebraicGeometry.IsOpenImmersion f

theorem AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsOpenImmersion f ↔ OpenEmbedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

theorem AlgebraicGeometry.isIso_iff_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ CategoryTheory.Epi f.val.base

theorem AlgebraicGeometry.isIso_iff_stalk_iso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

def AlgebraicGeometry.IsOpenImmersion.isoRestrict {X : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : X ≅ AlgebraicGeometry.Scheme.restrict Z ⋯

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

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsOpenImmersion.mono {X : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.forget_map_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inl) ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map CategoryTheory.Limits.WalkingCospan.Hom.inr))

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfLeft {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsOpenImmersion.forgetPreservesOfLeft {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsOpenImmersion.forgetPreservesOfRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

• AlgebraicGeometry.IsOpenImmersion.forgetPreservesOfRight f g = CategoryTheory.Limits.preservesPullbackSymmetry AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace f g

instance AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasPullback f g

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.HasPullback g f

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.pullback_snd_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.pullback_fst_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.fst

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.pullback_to_base {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsOpenImmersion.forgetToTopPreservesOfLeft {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToTop

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsOpenImmersion.forgetToTopPreservesOfRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToTop

Equations

• AlgebraicGeometry.IsOpenImmersion.forgetToTopPreservesOfRight f g = CategoryTheory.Limits.preservesPullbackSymmetry AlgebraicGeometry.Scheme.forgetToTop f g

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : Set.range ⇑CategoryTheory.Limits.pullback.snd.val.base = ((TopologicalSpace.Opens.map g.val.base).obj { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }).carrier

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : Set.range ⇑CategoryTheory.Limits.pullback.fst.val.base = ((TopologicalSpace.Opens.map g.val.base).obj { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }).carrier

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : Set.range ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f).val.base = Set.range ⇑f.val.base ∩ Set.range ⇑g.val.base

theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : Set.range ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g).val.base = Set.range ⇑g.val.base ∩ Set.range ⇑f.val.base

def AlgebraicGeometry.IsOpenImmersion.lift {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion 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

• AlgebraicGeometry.IsOpenImmersion.lift f g H' = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H'

theorem AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base) {Z : AlgebraicGeometry.Scheme} (h : Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.lift_fac {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H') f = g

theorem AlgebraicGeometry.IsOpenImmersion.lift_uniq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base) (l : Y ⟶ X) (hl : CategoryTheory.CategoryStruct.comp l f = g) : l = AlgebraicGeometry.IsOpenImmersion.lift f g H'

def AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.val.base = Set.range ⇑g.val.base) : X ≅ Y

Two open immersions with equal range are isomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.val.base = Set.range ⇑g.val.base) {Z : AlgebraicGeometry.Scheme} (h : Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.val.base = Set.range ⇑g.val.base) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom g = f

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.val.base = Set.range ⇑g.val.base) {Z : AlgebraicGeometry.Scheme} (h : Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.val.base = Set.range ⇑g.val.base) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv f = g

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.Hom.opensFunctor {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)

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

Equations

• AlgebraicGeometry.Scheme.Hom.opensFunctor f = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H

def AlgebraicGeometry.Scheme.Hom.invApp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X.presheaf.obj (Opposite.op U) ⟶ Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))

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

Equations

• AlgebraicGeometry.Scheme.Hom.invApp f U = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp H U

theorem AlgebraicGeometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : AlgebraicGeometry.IsOpenImmersion g] (V : TopologicalSpace.Opens ↑↑U.toPresheafedSpace) : (TopologicalSpace.Opens.map f.val.base).obj V = (TopologicalSpace.Opens.map fg.val.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V)

theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : AlgebraicGeometry.IsOpenImmersion g] (V : TopologicalSpace.Opens ↑↑U.toPresheafedSpace) : f.val.c.app (Opposite.op V) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.invApp g V) (CategoryTheory.CategoryStruct.comp (fg.val.c.app (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V))) (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op))

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

theorem AlgebraicGeometry.IsOpenImmersion.lift_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (H : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base) (V : TopologicalSpace.Opens ↑↑U.toPresheafedSpace) : (AlgebraicGeometry.IsOpenImmersion.lift f g H).val.c.app (Opposite.op V) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.invApp f V) (CategoryTheory.CategoryStruct.comp (g.val.c.app (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V))) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

theorem AlgebraicGeometry.Scheme.image_basicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (r : ↑(X.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (X.basicOpen r) = Y.basicOpen ((AlgebraicGeometry.Scheme.Hom.invApp f U) r)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRange_coe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : ↑(AlgebraicGeometry.Scheme.Hom.opensRange f) = Set.range ⇑f.val.base

def AlgebraicGeometry.Scheme.Hom.opensRange {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace

The image of an open immersion as an open set.

Equations

• AlgebraicGeometry.Scheme.Hom.opensRange f = { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).map x = CategoryTheory.Limits.pullback.fst

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_f {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).f x = 𝒰.f (f.val.base x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_J {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J = 𝒰.J

def AlgebraicGeometry.Scheme.OpenCover.pullbackCover {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) : AlgebraicGeometry.Scheme.OpenCover W

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_J {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover' 𝒰 f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_f {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover' 𝒰 f).f x = 𝒰.f (f.val.base x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_obj {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover' 𝒰 f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_map {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) (x : 𝒰.J) : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover' 𝒰 f).map x = CategoryTheory.Limits.pullback.snd

def AlgebraicGeometry.Scheme.OpenCover.pullbackCover' {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) {W : AlgebraicGeometry.Scheme} (f : W ⟶ X) : AlgebraicGeometry.Scheme.OpenCover W

Given an open cover on X, we may pull them back along a morphism f : W ⟶ X to obtain an open cover of W. This is similar to Scheme.OpenCover.pullbackCover, but here we take pullback (𝒰.map x) f instead of pullback f (𝒰.map x).

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : ⋃ (i : 𝒰.J), Set.range ⇑(𝒰.map i).val.base = Set.univ

theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : ⨆ (i : 𝒰.J), AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.map i) = ⊤

theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) [Finite 𝒰.J] [H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace] : CompactSpace ↑↑X.toPresheafedSpace

def AlgebraicGeometry.Scheme.OpenCover.inter {X : AlgebraicGeometry.Scheme} (𝒰₁ : AlgebraicGeometry.Scheme.OpenCover X) (𝒰₂ : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.Scheme.OpenCover X

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_J {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ⊤) : (AlgebraicGeometry.Scheme.openCoverOfSuprEqTop X U hU).J = s

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_map {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ⊤) (i : s) : (AlgebraicGeometry.Scheme.openCoverOfSuprEqTop X U hU).map i = AlgebraicGeometry.Scheme.ofRestrict X ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_obj {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ⊤) (i : s) : (AlgebraicGeometry.Scheme.openCoverOfSuprEqTop X U hU).obj i = AlgebraicGeometry.Scheme.restrict X ⋯

def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ⊤) : AlgebraicGeometry.Scheme.OpenCover X

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

Equations

• One or more equations did not get rendered due to their size.

structure AlgebraicGeometry.Scheme.AffineOpenCover (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) (v + 1))

An affine open cover of X consists of a family of open immersions into X from spectra of rings.

• J : Type v

  index set of an affine open cover of a scheme X

• obj : self.J → CommRingCat

  the ring associated to a component of an affine open cover

• map : (j : self.J) → AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (self.obj j)) ⟶ X

  the embedding of subschemes to X

• f : ↑↑X.toPresheafedSpace → self.J

  given a point of x : X, f x is the index of the subscheme which contains x

• Covers : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(self.map (self.f x)).val.base

  the subschemes covers X

• IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

  the embedding of subschemes are open immersions

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.AffineOpenCover X) : ∀ (a : ↑↑X.toPresheafedSpace), (AlgebraicGeometry.Scheme.AffineOpenCover.openCover 𝓤).f a = 𝓤.f a

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_obj {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.AffineOpenCover X) (j : 𝓤.J) : (AlgebraicGeometry.Scheme.AffineOpenCover.openCover 𝓤).obj j = AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (𝓤.obj j))

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_J {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.AffineOpenCover X) : (AlgebraicGeometry.Scheme.AffineOpenCover.openCover 𝓤).J = 𝓤.J

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_map {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.AffineOpenCover X) (j : 𝓤.J) : (AlgebraicGeometry.Scheme.AffineOpenCover.openCover 𝓤).map j = 𝓤.map j

def AlgebraicGeometry.Scheme.AffineOpenCover.openCover {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.AffineOpenCover X) : AlgebraicGeometry.Scheme.OpenCover X

The open cover associated to an affine open cover.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.affineOpenCover (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.AffineOpenCover X

A choice of an affine open cover of a scheme.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.AffineOpenCover.openCover (AlgebraicGeometry.Scheme.affineOpenCover X) = AlgebraicGeometry.Scheme.affineCover X

def AlgebraicGeometry.Scheme.OpenCover.affineRefinement {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.Scheme.AffineOpenCover X

Given any open cover 𝓤, this is an affine open cover which refines it. The morphism in the category of open covers which proves that this is indeed a refinement, see AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement.

Equations

• One or more equations did not get rendered due to their size.

structure AlgebraicGeometry.Scheme.OpenCover.Hom {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) (𝓥 : AlgebraicGeometry.Scheme.OpenCover X) : Type (max u v)

A morphism between open covers 𝓤 ⟶ 𝓥 indicates that 𝓤 is a refinement of 𝓥. Since open covers of schemes are indexed, the definition also involves a map on the indexing types.

• idx : 𝓤.J → 𝓥.J

  The map on indexing types associated to a morphism of open covers.

• app : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (self.idx j)

  The morphism between open subsets associated to a morphism of open covers.

• isOpen : ∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (self.app j)
• w : ∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.Hom.w_assoc {X : AlgebraicGeometry.Scheme} {𝓤 : AlgebraicGeometry.Scheme.OpenCover X} {𝓥 : AlgebraicGeometry.Scheme.OpenCover X} (self : AlgebraicGeometry.Scheme.OpenCover.Hom 𝓤 𝓥) (j : 𝓤.J) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app j) (CategoryTheory.CategoryStruct.comp (𝓥.map (self.idx j)) h) = CategoryTheory.CategoryStruct.comp (𝓤.map j) h

def AlgebraicGeometry.Scheme.OpenCover.Hom.id {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.Scheme.OpenCover.Hom 𝓤 𝓤

The identity morphism in the category of open covers of a scheme.

Equations

• AlgebraicGeometry.Scheme.OpenCover.Hom.id 𝓤 = { idx := fun (j : 𝓤.J) => j, app := fun (j : 𝓤.J) => CategoryTheory.CategoryStruct.id (𝓤.obj j), isOpen := ⋯, w := ⋯ }

def AlgebraicGeometry.Scheme.OpenCover.Hom.comp {X : AlgebraicGeometry.Scheme} {𝓤 : AlgebraicGeometry.Scheme.OpenCover X} {𝓥 : AlgebraicGeometry.Scheme.OpenCover X} {𝓦 : AlgebraicGeometry.Scheme.OpenCover X} (f : AlgebraicGeometry.Scheme.OpenCover.Hom 𝓤 𝓥) (g : AlgebraicGeometry.Scheme.OpenCover.Hom 𝓥 𝓦) : AlgebraicGeometry.Scheme.OpenCover.Hom 𝓤 𝓦

The composition of two morphisms in the category of open covers of a scheme.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.OpenCover.category {X : AlgebraicGeometry.Scheme} : CategoryTheory.Category.{max u v, max (v + 1) (u + 1)} (AlgebraicGeometry.Scheme.OpenCover X)

Equations

• AlgebraicGeometry.Scheme.OpenCover.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.id_idx_apply {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.id 𝓤).idx j = j

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.id_app {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.id 𝓤).app j = CategoryTheory.CategoryStruct.id (𝓤.obj j)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply {X : AlgebraicGeometry.Scheme} {𝓤 : AlgebraicGeometry.Scheme.OpenCover X} {𝓥 : AlgebraicGeometry.Scheme.OpenCover X} {𝓦 : AlgebraicGeometry.Scheme.OpenCover X} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.comp f g).idx j = g.idx (f.idx j)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.comp_app {X : AlgebraicGeometry.Scheme} {𝓤 : AlgebraicGeometry.Scheme.OpenCover X} {𝓥 : AlgebraicGeometry.Scheme.OpenCover X} {𝓦 : AlgebraicGeometry.Scheme.OpenCover X} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.comp f g).app j = CategoryTheory.CategoryStruct.comp (f.app j) (g.app (f.idx j))

def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement {X : AlgebraicGeometry.Scheme} (𝓤 : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.Scheme.AffineOpenCover.openCover (AlgebraicGeometry.Scheme.OpenCover.affineRefinement 𝓤) ⟶ 𝓤

Given any open cover 𝓤, this is an affine open cover which refines it.

Equations

• One or more equations did not get rendered due to their size.