Basic lemmas on K-morphisms and analytic K-spaces

Consequences of the definitions of K-local-ringed spaces, their morphisms and analytic K-spaces: the K-linearity of the restriction and stalk maps of a K-morphism (the constants are carried to the constants because a K-morphism commutes with the structural homomorphisms on global sections, and the constants over U, or at x, are the restrictions, or the germs, of the global constants); a K-morphism whose underlying morphism of locally ringed spaces is an isomorphism is a K-isomorphism, so that IsIso in An/K can be tested on the underlying morphism; and the existence of a local Kⁿ-coordination at every point [Hir64, Ch. 0, §1, p. 120].

theorem AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ_eq {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) : pullbackΓ f = CommRingCat.Hom.hom ((↑f).c.app (Opposite.op ⊤))

The global-section map of a K-morphism is the ⊤-component of its sheaf map.

theorem AnalyticSpace.KLocallyRingedSpace.Hom.algebraMap_res {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (c : K) : (CommRingCat.Hom.hom ((↑f).c.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (Y.algebraMap c)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (X.algebraMap c)

A K-morphism carries the constants over U to the constants over f⁻¹U.

theorem AnalyticSpace.KLocallyRingedSpace.Hom.algebraMap_stalk {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) (c : K) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑f) x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ ⊤ ((CategoryTheory.ConcreteCategory.hom (↑f).base) x) trivial)) (Y.algebraMap c)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) (X.algebraMap c)

The stalk map of a K-morphism carries the constant germs to the constant germs.

theorem AnalyticSpace.KLocallyRingedSpace.isIso_of_isIso_val {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) [CategoryTheory.IsIso ↑f] : CategoryTheory.IsIso f

A K-morphism whose underlying morphism of locally ringed spaces is an isomorphism is an isomorphism of K-local-ringed spaces (the inverse commutes with the K-structures automatically).

theorem AnalyticSpace.KLocallyRingedSpace.isIso_iff_isIso_val {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso ↑f

theorem AnalyticSpace.isIso_iff {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso ↑f

f is an isomorphism of An/K iff its underlying morphism of locally ringed spaces is an isomorphism.

theorem AnalyticSpace.exists_localCoordination {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : Nonempty (X.LocalCoordination x)

Every point has a local Kⁿ-coordination [Hir64, Ch. 0, §1, p. 120].