Open subspaces of local models are local models

Hironaka defines an analytic K-space by asking that every point have a neighbourhood K-isomorphic to a local analytic K-space (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) [Hir64, Ch. 0, §1]. Hironaka/AnalyticSpace/Defs.lean states that clause up to an open of the model — X|U ≅ (S(𝓘), …)|W for an open W of the model — because that form makes open subspaces analytic by a formal argument. The two forms define the same class of spaces provided an open subspace of a local model is again a local model: for an open W ⊆ S(𝓘) there is an open G' ⊆ G with W = S(𝓘) ∩ G' and (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)})|W ≅ (S(𝓘'), (𝒜_{G'}/𝓘')|_{S(𝓘')}), 𝓘' = (f₁|_{G'}, …, f_k|_{G'}). Hironaka uses this implicitly; it is proved here as localModel_restrictOpen_iso.

The argument. An open W of the support S(𝓘) is the trace of an open O of G (exists_opens_eq_preimage), and an open O of G is the trace of an open G' ≤ G of Kⁿ (exists_opens_le_eq_trace). Restriction to O commutes with the quotient (restrictOpen_quotient_iso of Hironaka/AnalyticSpace/QuotientMap.lean), so (S(𝓘), …)|W ≅ ((G, 𝒜_G)|O) / (𝓘|O). The open subspace (G, 𝒜_G)|O and (G', 𝒜_{G'}) are two open immersions into (Kⁿ, 𝒜) with the same image G', hence K-isomorphic (traceIso, isoOfRangeEq), and the quotient is transported along that isomorphism (quotient_kIso). What remains is to identify the transported ideal sheaf with 𝓘' = (f₁|_{G'}, …) (transportIdeal_restrictIdeal_modelIdeal). Every stalk of a model ideal is the image, under the stalk map of the open immersion into (Kⁿ, 𝒜), of the ideal (germ f₁, …, germ f_k) of the ambient stalk 𝒜_{Kⁿ,p} (ambientIdeal, stalkIdeal_modelIdeal_eq_map; the germ of f as a global section of 𝒜_G is the image of its ambient germ, stalkMap_ofRestrict_germ, by restrictStalkIso_germ_toGlobal), and pulling back along a K-morphism φ into (G, 𝒜_G) composes those stalk maps (stalkIdeal_comap_modelIdeal). Since the inclusion (G', 𝒜_{G'}) ⟶ (G, 𝒜_G) through the trace, followed by the open immersion of G, is the open immersion of G' (traceIncl_comp_ofRestrict), the pulled-back stalk is the image of the ambient ideal under the stalk map of (G', 𝒜_{G'}) ⟶ (Kⁿ, 𝒜), and the ambient ideals of f and of f|_{G'} agree because germs are insensitive to restriction (germ_res_apply). The point-set clause W = S(𝓘) ∩ G' reads both sides as {p ∈ G' | f₁(p) = ⋯ = f_k(p) = 0} through mem_range_localModel_ι_iff and mem_cosupport_modelIdeal_iff (range_restrict_localModel_ι).

The route through the ambient stalk avoids comparing stalk isomorphisms at two spellings of the same point of Kⁿ: the morphism identity traceIncl ≫ ofRestrict G = ofRestrict G' is rewritten in a statement about the composite morphism as a whole.

theorem AnalyticSpace.exists_opens_le_eq_trace (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : ∃ G' ≤ G, ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G'

An open of (G, 𝒜_G) is the trace of an open G₁ ≤ G of Kⁿ.

theorem AnalyticSpace.range_ofRestrict_ofRestrict_eq (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((analyticSpaceOfOpen K n G).ofRestrict O) ((affine K n).ofRestrict G))) = Set.range (KLocallyRingedSpace.Hom.toFun ((affine K n).ofRestrict G'))

The open immersion (G, 𝒜_G)|O ⟶ (Kⁿ, 𝒜) and the open immersion of (G', 𝒜_{G'}) have the same image G'.

noncomputable def AnalyticSpace.traceIso (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') : (analyticSpaceOfOpen K n G).restrictOpen O ≅ analyticSpaceOfOpen K n G'

The K-isomorphism (G, 𝒜_G)|O ≅ (G', 𝒜_{G'}) for an open O of G with trace G'.

Equations

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

noncomputable def AnalyticSpace.traceIncl (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') : analyticSpaceOfOpen K n G' ⟶ analyticSpaceOfOpen K n G

The inclusion (G', 𝒜_{G'}) ⟶ (G, 𝒜_G) through the trace.

Equations

• AnalyticSpace.traceIncl K n G hG O hO = CategoryTheory.CategoryStruct.comp (AnalyticSpace.traceIso K n G hG O hO).inv ((AnalyticSpace.analyticSpaceOfOpen K n G).ofRestrict O)

theorem AnalyticSpace.traceIncl_comp_ofRestrict (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') : CategoryTheory.CategoryStruct.comp (traceIncl K n G hG O hO) ((affine K n).ofRestrict G) = (affine K n).ofRestrict G'

theorem AnalyticSpace.traceIncl_base_apply (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') (p : ↑↑(analyticSpaceOfOpen K n G').toPresheafedSpace) : ↑((CategoryTheory.ConcreteCategory.hom (↑(traceIncl K n G hG O hO)).base) p) = ↑p

noncomputable def AnalyticSpace.ambientIdeal (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (x : Kn K n) : Ideal ↑((affine K n).presheaf.stalk x)

The ideal generated by the germs of the f_i at a point of Kⁿ, read in the stalk of 𝒜_{Kⁿ} (the unit ideal off G).

Equations

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

theorem AnalyticSpace.ambientIdeal_of_mem (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) {x : Kn K n} (h : x ∈ G) : ambientIdeal K n G f x = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G x h)) (f i))

