Open immersions of schemes

@[reducible, inline]

abbrev AlgebraicGeometry.IsOpenImmersion {X 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 (AlgebraicGeometry.Scheme.Hom.toLRSHom f)

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

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

@[deprecated AlgebraicGeometry.IsOpenImmersion.isOpen_range]

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

Alias of AlgebraicGeometry.IsOpenImmersion.isOpen_range.

theorem AlgebraicGeometry.Scheme.Hom.isOpenEmbedding {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] : Topology.IsOpenEmbedding ⇑f.base

@[deprecated AlgebraicGeometry.Scheme.Hom.isOpenEmbedding]

theorem AlgebraicGeometry.Scheme.Hom.openEmbedding {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] : Topology.IsOpenEmbedding ⇑f.base

Alias of AlgebraicGeometry.Scheme.Hom.isOpenEmbedding.

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

The image of an open immersion as an open set.

Equations

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

@[simp]

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

@[reducible, inline]

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

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

Equations

• f.opensFunctor = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f.toLRSHom

def AlgebraicGeometry.«term_''ᵁ_» : Lean.TrailingParserDescr

f ''ᵁ U is notation for the image (as an open set) of U under an open immersion f.

Equations

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

def AlgebraicGeometry.«term_''ᵁ_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

theorem AlgebraicGeometry.Scheme.Hom.image_le_image_of_le {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V) : f.opensFunctor.obj U ≤ f.opensFunctor.obj V

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (e : U ≤ V) : f.opensFunctor.map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] : f.opensFunctor.obj ⊤ = f.opensRange

theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.CategoryStruct.comp f g) = (AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)

theorem AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.Hom.opensRange f = ⊤

theorem AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.CategoryStruct.comp f g) = AlgebraicGeometry.Scheme.Hom.opensRange g

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : (TopologicalSpace.Opens.map f.base).obj (f.opensFunctor.obj U) = U

theorem AlgebraicGeometry.Scheme.Hom.image_le_image_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U U' : X.Opens) : (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U ≤ (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U' ↔ U ≤ U'

theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U) = f.opensRange ⊓ U

theorem AlgebraicGeometry.Scheme.Hom.image_injective {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] : Function.Injective fun (x : X.Opens) => f.opensFunctor.obj x

theorem AlgebraicGeometry.Scheme.Hom.image_iSup {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {ι : Sort u_1} (s : ι → X.Opens) : f.opensFunctor.obj (⨆ (i : ι), s i) = ⨆ (i : ι), f.opensFunctor.obj (s i)

theorem AlgebraicGeometry.Scheme.Hom.image_iSup₂ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {ι : Sort u_1} {κ : ι → Sort u_2} (s : (i : ι) → κ i → X.Opens) : f.opensFunctor.obj (⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), f.opensFunctor.obj (s i j)

def AlgebraicGeometry.Scheme.Hom.appIso {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj U)) ≅ X.presheaf.obj (Opposite.op U)

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

Equations

• f.appIso U = (CategoryTheory.asIso (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f.toLRSHom U)).symm

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (f.appIso V).inv = CategoryTheory.CategoryStruct.comp (f.appIso U).inv (Y.presheaf.map (f.opensFunctor.op.map i))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (i : Opposite.op U ⟶ Opposite.op V) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (f.appIso V).inv h) = CategoryTheory.CategoryStruct.comp (f.appIso U).inv (CategoryTheory.CategoryStruct.comp (Y.presheaf.map (f.opensFunctor.op.map i)) h)

theorem AlgebraicGeometry.Scheme.Hom.appIso_hom {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : (f.appIso U).hom = CategoryTheory.CategoryStruct.comp (f.app (f.opensFunctor.obj U)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

theorem AlgebraicGeometry.Scheme.Hom.appIso_hom' {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : (f.appIso U).hom = f.appLE (f.opensFunctor.obj U) U ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.app U) (CategoryTheory.CategoryStruct.comp (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.app_invApp' {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ f.opensRange) : CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op

A variant of app_invApp that gives an eqToHom instead of homOfLE.

theorem AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (hU : U ≤ f.opensRange) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.app U) (CategoryTheory.CategoryStruct.comp (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : CategoryTheory.CategoryStruct.comp (f.appIso U).inv (f.app (f.opensFunctor.obj U)) = X.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj (f.opensFunctor.obj U))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.appIso U).inv (CategoryTheory.CategoryStruct.comp (f.app (f.opensFunctor.obj U)) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) (x : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (Opposite.op U))) : (f.app (f.opensFunctor.obj U)) ((f.appIso U).inv x) = (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) x

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply' {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) (x : ↑(X.presheaf.obj (Opposite.op U))) : (f.app (f.opensFunctor.obj U)).hom ((f.appIso U).inv.hom x) = (X.presheaf.map (CategoryTheory.eqToHom ⋯).op).hom x

elementwise generates the ConcreteCategory.instFunLike lemma, we want CommRingCat.Hom.hom.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) (AlgebraicGeometry.Scheme.Hom.appIso f V).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).inv h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.appIso f V).inv ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) x) = (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv (AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) V e) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) V e) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

