Stalk maps of K-isomorphisms, open immersions and restricted morphisms

General lemmas on the stalk maps of morphisms of K-local-ringed spaces: the stalk maps of a K-isomorphism are bijective; those of the open immersion X | U ⟶ X are bijective (KLocallyRingedSpace.isIso_ofRestrict_stalkMap); and those of the restricted morphism g | U : A | U ⟶ B | U' (Hom.restrictTo) are isomorphisms, respectively bijective, at the points where those of g are. They serve the restriction of a complexification to an open subspace and the gluing of local complexifications (Hironaka/AnalyticSpace/Glue/Restrict.lean, Hironaka/AnalyticSpace/Glue/Trivial.lean) and the local isomorphism theory (Hironaka/AnalyticSpace/LocalIso.lean, Hironaka/AnalyticSpace/IsoOverOpen.lean).

Conventions. Bijectivity is stated for the underlying ring homomorphism (stalkMap a).hom (the form of Complexification.bijective_stalkMap); isomorphy in the category of commutative rings is the equivalent IsIso (Mathlib's ConcreteCategory.isIso_iff_bijective). The stalk map of g | U is conjugate to that of g by the stalk isomorphisms of the two open immersions, through Hom.restrictTo_comp_ofRestrict. For U = ⊤ the open immersion is an isomorphism and the lemmas reduce to the statement for g. Routine; not in the sources.

theorem AnalyticSpace.bijective_hom_comp {R S T : CommRingCat} {φ : R ⟶ S} {ψ : S ⟶ T} (hφ : Function.Bijective ⇑(CommRingCat.Hom.hom φ)) (hψ : Function.Bijective ⇑(CommRingCat.Hom.hom ψ)) : Function.Bijective ⇑(CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp φ ψ))

Bijectivity of a composite of ring-category morphisms from that of the factors.

theorem AnalyticSpace.KLocallyRingedSpace.KIso.bijective_stalkMap {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑e.hom) a))

The stalk maps of a K-isomorphism are bijective.

theorem AnalyticSpace.KLocallyRingedSpace.bijective_stalkMap_ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(X.ofRestrict U)) x))

The stalk maps of the open immersion X | U ⟶ X are bijective.

theorem AnalyticSpace.KLocallyRingedSpace.isIso_stalkMap_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, Hom.toFun g a ∈ U') (a : ↑↑(A.restrictOpen U).toPresheafedSpace) (hg : CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) ((CategoryTheory.ConcreteCategory.hom (↑(A.ofRestrict U)).base) a))) : CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(Hom.restrictTo g U U' h)) a)

The stalk maps of g | U : A | U ⟶ B | U' are isomorphisms where those of g are.

theorem AnalyticSpace.KLocallyRingedSpace.bijective_stalkMap_restrictTo {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (h : ∀ a ∈ U, Hom.toFun g a ∈ U') (a : ↑↑(A.restrictOpen U).toPresheafedSpace) (hg : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑g) ((CategoryTheory.ConcreteCategory.hom (↑(A.ofRestrict U)).base) a)))) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(Hom.restrictTo g U U' h)) a))

The stalk maps of g | U : A | U ⟶ B | U' are bijective where those of g are.