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

• (_ : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)) = (_ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g))

def AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme (X : AlgebraicGeometry.LocallyRingedSpace) (h : ∀ (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)), ∃ (R : CommRingCat) (f : AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.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

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

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

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_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)

@[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

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_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : PUnit.{v + 1} ), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).obj x = X

@[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}

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_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

@[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

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

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

@[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_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_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_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_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

• (_ : CategoryTheory.IsIso f.val.base) = (_ : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.forgetToTop.toPrefunctor.map f))

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

Equations

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

def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine (R : CommRingCat) : AlgebraicGeometry.Scheme.OpenCover (AlgebraicGeometry.Scheme.Spec.toPrefunctor.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.toPrefunctor.obj (Opposite.op (AlgebraicGeometry.Scheme.affineBasisCoverRing X i))

theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) (r : ↑(Exists.choose (_ : ∃ (R : CommRingCat), Nonempty (AlgebraicGeometry.LocallyRingedSpace.restrict X.toLocallyRingedSpace (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion (Exists.choose (_ : ∃ (U : TopologicalSpace.OpenNhds x) (R : CommRingCat), Nonempty (AlgebraicGeometry.LocallyRingedSpace.restrict X.toLocallyRingedSpace (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion U.obj)) ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.obj (Opposite.op R)))).obj)) ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.toPrefunctor.obj (Opposite.op R))))) : 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 (_ : ∃ (t : Finset ↑↑X.toPresheafedSpace), ⋃ x ∈ t, Set.range ⇑(𝒰.map (𝒰.f x)).val.base = ⊤) }) : (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 (_ : ∃ (t : Finset ↑↑X.toPresheafedSpace), ⋃ x ∈ t, Set.range ⇑(𝒰.map (𝒰.f x)).val.base = ⊤) }) : (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

• (_ : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f)) = 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).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace = U

@[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).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.toPrefunctor.map f_1 = X.presheaf.toPrefunctor.map ((IsOpenMap.functor (_ : IsOpenMap ⇑f)).toPrefunctor.map f_1.unop).op

@[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).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.toPrefunctor.obj X = X✝.presheaf.toPrefunctor.obj (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ⇑f)).toPrefunctor.obj X.unop))

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).toLocallyRingedSpace.toSheafedSpace.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.toPrefunctor.map ((IsOpenMap.adjunction (_ : IsOpenMap ⇑f)).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

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

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

Equations

• (_ : AlgebraicGeometry.IsOpenImmersion g) = (_ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g)

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 (_ : OpenEmbedding ⇑f.val.base)

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

• (_ : CategoryTheory.Mono f) = (_ : CategoryTheory.Mono f)

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.toPrefunctor.map f)

Equations

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

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

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

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).toPrefunctor.map CategoryTheory.Limits.WalkingCospan.Hom.inl) ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).toPrefunctor.map CategoryTheory.Limits.WalkingCospan.Hom.inr))

Equations

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

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

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

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).toPrefunctor.map CategoryTheory.Limits.WalkingCospan.Hom.inl) ((CategoryTheory.Functor.comp (CategoryTheory.Limits.cospan g f) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).toPrefunctor.map CategoryTheory.Limits.WalkingCospan.Hom.inr))

Equations

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

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

• (_ : CategoryTheory.Limits.HasPullback f g) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g))

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

• (_ : CategoryTheory.Limits.HasPullback g f) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan g f))

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

• (_ : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd) = (_ : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.snd)

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

• (_ : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.fst) = (_ : AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback.fst)

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

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

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).toPrefunctor.obj { carrier := Set.range ⇑f.val.base, is_open' := (_ : IsOpen (Set.range ⇑f.val.base)) }).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).toPrefunctor.obj { carrier := Set.range ⇑f.val.base, is_open' := (_ : IsOpen (Set.range ⇑f.val.base)) }).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.toPrefunctor.obj (Opposite.op U) ⟶ Y.presheaf.toPrefunctor.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).toPrefunctor.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).toPrefunctor.obj V = (TopologicalSpace.Opens.map fg.val.base).toPrefunctor.obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).toPrefunctor.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).toPrefunctor.obj V))) (Y.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map f.val.base).toPrefunctor.obj V = (TopologicalSpace.Opens.map fg.val.base).toPrefunctor.obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).toPrefunctor.obj V))).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).toPrefunctor.obj V))) (X.presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsOpenImmersion.lift f g H).val.base).toPrefunctor.obj V = (TopologicalSpace.Opens.map g.val.base).toPrefunctor.obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).toPrefunctor.obj V))).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.toPrefunctor.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.opensFunctor f).toPrefunctor.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' := (_ : IsOpen (Set.range ⇑f.val.base)) }

@[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 f (𝒰.map x)

@[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

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'_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'_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'_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

@[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

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_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 (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion (U i)))

@[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 (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion (U i)))

@[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

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.