def AlgebraicGeometry.IsOpenImmersion.opensEquiv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : X.Opens ≃ { U : Y.Opens // U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }

The open sets of an open subscheme corresponds to the open sets containing in the image.

Equations

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

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : { U : Y.Opens // U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }) : (AlgebraicGeometry.IsOpenImmersion.opensEquiv f).symm U = (TopologicalSpace.Opens.map f.base).obj ↑U

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) : ↑((AlgebraicGeometry.IsOpenImmersion.opensEquiv f) U) = (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U

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

instance AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap {R : Type u_1} [CommRing R] (f : R) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

theorem AlgebraicGeometry.IsOpenImmersion.of_isLocalization {R S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (f : R) [IsLocalization.Away f S] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))

theorem AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset {X : AlgebraicGeometry.Scheme} {x : ↑↑X.toPresheafedSpace} {U : X.Opens} (hxU : x ∈ U) : ∃ (R : CommRingCat) (f : AlgebraicGeometry.Spec R ⟶ X), AlgebraicGeometry.IsOpenImmersion f ∧ x ∈ Set.range ⇑f.base ∧ Set.range ⇑f.base ⊆ ↑U

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 = { toHom_1 := AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y.toLocallyRingedSpace f }

@[simp]

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

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

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

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

The restriction of a Scheme along an open embedding.

Equations

• X.restrict h = { toPresheafedSpace := X.restrict h, IsSheaf := ⋯, isLocalRing := ⋯, local_affine := ⋯ }

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

@[simp]

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

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

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

The canonical map from the restriction to the subspace.

Equations

• X.ofRestrict h = { toHom_1 := X.ofRestrict h }

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) : (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).base = f

theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) (V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) (V : X.Opens) : AlgebraicGeometry.Scheme.Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op

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

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_appLE {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) (V : X.Opens) (W : (X.restrict h).Opens) (e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V) : AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.ofRestrict_appIso {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) (U✝ : (X.restrict h).Opens) : AlgebraicGeometry.Scheme.Hom.appIso (X.ofRestrict h) U✝ = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (X.ofRestrict h)).obj U✝)))

@[simp]

theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑f) (V W : (TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace)ᵒᵖ) (i : V ⟶ W) : (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[instance 100]

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

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

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

instance AlgebraicGeometry.IsOpenImmersion.stalk_iso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)

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

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

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

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

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

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 Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Mono f

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

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

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

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

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

instance AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfLeft {X Y 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 Y 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.forget_preservesOfLeft {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

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

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

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

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

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

instance AlgebraicGeometry.IsOpenImmersion.pullback_to_base {X Y 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)

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

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

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

theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.snd f g) = (TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)

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

theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.fst g f) = (TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)

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

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

def AlgebraicGeometry.IsOpenImmersion.lift {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.base ⊆ Set.range ⇑f.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

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

@[simp]

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

theorem AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.base ⊆ Set.range ⇑f.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

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

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

Two open immersions with equal range are isomorphic.

Equations

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

@[simp]

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

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.base = Set.range ⇑g.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_inv_fac {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.base = Set.range ⇑g.base) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv f = g

theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f.base = Set.range ⇑g.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

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

theorem AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq {X Y U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : AlgebraicGeometry.IsOpenImmersion g] (V : U.Opens) : AlgebraicGeometry.Scheme.Hom.app f V = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso g V).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app fg ((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 Y U : AlgebraicGeometry.Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (H : Set.range ⇑g.base ⊆ Set.range ⇑f.base) (V : U.Opens) : AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.IsOpenImmersion.lift f g H) V = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ≅ Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U))

If f is an open immersion X ⟶ Y, the global sections of X are naturally isomorphic to the sections of Y over the image of f.

Equations

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

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_inv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv = AlgebraicGeometry.Scheme.Hom.appLE f (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv = AlgebraicGeometry.Scheme.Hom.app f U

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) h

theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.appLE f (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U) ((TopologicalSpace.Opens.map f.base).obj U) ⋯) ((Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) x) = (AlgebraicGeometry.Scheme.Hom.app f U) x

theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom ((AlgebraicGeometry.Scheme.Hom.app f U) x) = (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) x

noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIsoTop {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : X.presheaf.obj (Opposite.op ⊤) ≅ Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f))

Given an open immersion f : U ⟶ X, the isomorphism between global sections of U and the sections of X at the image of f.

Equations

• AlgebraicGeometry.IsOpenImmersion.ΓIsoTop f = (AlgebraicGeometry.Scheme.Hom.appIso f ⊤).symm ≪≫ CategoryTheory.Functor.mapIso Y.presheaf (CategoryTheory.eqToIso ⋯).op

instance AlgebraicGeometry.IsOpenImmersion.instLift {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g.base ⊆ Set.range ⇑f.base) [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.IsOpenImmersion.lift f g H')

instance AlgebraicGeometry.isOpenImmersion_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsOpenImmersion

instance AlgebraicGeometry.isOpenImmersion_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsOpenImmersion

instance AlgebraicGeometry.isOpenImmersion_isMultiplicative : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsOpenImmersion

instance AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsOpenImmersion

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