Coordinates and pullback for holomorphic germs

This module relates the standard model Fin (n + 1) → ℂ to the product model used by the pinned Weierstrass-preparation dependency. It also constructs contravariant pullback homomorphisms on holomorphic germs, the inclusion of lower-dimensional base germs, and the resulting algebra structure.

The standard successor-coordinate splitting

def LocalComplexGeometry.wptAmbientLinearEquiv (n : ℕ) : ComplexEuclidean (n + 1) ≃ₗ[ℂ] ClassicalComplexWPT.Ambient n

Split the last coordinate of ℂⁿ⁺¹, as a complex-linear equivalence.

Equations

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

noncomputable def LocalComplexGeometry.wptAmbientEquiv (n : ℕ) : ComplexEuclidean (n + 1) ≃L[ℂ] ClassicalComplexWPT.Ambient n

The continuous complex-linear splitting of the last coordinate of ℂⁿ⁺¹.

The codomain is definitionally WPT's (Fin n → ℂ) × ℂ ambient space.

Equations

• LocalComplexGeometry.wptAmbientEquiv n = (LocalComplexGeometry.wptAmbientLinearEquiv n).toContinuousLinearEquiv

@[simp]

theorem LocalComplexGeometry.wptAmbientEquiv_apply (n : ℕ) (x : ComplexEuclidean (n + 1)) : (wptAmbientEquiv n) x = (fun (i : Fin n) => x i.castSucc, x (Fin.last n))

@[simp]

theorem LocalComplexGeometry.wptAmbientEquiv_symm_apply (n : ℕ) (x : ClassicalComplexWPT.Ambient n) : (wptAmbientEquiv n).symm x = fun (i : Fin (n + 1)) => Fin.lastCases x.2 x.1 i

theorem LocalComplexGeometry.wptAmbientEquiv_zero (n : ℕ) : (wptAmbientEquiv n) 0 = 0

theorem LocalComplexGeometry.wptAmbientEquiv_symm_zero (n : ℕ) : (wptAmbientEquiv n).symm 0 = 0

theorem LocalComplexGeometry.analyticAt_comp_wptAmbientEquiv_iff (n : ℕ) (f : ClassicalComplexWPT.Ambient n → ℂ) : AnalyticAt ℂ (f ∘ ⇑(wptAmbientEquiv n)) 0 ↔ AnalyticAt ℂ f 0

Analyticity at the origin is preserved and reflected by the standard/WPT ambient-coordinate equivalence.

theorem LocalComplexGeometry.eventuallyEq_comp_wptAmbientEquiv_iff (n : ℕ) (f g : ClassicalComplexWPT.Ambient n → ℂ) : f ∘ ⇑(wptAmbientEquiv n) =ᶠ[nhds 0] g ∘ ⇑(wptAmbientEquiv n) ↔ f =ᶠ[nhds 0] g

Neighborhood equality at the origin is preserved and reflected by the standard/WPT ambient-coordinate equivalence.

Pullback of function germs and holomorphic germs

noncomputable def LocalComplexGeometry.functionGermPullbackHom {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) : FunctionGerm m →+* FunctionGerm n

Precomposition of function germs by a continuous linear map fixing the origin.

Equations

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

@[simp]

