The local model near a simple point is a manifold

Hironaka's "by means of jacobian criterion and the implicit function theorem" [Hir64, Ch. 0, §1, p. 121]: at a point z of the local model X = V(f) ⊆ G ⊆ Kⁿ with the chart data of Hironaka/AnalyticSpace/ModelChart.lean (an adapted chart e with (f) = (e_σ) near z), the open X|V over the good neighbourhood W is K-isomorphic to the open G' ⊆ K^{n−c}, G' = {v | ι_σ v ∈ e.target, e⁻¹(ι_σ v) ∈ W} with ι_σ = embedCompl σ the coordinate subspace (exists_kIso_analyticSpaceOfOpen_of_span_germ_eq). This file builds the underlying homeomorphism G' ≃ₜ V (v ↦ e⁻¹(ι_σ v), inverse w ↦ π_σ(e w)), the evaluation of the fibres 𝒜_{G,y}/𝓘_y → K of the quotient sheaf (well defined because 𝓘_y ⊆ 𝔪_y) through which the K-morphism (G', 𝒜_{G'}) → X|V acts on sections, and proves it a K-isomorphism: its stalk maps are surjective (a germ on G' pulls back along π_σ ∘ e) and injective (a surjection between regular local rings of the same dimension n − c is an isomorphism). Used by Hironaka/AnalyticSpace/Jacobian.lean and Hironaka/AnalyticSpace/RegEval.lean.

The opens V ⊆ X and G' ⊆ K^{n−c} and the homeomorphism between them

noncomputable def AnalyticSpace.ModelChartData.V {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace

The open V ∋ z of the local model lying over the good neighbourhood W.

Equations

• D.V = (TopologicalSpace.Opens.map (↑(AnalyticSpace.localModel.ι K n G f)).base).obj D.W

theorem AnalyticSpace.ModelChartData.mem_V {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {w : ↑↑(localModel K n G f).toPresheafedSpace} : w ∈ D.V ↔ ↑↑w ∈ D.W

theorem AnalyticSpace.ModelChartData.z_mem_V {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : z ∈ D.V

noncomputable def AnalyticSpace.ModelChartData.Θ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : Kn K (n - c)) : Kn K n

The map K^{n−c} → Kⁿ, v ↦ e⁻¹(ι_σ v) (junk outside e.target).

Equations

• D.Θ v = ↑D.e.symm { down := Manifold.embedCompl D.σ v.down }

theorem AnalyticSpace.ModelChartData.continuous_embed {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : Continuous fun (v : Kn K (n - c)) => { down := Manifold.embedCompl D.σ v.down }

The coordinate-subspace inclusion ι_σ : K^{n−c} → Kⁿ, continuous.

def AnalyticSpace.ModelChartData.G' {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : TopologicalSpace.Opens (Kn K (n - c))

The open G' ⊆ K^{n−c}: the points v with ι_σ v ∈ e.target and e⁻¹(ι_σ v) ∈ W.

Equations

• D.G' = { carrier := (fun (v : AnalyticSpace.Kn K (n - c)) => { down := Manifold.embedCompl D.σ v.down }) ⁻¹' (D.e.target ∩ ↑D.e.symm ⁻¹' ↑D.W), is_open' := ⋯ }

theorem AnalyticSpace.ModelChartData.mem_G' {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} : v ∈ D.G' ↔ { down := Manifold.embedCompl D.σ v.down } ∈ D.e.target ∧ D.Θ v ∈ D.W

theorem AnalyticSpace.ModelChartData.Θ_mem_W {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : D.Θ v ∈ D.W

theorem AnalyticSpace.ModelChartData.Θ_mem_G {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : D.Θ v ∈ G

theorem AnalyticSpace.ModelChartData.e_Θ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : ↑D.e (D.Θ v) = { down := Manifold.embedCompl D.σ v.down }

theorem AnalyticSpace.ModelChartData.Θ_mem_cosupport {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : ⟨D.Θ v, ⋯⟩ ∈ (modelIdeal K n G f).support

noncomputable def AnalyticSpace.ModelChartData.Ψ₀ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : ↥D.V

The underlying map G' → V, v ↦ e⁻¹(ι_σ v).

Equations

• D.Ψ₀ v = ⟨⟨⟨D.Θ ↑v, ⋯⟩, ⋯⟩, ⋯⟩

theorem AnalyticSpace.ModelChartData.Ψ₀_val {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : ↑↑↑(D.Ψ₀ v) = D.Θ ↑v

theorem AnalyticSpace.ModelChartData.mem_source_of_mem_V {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : ↑↑↑w ∈ D.e.source

theorem AnalyticSpace.ModelChartData.coord_eq_zero_of_mem_V {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) (i : Fin c) : (↑D.e ↑↑↑w).down (D.σ i) = 0

theorem AnalyticSpace.ModelChartData.embed_projCompl_e {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : { down := Manifold.embedCompl D.σ (Manifold.projCompl D.σ (↑D.e ↑↑↑w).down) } = ↑D.e ↑↑↑w

noncomputable def AnalyticSpace.ModelChartData.Ψ₀inv {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : ↥D.G'

The inverse map V → G', w ↦ π_σ(e w).

Equations

• D.Ψ₀inv w = ⟨{ down := Manifold.projCompl D.σ (↑D.e ↑↑↑w).down }, ⋯⟩

theorem AnalyticSpace.ModelChartData.Ψ₀inv_Ψ₀ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : D.Ψ₀inv (D.Ψ₀ v) = v

theorem AnalyticSpace.ModelChartData.Ψ₀_Ψ₀inv {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : D.Ψ₀ (D.Ψ₀inv w) = w

theorem AnalyticSpace.ModelChartData.continuous_Θ_restrict {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : Continuous fun (v : ↥D.G') => D.Θ ↑v

theorem AnalyticSpace.ModelChartData.isInducing_val {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : Topology.IsInducing fun (w : ↥D.V) => ↑↑↑w

The inclusion V → Kⁿ, w ↦ w, is inducing (three subtype layers).

theorem AnalyticSpace.ModelChartData.continuous_Ψ₀ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : Continuous D.Ψ₀

theorem AnalyticSpace.ModelChartData.continuous_Ψ₀inv {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : Continuous D.Ψ₀inv

noncomputable def AnalyticSpace.ModelChartData.homeo {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ↥D.G' ≃ₜ ↥D.V

The homeomorphism G' ≃ₜ V of Hironaka's implicit-function-theorem step.

Equations

• D.homeo = { toFun := D.Ψ₀, invFun := D.Ψ₀inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Evaluation of the fibres of the quotient sheaf

noncomputable def AnalyticSpace.evalRestrict {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) (y : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : ↑((analyticSpaceOfOpen K n G).presheaf.stalk y) →+* K

The stalk 𝒜_{G,y} of (G, 𝒜_G) read in 𝒜_{Kⁿ,y} and evaluated at y.

Equations

• AnalyticSpace.evalRestrict G y = (Manifold.eval K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n) ↑y).comp (CommRingCat.Hom.hom ((AnalyticSpace.affine K n).restrictStalkIso ⋯ y).hom)

theorem AnalyticSpace.evalRestrict_germ_toGlobal {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) (y : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) (g : AnalyticFun K n G) : (evalRestrict G y) ((CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ ⊤ y ⋯)) ((toGlobal K n G) g)) = g.eval y

theorem AnalyticSpace.evalRestrict_germ {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) (y : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) {W : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace} (hy : y ∈ W) (a : ↑((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op W))) : (evalRestrict G y) ((CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ W y hy)) a) = Manifold.extendSection K (Kn K n) a ↑y

evalRestrict of the germ of a section a of 𝒜_G over W ∋ y is the value a y.

theorem AnalyticSpace.stalkIdeal_le_ker_evalRestrict {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (w : ↑↑(localModel K n G f).toPresheafedSpace) : (modelIdeal K n G f).stalkIdeal ↑w ≤ RingHom.ker (evalRestrict G ↑w)

The germs of the generators f j evaluate to 0 at a point of the support.

noncomputable def AnalyticSpace.evalFiber {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (w : ↑↑(localModel K n G f).toPresheafedSpace) : QuotientSpace.fiber (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) w →+* K

Evaluation of the fibre 𝒜_{G,y}/𝓘_y of the quotient sheaf at a point y of the support: the value at y, well defined because 𝓘_y ⊆ 𝔪_y.

Equations

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

theorem AnalyticSpace.evalFiber_mk {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (w : ↑↑(localModel K n G f).toPresheafedSpace) (a : ↑((analyticSpaceOfOpen K n G).presheaf.stalk ↑w)) : (evalFiber G f w) ((Ideal.Quotient.mk (QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) ↑w)) a) = (evalRestrict G ↑w) a

The sheaf component: evaluation of germ families along Ψ₀

theorem AnalyticSpace.ModelChartData.contMDiff_embed {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ContMDiff (modelWithCornersSelf K (Kn K (n - c))) (modelWithCornersSelf K (Kn K n)) ⊤ fun (v : Kn K (n - c)) => { down := Manifold.embedCompl D.σ v.down }

The coordinate embedding ι_σ : K^{n−c} → Kⁿ is analytic.

theorem AnalyticSpace.ModelChartData.contMDiffOn_Θ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ContMDiffOn (modelWithCornersSelf K (Kn K (n - c))) (modelWithCornersSelf K (Kn K n)) ⊤ D.Θ ↑D.G'

Θ = e⁻¹ ∘ ι_σ is analytic on G'.

theorem AnalyticSpace.ModelChartData.mem_functor_obj_iff {X : TopCat} (U : TopologicalSpace.Opens ↑X) (Ω : TopologicalSpace.Opens ↑((TopologicalSpace.Opens.toTopCat X).obj U)) (x : ↑X) : x ∈ ⋯.functor.obj Ω ↔ ∃ (hx : x ∈ U), ⟨x, hx⟩ ∈ Ω

Membership in the image of an open of the subtype U under the inclusion.

noncomputable def AnalyticSpace.ModelChartData.Ψtop {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : (analyticSpaceOfOpen K (n - c) D.G').toTopCat ⟶ ((localModel K n G f).restrictOpen D.V).toTopCat

The underlying continuous map G' → V as a morphism of TopCat.

Equations

• D.Ψtop = TopCat.ofHom { toFun := D.Ψ₀, continuous_toFun := ⋯ }

theorem AnalyticSpace.ModelChartData.Ψtop_apply {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : (CategoryTheory.ConcreteCategory.hom D.Ψtop) v = D.Ψ₀ v

noncomputable def AnalyticSpace.ModelChartData.pullOpens {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) : TopologicalSpace.Opens (Kn K (n - c))

The open Ω'' ⊆ K^{n−c} under an open Ω of V: the image in K^{n−c} of Ψ₀⁻¹ Ω ⊆ G'.

Equations

• D.pullOpens Ω = ⋯.functor.obj ((TopologicalSpace.Opens.map D.Ψtop).obj Ω)

theorem AnalyticSpace.ModelChartData.mem_pullOpens {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} {v : Kn K (n - c)} : v ∈ D.pullOpens Ω ↔ ∃ (hv : v ∈ D.G'), D.Ψ₀ ⟨v, hv⟩ ∈ Ω

theorem AnalyticSpace.ModelChartData.mem_G'_of_mem_pullOpens {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} {v : Kn K (n - c)} (h : v ∈ D.pullOpens Ω) : v ∈ D.G'

theorem AnalyticSpace.ModelChartData.Ψ₀_mem_of_mem_pullOpens {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} {v : Kn K (n - c)} (h : v ∈ D.pullOpens Ω) : D.Ψ₀ ⟨v, ⋯⟩ ∈ Ω

noncomputable def AnalyticSpace.ModelChartData.ptOf {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} {v : Kn K (n - c)} (h : v ∈ D.pullOpens Ω) : ↥(⋯.functor.obj Ω)

The point of the open ι_V(Ω) ⊆ S under v ∈ Ω''.

Equations

• D.ptOf h = ⟨↑(D.Ψ₀ ⟨v, ⋯⟩), ⋯⟩

noncomputable def AnalyticSpace.ModelChartData.Fsec {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) (v : Kn K (n - c)) : K

The function on K^{n−c} obtained by evaluating a germ family s over Ω ⊆ V along Ψ₀ (and 0 outside Ω'').

Equations

• D.Fsec Ω s v = if h : v ∈ D.pullOpens Ω then (AnalyticSpace.evalFiber G f ↑(D.ptOf h)) (↑s (D.ptOf h)) else 0

theorem AnalyticSpace.ModelChartData.Fsec_of_mem {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) {v : Kn K (n - c)} (h : v ∈ D.pullOpens Ω) : D.Fsec Ω s v = (evalFiber G f ↑(D.ptOf h)) (↑s (D.ptOf h))

noncomputable def AnalyticSpace.ModelChartData.pullOpensS {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (T : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace) : TopologicalSpace.Opens (Kn K (n - c))

The open of K^{n−c} under an open T ⊆ S of the local model: the points v ∈ G' with Ψ₀ v ∈ T.

Equations

• D.pullOpensS T = ⋯.functor.obj ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp D.Ψtop D.V.inclusion')).obj T)

theorem AnalyticSpace.ModelChartData.mem_pullOpensS {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {T : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} {v : Kn K (n - c)} : v ∈ D.pullOpensS T ↔ ∃ (hv : v ∈ D.G'), ↑(D.Ψ₀ ⟨v, hv⟩) ∈ T

theorem AnalyticSpace.ModelChartData.Fsec_eq_extendSection_Θ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) {v : Kn K (n - c)} (h : v ∈ D.pullOpens Ω) {W₁ : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace} {a : ↑((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op W₁))} (hW : ↑↑(D.ptOf h) ∈ W₁) (hs : ↑s (D.ptOf h) = (Ideal.Quotient.mk (QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) ↑↑(D.ptOf h))) ((CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ W₁ (↑↑(D.ptOf h)) hW)) a)) : D.Fsec Ω s v = Manifold.extendSection K (Kn K n) a (D.Θ v)

The local formula: where the germ family s is the class of a section a of 𝒜_G, the evaluated function is a ∘ Θ.

theorem AnalyticSpace.ModelChartData.contMDiffOn_Fsec {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : ContMDiffOn (modelWithCornersSelf K (Kn K (n - c))) (modelWithCornersSelf K K) ⊤ (D.Fsec Ω s) ↑(D.pullOpens Ω)

The evaluated function F s is analytic on Ω'': near each point it is a ∘ Θ for a section a representing s, and Θ is analytic on G'.

noncomputable def AnalyticSpace.ModelChartData.secOf {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : ContMDiffMap (modelWithCornersSelf K (Kn K (n - c))) (modelWithCornersSelf K K) (↥(D.pullOpens Ω)) K ⊤

The section of 𝒜_{K^{n−c}} over Ω'' obtained from a germ family s over Ω.

Equations

• D.secOf Ω s = Manifold.sectionOfContMDiffOn (D.Fsec Ω s) (D.pullOpens Ω) ⋯

theorem AnalyticSpace.ModelChartData.secOf_apply {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) (v : ↥(D.pullOpens Ω)) : (D.secOf Ω s) v = (evalFiber G f ↑(D.ptOf ⋯)) (↑s (D.ptOf ⋯))

theorem AnalyticSpace.ModelChartData.secOf_one {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) : D.secOf Ω 1 = 1

theorem AnalyticSpace.ModelChartData.secOf_zero {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) : D.secOf Ω 0 = 0

theorem AnalyticSpace.ModelChartData.secOf_mul {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s t : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : D.secOf Ω (s * t) = D.secOf Ω s * D.secOf Ω t

theorem AnalyticSpace.ModelChartData.secOf_add {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s t : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : D.secOf Ω (s + t) = D.secOf Ω s + D.secOf Ω t

theorem AnalyticSpace.ModelChartData.pullOpens_mono {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₁ Ω₂ : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} (h : Ω₁ ≤ Ω₂) : D.pullOpens Ω₁ ≤ D.pullOpens Ω₂

theorem AnalyticSpace.ModelChartData.secOf_res {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₁ Ω₂ : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace} (h : Ω₁ ≤ Ω₂) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω₂))) : D.secOf Ω₁ ((CategoryTheory.ConcreteCategory.hom (((localModel K n G f).restrictOpen D.V).presheaf.map (CategoryTheory.homOfLE h).op)) s) = (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf K (Kn K (n - c)) (Kn K (n - c))).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (D.secOf Ω₂ s)

Compatibility with restriction.

noncomputable def AnalyticSpace.ModelChartData.secRingHom {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω)) →+* ↑(((TopCat.Presheaf.pushforward CommRingCat D.Ψtop).obj (analyticSpaceOfOpen K (n - c) D.G').presheaf).obj (Opposite.op Ω))

The component of the sheaf map at Ω: evaluation of germ families along Ψ₀, a ring homomorphism 𝒪_{X|V}(Ω) →+* 𝒜_{K^{n−c}}(Ω'').

Equations

• D.secRingHom Ω = { toFun := D.secOf Ω, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AnalyticSpace.ModelChartData.ΨcApp {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) : ((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω) ⟶ ((TopCat.Presheaf.pushforward CommRingCat D.Ψtop).obj (analyticSpaceOfOpen K (n - c) D.G').presheaf).obj (Opposite.op Ω)

The component at Ω as a morphism of CommRingCat.

Equations

• D.ΨcApp Ω = CommRingCat.ofHom (D.secRingHom Ω)

theorem AnalyticSpace.ModelChartData.ΨcApp_apply {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : (CategoryTheory.ConcreteCategory.hom (D.ΨcApp Ω)) s = D.secOf Ω s

noncomputable def AnalyticSpace.ModelChartData.Ψc {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ((localModel K n G f).restrictOpen D.V).presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat D.Ψtop).obj (analyticSpaceOfOpen K (n - c) D.G').presheaf

The sheaf component 𝒪_{X|V} ⟶ Ψ₀_* 𝒜_{G'}.

Equations

• D.Ψc = { app := fun (Ω : (TopologicalSpace.Opens ↑↑((AnalyticSpace.localModel K n G f).restrictOpen D.V).toPresheafedSpace)ᵒᵖ) => D.ΨcApp (Opposite.unop Ω), naturality := ⋯ }

The morphism of presheafed spaces and its stalk maps

noncomputable def AnalyticSpace.ModelChartData.ΨHom {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : (analyticSpaceOfOpen K (n - c) D.G').toPresheafedSpace ⟶ ((localModel K n G f).restrictOpen D.V).toPresheafedSpace

The morphism of presheafed spaces (G', 𝒜_{G'}) → X|V: Ψ₀ on points, evaluation of germ families along Ψ₀ on sections.

Equations

• D.ΨHom = { base := D.Ψtop, c := D.Ψc }

theorem AnalyticSpace.ModelChartData.ΨHom_base_apply {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : (CategoryTheory.ConcreteCategory.hom D.ΨHom.base) v = D.Ψ₀ v

theorem AnalyticSpace.ModelChartData.ΨHom_stalkMap_germ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace) (v : ↥D.G') (hv : D.Ψ₀ v ∈ Ω) (s : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op Ω))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v)) ((CategoryTheory.ConcreteCategory.hom (((localModel K n G f).restrictOpen D.V).presheaf.germ Ω (D.Ψ₀ v) hv)) s) = (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K (n - c) D.G').presheaf.germ ((TopologicalSpace.Opens.map D.Ψtop).obj Ω) v hv)) ((CategoryTheory.ConcreteCategory.hom (D.ΨcApp Ω)) s)

The stalk map of ΨHom on the germ of a section s: the germ of the evaluated section.

The stalks of X|V are regular of dimension n − c

theorem WithBot.eq_natCast_sub_of_add_natCast_eq {d : WithBot ℕ∞} {c n : ℕ} (h : d + ↑c = ↑n) : d = ↑(n - c)

d + c = n in WithBot ℕ∞ forces d = n − c.

theorem AnalyticSpace.ModelChartData.germ_hs_mem_maximalIdeal {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) (i : Fin c) : (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ D.U ↑↑↑w ⋯)) (D.hs i) ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk ↑↑↑w)

The germs of the hs i at a point of V lie in the maximal ideal (the hs vanish on the support).

theorem AnalyticSpace.ModelChartData.linearIndependent_dlin_germ_hs {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : LinearIndependent K fun (i : Fin c) => (dlin K n ↑↑↑w) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ D.U ↑↑↑w ⋯)) (D.hs i))

The germs of the hs i at a point of V have independent differentials.

theorem AnalyticSpace.ModelChartData.map_restrictStalkIso_stalkIdeal {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} (y : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : Ideal.map ((affine K n).restrictStalkIso ⋯ y).commRingCatIsoToRingEquiv ((modelIdeal K n G f).stalkIdeal y) = Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑y ⋯)) (f j))

The stalk ideal 𝓘_y of the local model, transported to 𝒜_{Kⁿ,y} along restrictStalkIso, is the ideal generated by the germs of the f j.

noncomputable def AnalyticSpace.ModelChartData.stalkEquivQuotient {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : ↑((localModel K n G f).presheaf.stalk ↑w) ≃+* ↑((affine K n).presheaf.stalk ↑↑↑w) ⧸ Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ D.U ↑↑↑w ⋯)) (D.hs i))

The stalk of the local model at a point w of V, read in 𝒜_{Kⁿ,w}: 𝒪_{X,w} ≅ 𝒜_{Kⁿ,w}/(hs).

Equations

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

theorem AnalyticSpace.ModelChartData.isRegularLocalRing_stalk_restrict {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (w : ↥D.V) : IsRegularLocalRing ↑(((localModel K n G f).restrictOpen D.V).presheaf.stalk w) ∧ ringKrullDim ↑(((localModel K n G f).restrictOpen D.V).presheaf.stalk w) = ↑(n - c)

The algebraic heart of Hironaka's statement [Hir64, Ch. 0, §1, p. 121]: the stalks of X|V are regular local rings of dimension n − c.

Injectivity of the stalk maps: the dimension argument

theorem AnalyticSpace.ModelChartData.stalkMap_injective_of_surjective {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') (hsurj : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v))) : Function.Injective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v))

A surjective stalk map of ΨHom is injective: its source 𝒪_{X|V, Ψ₀ v} is a regular local domain of dimension n − c (isRegularLocalRing_stalk_restrict), its target 𝒜_{K^{n−c}, v} has the same dimension, and a proper ideal of a Noetherian local domain with a quotient of full dimension is zero (Ideal.eq_bot_of_ringKrullDim_quotient_eq, Hironaka/Algebra/Local/QuotientParameters.lean).

Surjectivity of the stalk maps: pulling germs back along π_σ ∘ e

noncomputable def AnalyticSpace.ModelChartData.π {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (y : Kn K n) : Kn K (n - c)

The projection π : Kⁿ → K^{n−c}, y ↦ π_σ(e y) (junk outside e.source).

Equations

• D.π y = { down := Manifold.projCompl D.σ (↑D.e y).down }

theorem AnalyticSpace.ModelChartData.contMDiff_proj {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ContMDiff (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K (Kn K (n - c))) ⊤ fun (y : Kn K n) => { down := Manifold.projCompl D.σ y.down }

theorem AnalyticSpace.ModelChartData.contMDiffOn_π {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ContMDiffOn (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K (Kn K (n - c))) ⊤ D.π D.e.source

π = π_σ ∘ e is analytic on e.source.

theorem AnalyticSpace.ModelChartData.π_Θ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : D.π (D.Θ v) = v

theorem AnalyticSpace.ModelChartData.Θ_mem_source {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {v : Kn K (n - c)} (hv : v ∈ D.G') : D.Θ v ∈ D.e.source

def AnalyticSpace.ModelChartData.pullOpen {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') : TopologicalSpace.Opens (Kn K n)

The open Wg ⊆ Kⁿ on which the pullback g ∘ π of a section g of 𝒜_{G'} over Ω₀ is analytic: e.source ∩ π⁻¹(Ω₀).

Equations

• D.pullOpen Ω₀ = { carrier := D.e.source ∩ D.π ⁻¹' Subtype.val '' ↑Ω₀, is_open' := ⋯ }

theorem AnalyticSpace.ModelChartData.mem_pullOpen {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} {y : Kn K n} : y ∈ D.pullOpen Ω₀ ↔ y ∈ D.e.source ∧ ∃ (hy : D.π y ∈ D.G'), ⟨D.π y, hy⟩ ∈ Ω₀

theorem AnalyticSpace.ModelChartData.mem_source_of_mem_pullOpen {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} {y : Kn K n} (hy : y ∈ D.pullOpen Ω₀) : y ∈ D.e.source

theorem AnalyticSpace.ModelChartData.π_mem_of_mem_pullOpen {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} {y : Kn K n} (hy : y ∈ D.pullOpen Ω₀) : D.π y ∈ ⋯.functor.obj Ω₀

theorem AnalyticSpace.ModelChartData.Θ_mem_pullOpen {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} (v : ↥D.G') (hv : v ∈ Ω₀) : D.Θ ↑v ∈ D.pullOpen Ω₀

noncomputable def AnalyticSpace.ModelChartData.pullSection {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') (g : ↑((analyticSpaceOfOpen K (n - c) D.G').presheaf.obj (Opposite.op Ω₀))) : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.obj (Opposite.op (D.pullOpen Ω₀)))

The pullback g ∘ π as a section of 𝒜_{Kⁿ} over pullOpen Ω₀.

Equations

• D.pullSection Ω₀ g = Manifold.sectionOfContMDiffOn (Manifold.extendSection K (AnalyticSpace.Kn K (n - c)) g ∘ D.π) (D.pullOpen Ω₀) ⋯

noncomputable def AnalyticSpace.ModelChartData.pullOpenG {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') : TopologicalSpace.Opens ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace

The trace of pullOpen Ω₀ on G.

Equations

• D.pullOpenG Ω₀ = (TopologicalSpace.Opens.map G.inclusion').obj (D.pullOpen Ω₀)

theorem AnalyticSpace.ModelChartData.functor_pullOpenG_le {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') : ⋯.functor.obj (D.pullOpenG Ω₀) ≤ D.pullOpen Ω₀

noncomputable def AnalyticSpace.ModelChartData.pullSectionG {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') (g : ↑((analyticSpaceOfOpen K (n - c) D.G').presheaf.obj (Opposite.op Ω₀))) : ↑((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op (D.pullOpenG Ω₀)))

The pullback as a section of 𝒜_G.

Equations

• D.pullSectionG Ω₀ g = (CategoryTheory.ConcreteCategory.hom ((AnalyticSpace.affine K n).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (D.pullSection Ω₀ g)

noncomputable def AnalyticSpace.ModelChartData.pullFamily {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') (g : ↑((analyticSpaceOfOpen K (n - c) D.G').presheaf.obj (Opposite.op Ω₀))) : ↑((localModel K n G f).presheaf.obj (Opposite.op (QuotientSpace.preimage (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) (D.pullOpenG Ω₀))))

The germ family of the pullback on the support.

Equations

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

noncomputable def AnalyticSpace.ModelChartData.pullOpenV {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') : TopologicalSpace.Opens ↑↑((localModel K n G f).restrictOpen D.V).toPresheafedSpace

The open of V over pullOpen Ω₀.

Equations

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

theorem AnalyticSpace.ModelChartData.mem_pullOpenV {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} {w : ↥D.V} : w ∈ D.pullOpenV Ω₀ ↔ ↑↑↑w ∈ D.pullOpen Ω₀

theorem AnalyticSpace.ModelChartData.functor_pullOpenV_le {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') : ⋯.functor.obj (D.pullOpenV Ω₀) ≤ QuotientSpace.preimage (analyticSpaceOfOpen K n G).toLocallyRingedSpace (modelIdeal K n G f) (D.pullOpenG Ω₀)

noncomputable def AnalyticSpace.ModelChartData.pullFamilyV {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') (g : ↑((analyticSpaceOfOpen K (n - c) D.G').presheaf.obj (Opposite.op Ω₀))) : ↑(((localModel K n G f).restrictOpen D.V).presheaf.obj (Opposite.op (D.pullOpenV Ω₀)))

The pullback germ family as a section of X|V over pullOpenV Ω₀.

Equations

• D.pullFamilyV Ω₀ g = (CategoryTheory.ConcreteCategory.hom ((AnalyticSpace.localModel K n G f).presheaf.map (CategoryTheory.homOfLE ⋯).op)) (D.pullFamily Ω₀ g)

theorem AnalyticSpace.ModelChartData.mem_pullOpens_pullOpenV {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {Ω₀ : TopologicalSpace.Opens ↥D.G'} {v' : Kn K (n - c)} (h : v' ∈ D.pullOpens (D.pullOpenV Ω₀)) : ↑↑↑(D.ptOf h) ∈ D.pullOpen Ω₀

theorem AnalyticSpace.ModelChartData.secOf_pullFamilyV_apply {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (Ω₀ : TopologicalSpace.Opens ↥D.G') (g : ↑((analyticSpaceOfOpen K (n - c) D.G').presheaf.obj (Opposite.op Ω₀))) (v' : ↥(D.pullOpens (D.pullOpenV Ω₀))) : (D.secOf (D.pullOpenV Ω₀) (D.pullFamilyV Ω₀ g)) v' = Manifold.extendSection K (Kn K (n - c)) g ↑v'

The evaluated pull-back family is the section g itself: (g ∘ π) ∘ Θ = g.

theorem AnalyticSpace.ModelChartData.stalkMap_surjective {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v))

Surjectivity of the stalk maps: every germ g at v ∈ G' is the image of the germ family of g ∘ π.

The K-isomorphism

theorem AnalyticSpace.ModelChartData.stalkMap_bijective {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v))

theorem AnalyticSpace.ModelChartData.isLocalHom_stalkMap {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) (v : ↥D.G') : IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap D.ΨHom v))

noncomputable def AnalyticSpace.ModelChartData.ΨLRS {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : (analyticSpaceOfOpen K (n - c) D.G').toLocallyRingedSpace ⟶ ((localModel K n G f).restrictOpen D.V).toLocallyRingedSpace

The morphism of locally ringed spaces (G', 𝒜_{G'}) ⟶ X|V.

Equations

• D.ΨLRS = { toHom := D.ΨHom, prop := ⋯ }

theorem AnalyticSpace.ModelChartData.ΨLRS_algebraMap {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Γ.map D.ΨLRS.op)).comp ((localModel K n G f).restrictOpen D.V).algebraMap = (analyticSpaceOfOpen K (n - c) D.G').algebraMap

Ψ carries the constants to the constants: it is a K-morphism.

noncomputable def AnalyticSpace.ModelChartData.Ψ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : analyticSpaceOfOpen K (n - c) D.G' ⟶ (localModel K n G f).restrictOpen D.V

The K-morphism (G', 𝒜_{G'}) ⟶ X|V.

Equations

• D.Ψ = ⟨D.ΨLRS, ⋯⟩

theorem AnalyticSpace.ModelChartData.isIso_Ψ {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : CategoryTheory.IsIso D.Ψ

noncomputable def AnalyticSpace.ModelChartData.kIso {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) : ((localModel K n G f).restrictOpen D.V).KIso (analyticSpaceOfOpen K (n - c) D.G')

The K-isomorphism X|V ≅ (G', 𝒜_{G'}) [Hir64, Ch. 0, §1, p. 121].

Equations

• D.kIso = (CategoryTheory.asIso D.Ψ).symm

theorem AnalyticSpace.exists_kIso_analyticSpaceOfOpen_of_span_germ_eq {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) {c : ℕ} (h : Fin c → ↑((affine K n).presheaf.stalk ↑↑z)) (hgen : Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f i)) = Ideal.span (Set.range h)) (hind : LinearIndependent K fun (i : Fin c) => (dlin K n ↑↑z) (h i)) : ∃ (V : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace) (_ : z ∈ V) (G' : TopologicalSpace.Opens (Kn K (n - c))), Nonempty (((localModel K n G f).restrictOpen V).KIso (analyticSpaceOfOpen K (n - c) G'))

The implicit function theorem for a local model [Hir64, Ch. 0, §1, p. 121]: if at a point z of the local model X = V(f₁, …, f_k) ⊆ G ⊆ Kⁿ the ideal 𝓘_z = (f₁, …, f_k)_z of 𝒜_{Kⁿ,z} is generated by c germs h₁, …, h_c with linearly independent differentials at z, then a neighbourhood X|V of z is K-isomorphic to (G', 𝒜_{G'}) for an open G' ⊆ Kⁿ⁻ᶜ.