The support of a local model is the zero set of its equations

The local analytic K-space (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}), 𝓘 = (f₁, …, f_k), has support S(𝓘) = supp (𝒜_G/𝓘) = {x ∈ G | f₁(x) = ⋯ = f_k(x) = 0} [Hir64, Ch. 0, §1]. The stalk 𝓘_x is generated by the germs of the f_i; in the local ring 𝒜_{G,x} an ideal generated by a set is the unit ideal iff the set contains a unit (Ideal.span_eq_top_iff_exists_isUnit); and a germ of 𝒜_{Kⁿ} is a unit iff its value is nonzero, read through Mathlib's identification of the stalk of the restricted sheaf 𝒜_G with the stalk of 𝒜_{Kⁿ} (restrictStalkIso). The point-set description mem_range_localModel_ι_iff is what identifies an open subspace of a local model with a local model (Hironaka/AnalyticSpace/LocalModelRestrict.lean).

theorem AnalyticSpace.isUnit_germ_affine_iff (K : Type) [RCLike K] (n : ℕ) (U : TopologicalSpace.Opens (Kn K n)) (x : ↥U) (g : AnalyticFun K n U) : IsUnit ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U ↑x ⋯)) g) ↔ g.eval x ≠ 0

A germ at x ∈ U of an analytic function on U ⊆ Kⁿ is a unit of 𝒜_{Kⁿ,x} iff its value at x is nonzero.

theorem AnalyticSpace.restrictStalkIso_germ_toGlobal (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (g : AnalyticFun K n G) : (CategoryTheory.ConcreteCategory.hom ((affine K n).restrictStalkIso ⋯ x).hom) ((CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ ⊤ x ⋯)) ((toGlobal K n G) g)) = (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑x ⋯)) g

The germ at x ∈ G of a global section of 𝒜_G corresponds, under the identification of the stalk of 𝒜_G with 𝒜_{Kⁿ,x}, to the germ of the analytic function it comes from.

theorem AnalyticSpace.isUnit_germ_toGlobal_iff (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (g : AnalyticFun K n G) : IsUnit ((CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ ⊤ x ⋯)) ((toGlobal K n G) g)) ↔ g.eval x ≠ 0

The germ at x ∈ G of a global section of 𝒜_G is a unit iff the value at x of the analytic function it comes from is nonzero.

theorem AnalyticSpace.mem_cosupport_modelIdeal_iff (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : x ∈ (modelIdeal K n G f).support ↔ ∀ (i : Fin k), (f i).eval x = 0

A point of G lies in the support S(𝓘) of the local model iff every equation f_i vanishes at it [Hir64, Ch. 0, §1].

theorem AnalyticSpace.mem_range_localModel_ι_iff (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (p : Kn K n) : p ∈ Set.range (KLocallyRingedSpace.Hom.toFun (localModel.ι K n G f)) ↔ ∃ (hp : p ∈ G), ∀ (i : Fin k), (f i).eval ⟨p, hp⟩ = 0

The support S(𝓘) of the local model, embedded in Kⁿ, is the common zero set {f₁ = ⋯ = f_k = 0} ⊆ G [Hir64, Ch. 0, §1].