Documentation

TauCeti.Geometry.Manifold.Complex.StructureSheaf.MaximalIdeal

Local coordinates generate the maximal ideal of a holomorphic stalk #

Let X be a complex manifold modelled on ๐“˜(โ„‚, E) and let e be a holomorphic chart at x. Every continuous linear functional โ„“ on E gives a holomorphic coordinate y โ†ฆ โ„“ (e y - e x) centered at x, and its germ e.holomorphicLinearCoordinateGerm he x โ„“ hx lies in the maximal ideal of the stalk ๐’ช_x, which is the kernel of evaluation at x.

When E is finite-dimensional, Hadamard's lemma AnalyticAt.exists_analyticAt_eventually_sub_eq writes every germ vanishing at x as โˆ‘ i, zแตข * qแตข, where zแตข are the coordinate germs along the coordinate functionals b.coord i of a basis b of E, and the values qแตข(x) are the partial derivatives of the germ in the chart. Consequently:

The first statement is the several-variable analogue of the one-variable OpenPartialHomeomorph.ker_eval_eq_span_holomorphicCoordinateGerm for complex curves. Together, the two statements say that n = dim E coordinate germs generate the maximal ideal ๐”ช of the analytic local ring, and that a germ in ๐”ช is determined modulo ๐”ชยฒ by its derivative at x read in the chart.

References #

Linear coordinates of a chart #