theorem LocalComplexGeometry.functionGermPullbackHom_coe {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (f : ComplexEuclidean m → ℂ) : (functionGermPullbackHom L) ↑f = ↑(f ∘ ⇑L)

@[simp]

theorem LocalComplexGeometry.functionGermPullbackHom_value {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (φ : FunctionGerm m) : Filter.Germ.value ((functionGermPullbackHom L) φ) = Filter.Germ.value φ

@[simp]

theorem LocalComplexGeometry.functionGermPullbackHom_id (n : ℕ) : functionGermPullbackHom (ContinuousLinearMap.id ℂ (ComplexEuclidean n)) = RingHom.id (FunctionGerm n)

theorem LocalComplexGeometry.functionGermPullbackHom_comp {n m k : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (M : ComplexEuclidean m →L[ℂ] ComplexEuclidean k) : functionGermPullbackHom (M ∘SL L) = (functionGermPullbackHom L).comp (functionGermPullbackHom M)

theorem LocalComplexGeometry.functionGermPullbackHom_leftInverse {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) : Function.LeftInverse ⇑(functionGermPullbackHom ↑L.symm) ⇑(functionGermPullbackHom ↑L)

theorem LocalComplexGeometry.functionGermPullbackHom_rightInverse {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) : Function.RightInverse ⇑(functionGermPullbackHom ↑L.symm) ⇑(functionGermPullbackHom ↑L)

noncomputable def LocalComplexGeometry.holomorphicGermPullbackHom {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) : ↥(HolomorphicGerm m) →+* ↥(HolomorphicGerm n)

Pullback of holomorphic germs by a continuous complex-linear map.

Equations

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

@[simp]

theorem LocalComplexGeometry.holomorphicGermPullbackHom_coe {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (φ : ↥(HolomorphicGerm m)) : ↑((holomorphicGermPullbackHom L) φ) = (functionGermPullbackHom L) ↑φ

@[simp]

theorem LocalComplexGeometry.holomorphicGermPullbackHom_ofFunction {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (f : ComplexEuclidean m → ℂ) (hf : AnalyticAt ℂ f 0) : (holomorphicGermPullbackHom L) (HolomorphicGerm.ofFunction f hf) = HolomorphicGerm.ofFunction (f ∘ ⇑L) ⋯

@[simp]

theorem LocalComplexGeometry.evalAtOrigin_holomorphicGermPullbackHom {n m : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (φ : ↥(HolomorphicGerm m)) : evalAtOrigin ((holomorphicGermPullbackHom L) φ) = evalAtOrigin φ

@[simp]

theorem LocalComplexGeometry.holomorphicGermPullbackHom_id (n : ℕ) : holomorphicGermPullbackHom (ContinuousLinearMap.id ℂ (ComplexEuclidean n)) = RingHom.id ↥(HolomorphicGerm n)

theorem LocalComplexGeometry.holomorphicGermPullbackHom_comp {n m k : ℕ} (L : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) (M : ComplexEuclidean m →L[ℂ] ComplexEuclidean k) : holomorphicGermPullbackHom (M ∘SL L) = (holomorphicGermPullbackHom L).comp (holomorphicGermPullbackHom M)

noncomputable def LocalComplexGeometry.coordinatePullback {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) : ↥(HolomorphicGerm m) ≃+* ↥(HolomorphicGerm n)

Pullback by a continuous complex-linear equivalence, as a ring equivalence.

The direction is contravariant: an equivalence L : ℂⁿ ≃L[ℂ] ℂᵐ induces an equivalence from germs on ℂᵐ to germs on ℂⁿ.

Equations

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

@[simp]

theorem LocalComplexGeometry.coordinatePullback_apply {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) (φ : ↥(HolomorphicGerm m)) : (coordinatePullback L) φ = (holomorphicGermPullbackHom ↑L) φ

@[simp]

theorem LocalComplexGeometry.coordinatePullback_symm_apply {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) (φ : ↥(HolomorphicGerm n)) : (coordinatePullback L).symm φ = (holomorphicGermPullbackHom ↑L.symm) φ

theorem LocalComplexGeometry.evalAtOrigin_coordinatePullback {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) (φ : ↥(HolomorphicGerm m)) : evalAtOrigin ((coordinatePullback L) φ) = evalAtOrigin φ

@[simp]

theorem LocalComplexGeometry.coordinatePullback_refl (n : ℕ) : coordinatePullback (ContinuousLinearEquiv.refl ℂ (ComplexEuclidean n)) = RingEquiv.refl ↥(HolomorphicGerm n)

theorem LocalComplexGeometry.coordinatePullback_trans {n m k : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) (M : ComplexEuclidean m ≃L[ℂ] ComplexEuclidean k) : coordinatePullback (L.trans M) = (coordinatePullback M).trans (coordinatePullback L)

@[simp]

theorem LocalComplexGeometry.coordinatePullback_symm {n m : ℕ} (L : ComplexEuclidean n ≃L[ℂ] ComplexEuclidean m) : coordinatePullback L.symm = (coordinatePullback L).symm

Base inclusion and the last coordinate

noncomputable def LocalComplexGeometry.baseProjectionCLM (n : ℕ) : ComplexEuclidean (n + 1) →L[ℂ] ComplexEuclidean n

Projection from ℂⁿ⁺¹ to its first n coordinates.

Equations

• LocalComplexGeometry.baseProjectionCLM n = ContinuousLinearMap.fst ℂ (LocalComplexGeometry.ComplexEuclidean n) ℂ ∘SL ↑(LocalComplexGeometry.wptAmbientEquiv n)

@[simp]

theorem LocalComplexGeometry.baseProjectionCLM_apply (n : ℕ) (x : ComplexEuclidean (n + 1)) : (baseProjectionCLM n) x = fun (i : Fin n) => x i.castSucc

noncomputable def LocalComplexGeometry.baseSectionCLM (n : ℕ) : ComplexEuclidean n →L[ℂ] ComplexEuclidean (n + 1)

The zero-last-coordinate section z ↦ (z, 0) in the standard model.

Equations

• LocalComplexGeometry.baseSectionCLM n = ↑(LocalComplexGeometry.wptAmbientEquiv n).symm ∘SL ContinuousLinearMap.inl ℂ (LocalComplexGeometry.ComplexEuclidean n) ℂ

@[simp]

theorem LocalComplexGeometry.baseSectionCLM_castSucc (n : ℕ) (z : ComplexEuclidean n) (i : Fin n) : (baseSectionCLM n) z i.castSucc = z i

@[simp]

theorem LocalComplexGeometry.baseSectionCLM_last (n : ℕ) (z : ComplexEuclidean n) : (baseSectionCLM n) z (Fin.last n) = 0

noncomputable def LocalComplexGeometry.lastCoordinateCLM (n : ℕ) : ComplexEuclidean (n + 1) →L[ℂ] ℂ

Extraction of the last coordinate of ℂⁿ⁺¹.

Equations

• LocalComplexGeometry.lastCoordinateCLM n = ContinuousLinearMap.snd ℂ (LocalComplexGeometry.ComplexEuclidean n) ℂ ∘SL ↑(LocalComplexGeometry.wptAmbientEquiv n)

@[simp]

theorem LocalComplexGeometry.lastCoordinateCLM_apply (n : ℕ) (x : ComplexEuclidean (n + 1)) : (lastCoordinateCLM n) x = x (Fin.last n)

@[simp]

theorem LocalComplexGeometry.baseProjectionCLM_comp_baseSectionCLM (n : ℕ) : baseProjectionCLM n ∘SL baseSectionCLM n = ContinuousLinearMap.id ℂ (ComplexEuclidean n)

noncomputable def LocalComplexGeometry.lowerDimensionalInclusion (n : ℕ) : ↥(HolomorphicGerm n) →+* ↥(HolomorphicGerm (n + 1))

Include a base germ as a germ independent of the last coordinate.

Equations

• LocalComplexGeometry.lowerDimensionalInclusion n = LocalComplexGeometry.holomorphicGermPullbackHom (LocalComplexGeometry.baseProjectionCLM n)

noncomputable def LocalComplexGeometry.lowerDimensionalRestriction (n : ℕ) : ↥(HolomorphicGerm (n + 1)) →+* ↥(HolomorphicGerm n)

Restrict an ambient germ to the zero-last-coordinate base section.

Equations

• LocalComplexGeometry.lowerDimensionalRestriction n = LocalComplexGeometry.holomorphicGermPullbackHom (LocalComplexGeometry.baseSectionCLM n)

@[simp]

theorem LocalComplexGeometry.lowerDimensionalInclusion_ofFunction {n : ℕ} (f : ComplexEuclidean n → ℂ) (hf : AnalyticAt ℂ f 0) : (lowerDimensionalInclusion n) (HolomorphicGerm.ofFunction f hf) = HolomorphicGerm.ofFunction (f ∘ ⇑(baseProjectionCLM n)) ⋯

@[simp]

theorem LocalComplexGeometry.lowerDimensionalRestriction_ofFunction {n : ℕ} (f : ComplexEuclidean (n + 1) → ℂ) (hf : AnalyticAt ℂ f 0) : (lowerDimensionalRestriction n) (HolomorphicGerm.ofFunction f hf) = HolomorphicGerm.ofFunction (f ∘ ⇑(baseSectionCLM n)) ⋯

@[simp]

theorem LocalComplexGeometry.evalAtOrigin_lowerDimensionalInclusion {n : ℕ} (φ : ↥(HolomorphicGerm n)) : evalAtOrigin ((lowerDimensionalInclusion n) φ) = evalAtOrigin φ

@[simp]

theorem LocalComplexGeometry.evalAtOrigin_lowerDimensionalRestriction {n : ℕ} (φ : ↥(HolomorphicGerm (n + 1))) : evalAtOrigin ((lowerDimensionalRestriction n) φ) = evalAtOrigin φ

@[simp]

theorem LocalComplexGeometry.lowerDimensionalRestriction_comp_inclusion (n : ℕ) : (lowerDimensionalRestriction n).comp (lowerDimensionalInclusion n) = RingHom.id ↥(HolomorphicGerm n)

theorem LocalComplexGeometry.lowerDimensionalInclusion_injective (n : ℕ) : Function.Injective ⇑(lowerDimensionalInclusion n)

noncomputable def LocalComplexGeometry.lastCoordinateGerm (n : ℕ) : ↥(HolomorphicGerm (n + 1))

The germ of the last coordinate w on ℂⁿ⁺¹.

Equations

• LocalComplexGeometry.lastCoordinateGerm n = LocalComplexGeometry.HolomorphicGerm.ofFunction ⇑(LocalComplexGeometry.lastCoordinateCLM n) ⋯

@[simp]

theorem LocalComplexGeometry.evalAtOrigin_lastCoordinateGerm (n : ℕ) : evalAtOrigin (lastCoordinateGerm n) = 0

@[simp]

theorem LocalComplexGeometry.lowerDimensionalRestriction_lastCoordinateGerm (n : ℕ) : (lowerDimensionalRestriction n) (lastCoordinateGerm n) = 0

The ambient germ ring as an algebra over the base germ ring

@[instance_reducible]

noncomputable instance LocalComplexGeometry.holomorphicGermSuccAlgebra (n : ℕ) : Algebra ↥(HolomorphicGerm n) ↥(HolomorphicGerm (n + 1))

The natural algebra structure induced by germs independent of the last coordinate.

Equations

• LocalComplexGeometry.holomorphicGermSuccAlgebra n = (LocalComplexGeometry.lowerDimensionalInclusion n).toAlgebra

@[simp]

theorem LocalComplexGeometry.algebraMap_holomorphicGermSucc (n : ℕ) : algebraMap ↥(HolomorphicGerm n) ↥(HolomorphicGerm (n + 1)) = lowerDimensionalInclusion n

@[simp]

theorem LocalComplexGeometry.algebraMap_holomorphicGermSucc_apply (n : ℕ) (φ : ↥(HolomorphicGerm n)) : (algebraMap ↥(HolomorphicGerm n) ↥(HolomorphicGerm (n + 1))) φ = (lowerDimensionalInclusion n) φ

theorem LocalComplexGeometry.holomorphicGermSucc_smul_eq_mul (n : ℕ) (a : ↥(HolomorphicGerm n)) (f : ↥(HolomorphicGerm (n + 1))) : a • f = (lowerDimensionalInclusion n) a * f