`K`-local-ringed spaces: basic properties #

The elementary theory of K-local-ringed spaces and their K-morphisms.

A K-morphism pulls the constants back to the constants (Hom.pullbackΓ, Hom.pullbackΓ_algebraMap), and the germ of the pullback of a global section is the stalk map on its germ (germ_top_pullbackΓ).
The underlying morphism of locally ringed spaces and the underlying map of identities, composites and factorizations (Hom.id_val, Hom.comp_val, Hom.ofFac_val, Hom.toFun_id, Hom.toFun_comp, Hom.range_toFun_comp), which is continuous (Hom.continuous_toFun); the range of the open immersion X | U ⟶ X is U (range_toFun_ofRestrict).
A K-isomorphism is an isomorphism of locally ringed spaces (KIso.isIso_hom_val) and a homeomorphism (KIso.homeomorph).
Two open immersions of K-local-ringed spaces with the same range are K-isomorphic (isoOfRangeEq, by Mathlib's IsOpenImmersion.lift and its uniqueness), and the range of an open immersion is open (isOpen_range_toFun).
The K-morphisms of analytic maps are functorial (ofManifoldHom_id, ofManifoldHom_comp, both by rfl) and have the analytic map as underlying map (toFun_ofManifoldHom).

def AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) :

↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op Y.toLocallyRingedSpace)) →+* ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X.toLocallyRingedSpace))

The pullback of a global section along a K-morphism, Γ(Y, 𝒪_Y) →+* Γ(X, 𝒪_X).

Equations

AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ f = CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Γ.map (↑f).op)

Instances For

source

theorem AnalyticSpace.KLocallyRingedSpace.Hom.pullbackΓ_algebraMap {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) (c : K) :

(pullbackΓ f) (Y.algebraMap c) = X.algebraMap c

A K-morphism pulls the constants of Y back to the constants of X.

source

theorem AnalyticSpace.KLocallyRingedSpace.germ_top_pullbackΓ {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (l : A ⟶ B) (τ : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op B.toLocallyRingedSpace))) (x : ↑↑A.toPresheafedSpace) :

(CategoryTheory.ConcreteCategory.hom (A.presheaf.germ ⊤ x trivial)) ((Hom.pullbackΓ l) τ) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑l) x)) ((CategoryTheory.ConcreteCategory.hom (B.presheaf.germ ⊤ ((CategoryTheory.ConcreteCategory.hom (↑l).base) x) trivial)) τ)

The germ at x of the pullback of a global section is the stalk map on its germ.

source

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.ofFac_val {K : Type} [RCLike K] {A B X : KLocallyRingedSpace K} (a : A ⟶ X) (b : B ⟶ X) (l : A.toLocallyRingedSpace ⟶ B.toLocallyRingedSpace) (hl : CategoryTheory.CategoryStruct.comp l ↑b = ↑a) :

↑(ofFac a b l hl) = l

source

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.comp_val {K : Type} [RCLike K] {X Y Z : KLocallyRingedSpace K} (f : X ⟶ Y) (g : Y ⟶ Z) :

↑(CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ↑f ↑g

The morphism of locally ringed spaces underlying a composite of K-morphisms is the composite.

source

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.id_val {K : Type} [RCLike K] (X : KLocallyRingedSpace K) :

↑(CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.toLocallyRingedSpace

The morphism of locally ringed spaces underlying the identity K-morphism is the identity.

source

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.toFun_comp {K : Type} [RCLike K] {X Y Z : KLocallyRingedSpace K} (f : X ⟶ Y) (g : Y ⟶ Z) :

toFun (CategoryTheory.CategoryStruct.comp f g) = toFun g ∘ toFun f

The underlying map of a composite is the composite of the underlying maps.

source

theorem AnalyticSpace.KLocallyRingedSpace.Hom.toFun_id {K : Type} [RCLike K] (X : KLocallyRingedSpace K) :

toFun (CategoryTheory.CategoryStruct.id X) = id

The underlying map of the identity is the identity.

source

theorem AnalyticSpace.KLocallyRingedSpace.Hom.range_toFun_comp {K : Type} [RCLike K] {X Y Z : KLocallyRingedSpace K} (f : X ⟶ Y) (g : Y ⟶ Z) :

Set.range (toFun (CategoryTheory.CategoryStruct.comp f g)) = toFun g '' Set.range (toFun f)

The range of a composite is the image under the second map of the range of the first.

source

theorem AnalyticSpace.KLocallyRingedSpace.Hom.continuous_toFun {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) :

Continuous (toFun f)

The underlying map of a K-morphism is continuous.

source

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.range_toFun_ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) :

Set.range (Hom.toFun (X.ofRestrict U)) = ↑U

The range of the open immersion X | U ⟶ X is U.

source

instance AnalyticSpace.KLocallyRingedSpace.KIso.isIso_hom_val {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) :

CategoryTheory.IsIso ↑e.hom

The underlying morphism of locally ringed spaces of a K-isomorphism is an isomorphism.

source

noncomputable def AnalyticSpace.KLocallyRingedSpace.KIso.homeomorph {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) :

↑↑A.toPresheafedSpace ≃ₜ ↑↑B.toPresheafedSpace

The homeomorphism underlying a K-isomorphism.

Equations

e.homeomorph = TopCat.homeoOfIso (AlgebraicGeometry.LocallyRingedSpace.forgetToTop.mapIso (CategoryTheory.asIso ↑e.hom))

Instances For

source

noncomputable def AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq {K : Type} [RCLike K] {A B X : KLocallyRingedSpace K} (a : A ⟶ X) (b : B ⟶ X) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑a] [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑b] (h : Set.range (Hom.toFun a) = Set.range (Hom.toFun b)) :

A ≅ B

Two open immersions of K-local-ringed spaces with the same range are K-isomorphic (the K-version of Mathlib's IsOpenImmersion.isoOfRangeEq, by the universal property of open immersions).

Equations