Documentation

LeanPool.LocalComplexGeometry.Germs.Ring

Constant germs and the residue field #

This file packages the constant inclusion, identifies the residue field with ℂ, and supplies the zero-dimensional base case used by Rückert induction.

source
noncomputable def LocalComplexGeometry.constantGermHom (n : ℕ) :
ℂ →+* ↥(HolomorphicGerm n)

Embed a complex number as a constant holomorphic germ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LocalComplexGeometry.evalAtOrigin_constantGerm (n : ℕ) (c : ℂ) :
    (evalAtOriginHom n) ((constantGermHom n) c) = c
    source
    theorem LocalComplexGeometry.evalAtOrigin_surjective (n : ℕ) :
    Function.Surjective ⇑(evalAtOriginHom n)

    Evaluation at the origin is onto, with the constant-germ map as a section.

    source
    theorem LocalComplexGeometry.holomorphicGerm_maximalIdeal_eq_ker (n : ℕ) :
    IsLocalRing.maximalIdeal ↥(HolomorphicGerm n) = RingHom.ker (evalAtOriginHom n)

    The maximal ideal is the kernel of evaluation at the origin.

    source
    noncomputable def LocalComplexGeometry.holomorphicGermResidueFieldEquiv (n : ℕ) :
    ↥(HolomorphicGerm n) ⧸ IsLocalRing.maximalIdeal ↥(HolomorphicGerm n) ≃+* ℂ

    The residue field of the holomorphic local ring is canonically ℂ.

    Equations
    Instances For
      source
      @[simp]
      theorem LocalComplexGeometry.holomorphicGerm_residueFieldEquiv_mk (n : ℕ) (f : ↥(HolomorphicGerm n)) :
      (holomorphicGermResidueFieldEquiv n) ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥(HolomorphicGerm n))) f) = evalAtOrigin f
      source
      theorem LocalComplexGeometry.evalAtOrigin_injective_zero :
      Function.Injective ⇑(evalAtOriginHom 0)

      In complex dimension zero, evaluation is injective.

      source
      noncomputable def LocalComplexGeometry.holomorphicGermZeroEquiv :
      ↥(HolomorphicGerm 0) ≃+* ℂ

      The zero-dimensional holomorphic germ ring is canonically ℂ.

      Equations
      Instances For
        source
        @[simp]
        theorem LocalComplexGeometry.holomorphicGermZeroEquiv_apply (f : ↥(HolomorphicGerm 0)) :
        holomorphicGermZeroEquiv f = evalAtOrigin f
        source
        theorem LocalComplexGeometry.holomorphicGerm_isNoetherian_zero :
        IsNoetherianRing ↥(HolomorphicGerm 0)

        The zero-dimensional case of Rückert's basis theorem.