source
noncomputable def OpenPartialHomeomorph.holomorphicLinearCoordinateSection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (โ„“ : StrongDual โ„‚ E) (z : E) :
โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).obj.obj (Opposite.op { carrier := e.source, is_open' := โ‹ฏ }))

The coordinate of the chart e along a continuous linear functional โ„“, translated by z, as a holomorphic section on the chart source: y โ†ฆ โ„“ (e y - z).

Instances For
    source
    @[simp]
    theorem OpenPartialHomeomorph.holomorphicLinearCoordinateSection_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (โ„“ : StrongDual โ„‚ E) (z : E) (y : โ†ฅ{ carrier := e.source, is_open' := โ‹ฏ }) :
    TauCeti.holomorphicStructureSheaf.toFun (modelWithCornersSelf โ„‚ E) X (Opposite.op { carrier := e.source, is_open' := โ‹ฏ }) (e.holomorphicLinearCoordinateSection he โ„“ z) y = โ„“ (โ†‘e โ†‘y - z)

    The translated linear coordinate section evaluates at y to โ„“ (e y - z).

    source
    noncomputable def OpenPartialHomeomorph.holomorphicLinearCoordinateGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (x : X) (โ„“ : StrongDual โ„‚ E) (hx : x โˆˆ e.source) :
    โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.stalk x)

    The germ at x of the centered linear coordinate y โ†ฆ โ„“ (e y - e x) of the chart e.

    Instances For
      source
      theorem OpenPartialHomeomorph.holomorphicLinearCoordinateGerm_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (x : X) (โ„“ : StrongDual โ„‚ E) (hx : x โˆˆ e.source) :
      e.holomorphicLinearCoordinateGerm he x โ„“ hx = (CategoryTheory.ConcreteCategory.hom ((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.germ { carrier := e.source, is_open' := โ‹ฏ } x hx)) (e.holomorphicLinearCoordinateSection he โ„“ (โ†‘e x))

      The centered linear coordinate germ is the germ of the translated coordinate section.

      source
      @[simp]
      theorem OpenPartialHomeomorph.toFilterGerm_holomorphicLinearCoordinateGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (x : X) (โ„“ : StrongDual โ„‚ E) (hx : x โˆˆ e.source) {l : Filter X} (hl : l โ‰ค nhds x) :
      (TauCeti.holomorphicStructureSheaf.toFilterGerm (modelWithCornersSelf โ„‚ E) X x l hl) (e.holomorphicLinearCoordinateGerm he x โ„“ hx) = โ†‘fun (y : X) => โ„“ (โ†‘e y - โ†‘e x)

      As a germ of functions, the centered linear coordinate germ is y โ†ฆ โ„“ (e y - e x).

      source
      @[simp]
      theorem OpenPartialHomeomorph.eval_holomorphicLinearCoordinateGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) (x : X) (โ„“ : StrongDual โ„‚ E) (hx : x โˆˆ e.source) :
      (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) (e.holomorphicLinearCoordinateGerm he x โ„“ hx) = 0

      The centered linear coordinate germs vanish at their center.

      Hadamard's lemma for holomorphic germs #

      source
      theorem OpenPartialHomeomorph.analyticAt_comp_symm_of_toFilterGerm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) {x : X} (hx : x โˆˆ e.source) {s : โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.stalk x)} {ฯ† : X โ†’ โ„‚} (hฯ† : (TauCeti.holomorphicStructureSheaf.toFilterGerm (modelWithCornersSelf โ„‚ E) X x (nhds x) โ‹ฏ) s = โ†‘ฯ†) :
      AnalyticAt โ„‚ (ฯ† โˆ˜ โ†‘e.symm) (โ†‘e x)

      Every representative of a holomorphic germ at x is analytic at e x when read in the chart e.

      source
      theorem OpenPartialHomeomorph.exists_eq_sum_holomorphicLinearCoordinateGerm_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) {x : X} [FiniteDimensional โ„‚ E] {ฮน : Type u_2} (b : Module.Basis ฮน โ„‚ E) [Fintype ฮน] (hx : x โˆˆ e.source) {s : โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.stalk x)} (hs : (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) s = 0) {ฯ† : X โ†’ โ„‚} (hฯ† : (TauCeti.holomorphicStructureSheaf.toFilterGerm (modelWithCornersSelf โ„‚ E) X x (nhds x) โ‹ฏ) s = โ†‘ฯ†) :
      โˆƒ (q : ฮน โ†’ โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.stalk x)), s = โˆ‘ i : ฮน, e.holomorphicLinearCoordinateGerm he x (LinearMap.toContinuousLinearMap (b.coord i)) hx * q i โˆง โˆ€ (i : ฮน), (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) (q i) = (fderiv โ„‚ (ฯ† โˆ˜ โ†‘e.symm) (โ†‘e x)) (b i)

      Hadamard's lemma for holomorphic germs. A holomorphic germ vanishing at x is a combination โˆ‘ i, zแตข * qแตข of the centered coordinate germs zแตข along the coordinate functionals of a basis b, whose coefficients qแตข take at x the values of the partial derivatives โˆ‚ฯ†/โˆ‚zแตข of any representative ฯ†, read in the chart e.

      The maximal ideal and its square #

      source
      theorem OpenPartialHomeomorph.ker_eval_eq_span_holomorphicLinearCoordinateGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) {x : X} [FiniteDimensional โ„‚ E] {ฮน : Type u_2} (b : Module.Basis ฮน โ„‚ E) (hx : x โˆˆ e.source) :
      RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) = Ideal.span (Set.range fun (i : ฮน) => e.holomorphicLinearCoordinateGerm he x (LinearMap.toContinuousLinearMap (b.coord i)) hx)

      Local coordinates generate the maximal ideal. The germs at x of the centered coordinates y โ†ฆ b.coord i (e y - e x) of a holomorphic chart, for a basis b of the finite-dimensional model E, generate the ideal of holomorphic germs vanishing at x.

      source
      theorem OpenPartialHomeomorph.ker_eval_eq_span_range_holomorphicLinearCoordinateGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) {x : X} [FiniteDimensional โ„‚ E] (hx : x โˆˆ e.source) :
      RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) = Ideal.span (Set.range fun (โ„“ : StrongDual โ„‚ E) => e.holomorphicLinearCoordinateGerm he x โ„“ hx)

      The ideal of holomorphic germs vanishing at x is generated by the centered linear coordinate germs y โ†ฆ โ„“ (e y - e x) of a holomorphic chart, over all continuous linear functionals โ„“ on the finite-dimensional model E.

      source
      theorem OpenPartialHomeomorph.mem_ker_eval_sq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„‚ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersSelf โ„‚ E) โŠค X) {x : X} [FiniteDimensional โ„‚ E] (hx : x โˆˆ e.source) {s : โ†‘((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf โ„‚ E) X).presheaf.stalk x)} {ฯ† : X โ†’ โ„‚} (hฯ† : (TauCeti.holomorphicStructureSheaf.toFilterGerm (modelWithCornersSelf โ„‚ E) X x (nhds x) โ‹ฏ) s = โ†‘ฯ†) :
      s โˆˆ RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf โ„‚ E) X x) ^ 2 โ†” ฯ† x = 0 โˆง fderiv โ„‚ (ฯ† โˆ˜ โ†‘e.symm) (โ†‘e x) = 0

      The square of the maximal ideal. A holomorphic germ lies in the square of the ideal of germs vanishing at x exactly when any of its representatives ฯ† vanishes at x together with its derivative read in a holomorphic chart e.