theorem AnalyticSpace.stalkMap_ofRestrict_germ (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (q : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (g : AnalyticFun K n G) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑((affine K n).ofRestrict G)) q)) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑q ⋯)) g) = (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ ⊤ q ⋯)) ((toGlobal K n G) g)

The stalk map of (G, 𝒜_G) ⟶ (Kⁿ, 𝒜) carries the ambient germ of g to the germ of g as a global section of 𝒜_G.

theorem AnalyticSpace.stalkIdeal_modelIdeal_eq_map (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (q : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) q = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑((affine K n).ofRestrict G)) q)) (ambientIdeal K n G f ↑q)

The stalk ideal of a local model is the image of the ambient ideal.

theorem AnalyticSpace.stalkIdeal_comap_modelIdeal (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) {Y : KLocallyRingedSpace K} (φ : Y ⟶ analyticSpaceOfOpen K n G) (p : ↑↑Y.toPresheafedSpace) : (QuotientSpace.comap (↑φ) (modelIdeal K n G f)).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(CategoryTheory.CategoryStruct.comp φ ((affine K n).ofRestrict G))) p)) (ambientIdeal K n G f ((CategoryTheory.ConcreteCategory.hom (↑(CategoryTheory.CategoryStruct.comp φ ((affine K n).ofRestrict G))).base) p))

The pull-back of the model ideal along a K-morphism into (G, 𝒜_G), through the composite with the open immersion into (Kⁿ, 𝒜).

theorem AnalyticSpace.transportIdeal_restrictIdeal_modelIdeal (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') {k : ℕ} (f : Fin k → AnalyticFun K n G) : KLocallyRingedSpace.transportIdeal (traceIso K n G hG O hO).symm ((analyticSpaceOfOpen K n G).restrictIdeal (modelIdeal K n G f) O) = modelIdeal K n G' fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.map (CategoryTheory.homOfLE hG).op)) (f i)

The ideal sheaf of a local model, restricted to O and transported along the trace isomorphism, is the ideal sheaf of the restricted equations: 𝓘|_{G'} = (f₁|_{G'}, …, f_k|_{G'}).

theorem AnalyticSpace.range_restrict_localModel_ι (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' ≤ G) (O : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : ∀ (p : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace), p ∈ O ↔ ↑p ∈ G') {k : ℕ} (f : Fin k → AnalyticFun K n G) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((localModel K n G f).ofRestrict ((analyticSpaceOfOpen K n G).quotientOpens (modelIdeal K n G f) O)) (localModel.ι K n G f))) = Set.range (KLocallyRingedSpace.Hom.toFun (localModel.ι K n G' fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.map (CategoryTheory.homOfLE hG).op)) (f i)))

The point set of the open subspace of the model over O, and that of the restricted model, agree in Kⁿ: both are {p ∈ G' | f₁(p) = ⋯ = f_k(p) = 0}.

theorem AnalyticSpace.localModel_restrictOpen_iso (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace) : ∃ (G' : TopologicalSpace.Opens (Kn K n)) (h : G' ≤ G), Nonempty (((localModel K n G f).restrictOpen W).KIso (localModel K n G' fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.map (CategoryTheory.homOfLE h).op)) (f i))) ∧ Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((localModel K n G f).ofRestrict W) (localModel.ι K n G f))) = Set.range (KLocallyRingedSpace.Hom.toFun (localModel.ι K n G' fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.map (CategoryTheory.homOfLE h).op)) (f i)))

An open subspace W of the local analytic K-space (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) is K-isomorphic to the local analytic K-space of the restricted equations on an open G' ≤ G, with the same point set in Kⁿ [Hir64, Ch. 0, §1].