The space of a manifold restricted to an open subset

The open subspace Sp(M) | U of the K-local-ringed space of a manifold M is the space of the open submanifold U. The inclusion U → M is an analytic map whose K-morphism ofManifoldHom Subtype.val is an open immersion (isOpenImmersion_ofManifoldHom_val): the base map is the open embedding of U, and on sections the restriction 𝒪_M(V) → 𝒪_U(V ∩ U) is a bijection, an analytic function on an open V ⊆ U being an analytic function on the open V of M. Two open immersions with the same range are K-isomorphic over their common target (isoOfRangeEq), which gives ofManifold_restrictOpen_iso : Sp(M) | U ≅ Sp(U), an isomorphism over Sp(M) (ofManifold_restrictOpen_iso_hom_comp). This is the analytic analogue of Mathlib's ChartedSpace.restrictLocallyRingedSpaceIso for smooth manifolds, stated for K-local-ringed spaces.

The isomorphism is used throughout the comparison of manifolds with their spaces: the chart isomorphisms (Hironaka.AnalyticSpace.Manifold.Chart, Hironaka.AnalyticSpace.ChartLift), the stratum isomorphisms (Hironaka.AnalyticSpace.Manifold.Stratum, Hironaka.AnalyticSpace.Manifold.StratumIso, Hironaka.AnalyticSpace.HomExtNonSingular), morphisms into an open subset of Kⁿ (Hironaka.AnalyticSpace.HomOfSectionsAffine), and the restriction of local resolutions to the pieces of a cover (Hironaka.Resolution.Analytic.Kol07Thm45.PieceRestrict).

theorem AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq_hom_comp {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)) : CategoryTheory.CategoryStruct.comp (isoOfRangeEq a b h).hom b = a

The isomorphism of two open immersions with the same range is over the target.

instance AnalyticSpace.KLocallyRingedSpace.isOpenImmersion_ofManifoldHom_val {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(ofManifoldHom Subtype.val ⋯)

The K-morphism of the inclusion of an open submanifold is an open immersion: an analytic function on an open V ⊆ U is an analytic function on the open V of M, so the restriction of sections is bijective (the analytic analogue of Mathlib's instance for ChartedSpace.locallyRingedSpaceMap Subtype.val).

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifold_restrictOpen_iso {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) : ((ofManifold K E M).restrictOpen U).KIso (ofManifold K E ↥U)

Sp(M) | U ≅ Sp(U) for an open U ⊆ M (the analytic analogue of Mathlib's ChartedSpace.restrictLocallyRingedSpaceIso, as K-local-ringed spaces).

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.ofManifold_restrictOpen_iso_hom_comp {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) : CategoryTheory.CategoryStruct.comp (ofManifold_restrictOpen_iso U).hom (ofManifoldHom Subtype.val ⋯) = (ofManifold K E M).ofRestrict U

The isomorphism Sp(M) | U ≅ Sp(U) is over Sp(M): composed with Sp(U → M) it is the open immersion Sp(M) | U ⟶ Sp(M).