Documentation

Hironaka.AnalyticSpace.RegEval

Evaluation at a simple point of an analytic K-space #

At a simple point x of an analytic K-space X (a regular stalk), Hironaka/AnalyticSpace/RegPoints.lean provides a K-isomorphism e : (G', ๐’œ_{G'}) โ‰… X | V of a neighbourhood with an open of K^d [Hir64, Ch. 0, ยง1, p. 121]. Reading the stalk ๐’ช_{X,x} through it, ๐’ช_{X,x} โ‰… ๐’œ_{K^d, q}, and evaluating at q gives a local ring homomorphism ๐’ช_{X,x} โ†’+* K fixing the constants (chartEval). Such a homomorphism is unique (ringHom_eq_of_isLocalHom_of_const: for r, r โˆ’ (f r) is a non-unit, hence so is its image under any other local g, forcing g r = f r), so the evaluation regEval is canonical โ€” it does not depend on the chart โ€” and can be computed through any chart (chartEval_eq_regEval); the evaluation of the germ of a section is the value of its chart pullback (regEval_germ). That the residue field of a simple point is K is read off a local coordination; the inference is the library's. Routine; used by Hironaka/AnalyticSpace/Manifold/Stratum.lean.

source
theorem AnalyticSpace.ringHom_eq_of_isLocalHom_of_const {K : Type} [RCLike K] {R : Type u_1} [CommRing R] (c : K โ†’+* R) (f g : R โ†’+* K) [IsLocalHom g] (hf : โˆ€ (a : K), f (c a) = a) (hg : โˆ€ (a : K), g (c a) = a) :
f = g

A ring homomorphism f and a local ring homomorphism g from a ring R to the field K that agree on the constants c : K โ†’+* R are equal โ€” f kills r โˆ’ c (f r), which is therefore a non-unit, so g sends it to a non-unit of K, that is to 0.

source
theorem AnalyticSpace.KLocallyRingedSpace.KIso.inv_base_hom_base {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : โ†‘โ†‘A.toPresheafedSpace) :
(CategoryTheory.ConcreteCategory.hom (โ†‘e.inv).base) ((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) a) = a
source
theorem AnalyticSpace.KLocallyRingedSpace.KIso.hom_base_inv_base {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (b : โ†‘โ†‘B.toPresheafedSpace) :
(CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) ((CategoryTheory.ConcreteCategory.hom (โ†‘e.inv).base) b) = b
source
noncomputable def AnalyticSpace.chartEval {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) :
โ†‘(X.presheaf.stalk โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q)) โ†’+* K

Reading the stalk of X at a point of V through a K-isomorphism e : (G', ๐’œ_{G'}) โ‰… X | V and evaluating: ๐’ช_{X, e q} โ†’ ๐’ช_{X|V, e q} โ†’ ๐’œ_{G', q} โ†’ K.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AnalyticSpace.isLocalHom_evalRestrict {K : Type} [RCLike K] (d : โ„•) (G : TopologicalSpace.Opens (Kn K d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G).toPresheafedSpace) :
    IsLocalHom (evalRestrict G q)

    evalRestrict is a local homomorphism (a germ is a unit iff its value is nonzero).

    source
    theorem AnalyticSpace.evalRestrict_constAt {K : Type} [RCLike K] (d : โ„•) (G : TopologicalSpace.Opens (Kn K d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G).toPresheafedSpace) (c : K) :
    (evalRestrict G q) (((analyticSpaceOfOpen K d G).constAt q) c) = c

    evalRestrict fixes the constants.

    source
    theorem AnalyticSpace.isLocalHom_chartEval {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) :
    IsLocalHom (X.chartEval e q)
    source
    theorem AnalyticSpace.chartEval_constAt {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) (c : K) :
    (X.chartEval e q) ((X.constAt โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q)) c) = c
    source
    theorem AnalyticSpace.exists_isLocalHom_const_eq {K : Type} [RCLike K] (X : AnalyticSpace K) {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.regularLocus) :
    โˆƒ (f : โ†‘(X.presheaf.stalk x) โ†’+* K), IsLocalHom f โˆง โˆ€ (c : K), f ((X.constAt x) c) = c

    At a simple point there is a local homomorphism ๐’ช_{X,x} โ†’+* K fixing the constants (through a manifold chart, isRegular_stalk_iff_exists_manifold_nhd).

    source
    noncomputable def AnalyticSpace.regEval {K : Type} [RCLike K] (X : AnalyticSpace K) {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.regularLocus) :
    โ†‘(X.presheaf.stalk x) โ†’+* K

    The evaluation at a simple point x: the unique local ring homomorphism ๐’ช_{X,x} โ†’+* K fixing the constants.

    Equations
    Instances For
      source
      theorem AnalyticSpace.isLocalHom_regEval {K : Type} [RCLike K] (X : AnalyticSpace K) {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.regularLocus) :
      IsLocalHom (X.regEval hx)
      source
      theorem AnalyticSpace.regEval_constAt {K : Type} [RCLike K] (X : AnalyticSpace K) {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.regularLocus) (c : K) :
      (X.regEval hx) ((X.constAt x) c) = c
      source
      theorem AnalyticSpace.eq_regEval {K : Type} [RCLike K] (X : AnalyticSpace K) {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.regularLocus) (f : โ†‘(X.presheaf.stalk x) โ†’+* K) (hf : โˆ€ (c : K), f ((X.constAt x) c) = c) :
      f = X.regEval hx

      The evaluation is the unique ring homomorphism to K fixing the constants.

      source
      theorem AnalyticSpace.chartEval_eq_regEval {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) (hreg : โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q) โˆˆ X.regularLocus) :
      X.chartEval e q = X.regEval hreg

      The evaluation can be computed through any chart.

      source
      theorem AnalyticSpace.mem_reg_of_chart {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) :
      โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q) โˆˆ X.regularLocus

      Every point of a chart neighbourhood is simple (isRegularLocalRing_stalk_of_kIso_analyticSpaceOfOpen).

      source
      noncomputable def AnalyticSpace.sectionViaChart {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (W : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace) (s : โ†‘(X.presheaf.obj (Opposite.op W))) :
      โ†‘((analyticSpaceOfOpen K d G').presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (โ†‘e.hom).base).obj ((TopologicalSpace.Opens.map (โ†‘(X.ofRestrict V)).base).obj W))))

      The pullback along the chart of a section s of ๐’ช_X over W, as a section of ๐’œ_{G'} over the preimage of W โˆฉ V.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AnalyticSpace.regEval_germ {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) (W : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace) (hW : โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q) โˆˆ W) (s : โ†‘(X.presheaf.obj (Opposite.op W))) :
        (X.regEval โ‹ฏ) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ W (โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q)) hW)) s) = Manifold.extendSection K (Kn K d) (X.sectionViaChart e W s) โ†‘q

        The evaluation of the germ of a section is the value of its chart pullback: regEval (s_x) = (e^* s)(q) for x = e q.