Local isomorphisms of K-local-ringed spaces on points and stalks

If the restriction φ|U : X|U → Y|V of a K-morphism φ : X → Y is a K-isomorphism, then φ is injective on U, maps open subsets of U to open subsets of Y, and has bijective stalk maps at the points of U. Also the hom equations of the double-restriction isomorphism (X|U)|V ≅ X|(imageOpens U V) (restrictOpen_restrictOpen_iso). Routine.

theorem AnalyticSpace.KLocallyRingedSpace.KIso.homeomorph_apply {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) : e.homeomorph a = Hom.toFun e.hom a

theorem AnalyticSpace.KLocallyRingedSpace.imageOpens_le {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) : imageOpens U V ≤ U

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpen_restrictOpen_iso_inv_comp {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (restrictOpen_restrictOpen_iso U V).inv (CategoryTheory.CategoryStruct.comp ((X.restrictOpen U).ofRestrict V) (X.ofRestrict U)) = X.ofRestrict (imageOpens U V)

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpen_restrictOpen_iso_inv_comp_assoc {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) {Z : KLocallyRingedSpace K} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictOpen_restrictOpen_iso U V).inv (CategoryTheory.CategoryStruct.comp ((X.restrictOpen U).ofRestrict V) (CategoryTheory.CategoryStruct.comp (X.ofRestrict U) h)) = CategoryTheory.CategoryStruct.comp (X.ofRestrict (imageOpens U V)) h

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictToHomeomorph {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hUV : ∀ u ∈ U, Hom.toFun φ u ∈ V) [CategoryTheory.IsIso (Hom.restrictTo φ U V hUV)] : ↑↑(A.restrictOpen U).toPresheafedSpace ≃ₜ ↑↑(B.restrictOpen V).toPresheafedSpace

The homeomorphism U ≃ₜ V underlying the local isomorphism.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.restrictToHomeomorph_apply_val {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hUV : ∀ u ∈ U, Hom.toFun φ u ∈ V) [CategoryTheory.IsIso (Hom.restrictTo φ U V hUV)] (u : ↑↑(A.restrictOpen U).toPresheafedSpace) : ↑((restrictToHomeomorph φ U V hUV) u) = Hom.toFun φ ↑u

theorem AnalyticSpace.KLocallyRingedSpace.injOn_toFun_of_isIso_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hUV : ∀ u ∈ U, Hom.toFun φ u ∈ V) [CategoryTheory.IsIso (Hom.restrictTo φ U V hUV)] : Set.InjOn (Hom.toFun φ) ↑U

A local isomorphism is injective on U.

theorem AnalyticSpace.KLocallyRingedSpace.isOpen_image_of_isIso_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hUV : ∀ u ∈ U, Hom.toFun φ u ∈ V) [CategoryTheory.IsIso (Hom.restrictTo φ U V hUV)] {S : Set ↑↑A.toPresheafedSpace} (hS : IsOpen S) : IsOpen (Hom.toFun φ '' (S ∩ ↑U))

A local isomorphism maps open subsets of U to open subsets of B.

theorem AnalyticSpace.KLocallyRingedSpace.bijective_stalkMap_of_isIso_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (φ : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hUV : ∀ u ∈ U, Hom.toFun φ u ∈ V) [CategoryTheory.IsIso (Hom.restrictTo φ U V hUV)] (u : ↑↑A.toPresheafedSpace) (hu : u ∈ U) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑φ) u))

A local isomorphism has bijective stalk maps at the points of U.