Documentation

LeanPool.LocalComplexGeometry.Nullstellensatz.Coordinates

Coordinate pullback of local set germs #

The analytic Nullstellensatz is invariant under invertible complex-linear coordinates. This file records that invariance at the predicate-germ level, without evaluating abstract function germs away from the origin.

source
noncomputable def LocalComplexGeometry.localSetGermPullback {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) :
LocalSetGerm m → LocalSetGerm n

Pull a local predicate germ back along a continuous complex-linear map.

Equations
Instances For
    source
    @[simp]
    theorem LocalComplexGeometry.localSetGermPullback_top {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) :
    localSetGermPullback L ⊤ = ⊤
    source
    @[simp]
    theorem LocalComplexGeometry.localSetGermPullback_inf {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (Z W : LocalSetGerm m) :
    localSetGermPullback L (Z ⊓ W) = localSetGermPullback L Z ⊓ localSetGermPullback L W
    source
    theorem LocalComplexGeometry.localSetGermPullback_mono {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) :
    Monotone (localSetGermPullback L)
    source
    @[simp]
    theorem LocalComplexGeometry.localSetGermPullback_zeroLocus {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (f : ↥(HolomorphicGerm m)) :
    localSetGermPullback L (germZeroLocus f) = germZeroLocus ((holomorphicGermPullbackHom L) f)
    source
    theorem LocalComplexGeometry.localSetGermPullback_le_iff {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) (Z W : LocalSetGerm m) :
    localSetGermPullback (↑L) Z ≤ localSetGermPullback (↑L) W ↔ Z ≤ W

    Pullback by a continuous-linear equivalence reflects as well as preserves inclusion of local set germs.

    source
    theorem LocalComplexGeometry.localSetGermPullback_finiteCommonZeroSet {n : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean n) (S : Finset ↥(HolomorphicGerm n)) :
    localSetGermPullback (↑L) (finiteCommonZeroSet S) = finiteCommonZeroSet (Finset.image (⇑(coordinatePullback L)) S)

    Pullback commutes with a finite common zero set under an invertible linear coordinate change.

    source
    theorem LocalComplexGeometry.idealZeroSetGerm_map_coordinatePullback {n : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean n) (I : Ideal ↥(HolomorphicGerm n)) :
    idealZeroSetGerm (Ideal.map (coordinatePullback L).toRingHom I) = localSetGermPullback (↑L) (idealZeroSetGerm I)

    Mapping an ideal by a coordinate pullback maps its local zero-set germ by the corresponding geometric pullback.

    source
    theorem LocalComplexGeometry.coordinatePullback_mem_vanishingIdeal_iff {n : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean n) (I : Ideal ↥(HolomorphicGerm n)) (f : ↥(HolomorphicGerm n)) :
    (coordinatePullback L) f ∈ vanishingIdeal (idealZeroSetGerm (Ideal.map (coordinatePullback L).toRingHom I)) ↔ f ∈ vanishingIdeal (idealZeroSetGerm I)

    Vanishing-ideal membership is reflected by an invertible linear coordinate change.

    source
    theorem LocalComplexGeometry.vanishingIdeal_idealZeroSetGerm_eq_iff_coordinateMap {n : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean n) (I : Ideal ↥(HolomorphicGerm n)) :
    vanishingIdeal (idealZeroSetGerm (Ideal.map (coordinatePullback L).toRingHom I)) = Ideal.map (coordinatePullback L).toRingHom I ↔ vanishingIdeal (idealZeroSetGerm I) = I

    Equality with the vanishing ideal is invariant under invertible linear coordinate changes.