The differential of a germ of 𝒜_{Kⁿ}

The Taylor homomorphism T_q : 𝒜_{Kⁿ,q} → K[[X]] of a regular coordinate chart [BM97, (0.3)], here taylorHom in the identity chart of Kⁿ. The differential d_q s of a germ s at q is the linear part of its Taylor series: the vector (∂_i s (q))_i ∈ Kⁿ of the coefficients of X_i in T_q s, read as the functional v ↦ ∑ ∂_i s(q) v_i on Kⁿ. It is the linearPart of Hironaka/Manifold/Chart/Cotangent.lean in the identity chart of Kⁿ with the coordinates ContinuousLinearEquiv.ulift, here as an additive map dlin : 𝒜_{Kⁿ,q} →+ (Fin n → K) on the presentation (affine K n).presheaf.stalk q of the stalk (the same type as (structureSheaf K Kⁿ Kⁿ).presheaf.stalk q, on which the K-algebra structure and linearPart live; dlin_eq_linearPart is rfl). The differential identifies 𝔪_q/𝔪_q² with the dual of Kⁿ, and germs of 𝔪_q are part of a regular system of parameters iff their differentials are linearly independent (Hironaka/AnalyticSpace/RegularParameters.lean); the statements about dlin alone are proved here.

• taylorAt K n q: the Taylor homomorphism of 𝒜_{Kⁿ,q} in the identity chart of Kⁿ with the coordinates ContinuousLinearEquiv.ulift;
• dlin K n q: the differential, s ↦ (coeff (X_i) (T_q s))_i; dlin_eq_linearPart;
• dlin_coordAt_sub: the normalisation d_q (z_i − q_i) = e_i, so dlin is the coordinate differential and not one up to GL_n(K);
• dlin_constAt, dlin_const_mul, dlin_eq_zero_iff_mem_maximalIdeal_sq, exists_mem_maximalIdeal_dlin_eq, linearIndependent_dlin_germ_iff_hasIndependentDifferentialsAt: the differential of a constant vanishes, dlin is K-linear, a germ of 𝔪_q has zero differential iff it lies in 𝔪_q² (Hadamard's lemma), every functional is a differential, and the linear independence of the differentials of germs of analytic functions is the independence of their derivatives (HasIndependentDifferentialsAt).

noncomputable def AnalyticSpace.taylorAt (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) : ↑((affine K n).presheaf.stalk q) →+* MvPowerSeries (Fin n) K

The Taylor homomorphism T_q : 𝒜_{Kⁿ,q} →+* K[[X₁, …, Xₙ]] in the identity chart of Kⁿ, with the coordinates ContinuousLinearEquiv.ulift : Kⁿ ≃L[K] (Fin n → K).

Equations

• AnalyticSpace.taylorAt K n q = Manifold.taylorHom (AnalyticSpace.Kn K n) ContinuousLinearEquiv.ulift (chartAt (AnalyticSpace.Kn K n) q) ⋯ ⋯

theorem AnalyticSpace.taylorAt_apply (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (s : ↑((affine K n).presheaf.stalk q)) : (taylorAt K n q) s = (Manifold.taylorHom (Kn K n) ContinuousLinearEquiv.ulift (chartAt (Kn K n) q) ⋯ ⋯) s

noncomputable def AnalyticSpace.dlin (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) : ↑((affine K n).presheaf.stalk q) →+ Fin n → K

The differential of a germ at q, the linear part of its Taylor series: the vector of the coefficients of X₁, …, Xₙ in T_q s, i.e. (∂_i s (q))_i. It is linearPart in the identity chart of Kⁿ (dlin_eq_linearPart).

Equations

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

theorem AnalyticSpace.dlin_apply (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (s : ↑((affine K n).presheaf.stalk q)) (i : Fin n) : (dlin K n q) s i = (MvPowerSeries.coeff (Finsupp.single i 1)) ((taylorAt K n q) s)

theorem AnalyticSpace.dlin_eq_linearPart (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (s : ↑((affine K n).presheaf.stalk q)) : (dlin K n q) s = (Manifold.linearPart (Kn K n) ContinuousLinearEquiv.ulift (chartAt (Kn K n) q) ⋯ ⋯) s

dlin is the K-linear linearPart of Hironaka/Manifold/Chart/Cotangent.lean in the identity chart of Kⁿ with the coordinates ContinuousLinearEquiv.ulift, definitionally.

theorem AnalyticSpace.constAt_affine_eq (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) : ((affine K n).constAt q) c = (Manifold.const K (Kn K n) (Kn K n) q) c

The constants of 𝒜_{Kⁿ,q} given by the K-structure (constAt) are the constant germs const.

theorem AnalyticSpace.dlin_coordAt_sub (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (i : Fin n) : (dlin K n q) (coordAt K n q i - (Manifold.const K (Kn K n) (Kn K n) q) (q.down i)) = Pi.single i 1

The normalisation: the differential of the centred coordinate germ z_i − q_i is the i-th standard basis vector — dlin is the coordinate differential (∂_i s (q))_i.

theorem AnalyticSpace.dlin_constAt (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) : (dlin K n q) (((affine K n).constAt q) c) = 0

The differential of a constant vanishes.

theorem AnalyticSpace.dlin_const_mul' (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) (s : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : (dlin K n q) ((Manifold.const K (Kn K n) (Kn K n) q) c * s) = c • (dlin K n q) s

The differential is K-linear: it scales with the constant germs const.

theorem AnalyticSpace.dlin_const_mul (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) (s : ↑((affine K n).presheaf.stalk q)) : (dlin K n q) (((affine K n).constAt q) c * s) = c • (dlin K n q) s

The differential is K-linear: it scales with the constants constAt of the K-structure.

theorem AnalyticSpace.dlin_eq_zero_iff_mem_maximalIdeal_sq (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {s : ↑((affine K n).presheaf.stalk q)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk q)) : (dlin K n q) s = 0 ↔ s ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk q) ^ 2

A germ of 𝔪_q has zero differential iff it lies in 𝔪_q² (Hadamard's lemma).

theorem AnalyticSpace.exists_mem_maximalIdeal_dlin_eq (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (v : Fin n → K) : ∃ s ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk q), (dlin K n q) s = v

Every functional on Kⁿ is the differential of a germ vanishing at q — the differential is onto: v = d_q (∑ v_i (z_i − q_i)).

theorem AnalyticSpace.linearIndependent_dlin_germ_iff_hasIndependentDifferentialsAt (K : Type) [RCLike K] (n : ℕ) (U : TopologicalSpace.Opens (Kn K n)) {c : ℕ} (g : Fin c → AnalyticFun K n U) (q : Kn K n) (hq : q ∈ U) : (LinearIndependent K fun (i : Fin c) => (dlin K n q) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U q hq)) (g i))) ↔ Manifold.HasIndependentDifferentialsAt (Kn K n) (fun (i : Fin c) => Manifold.extendSection K (Kn K n) (g i)) q

For germs of analytic functions on an open U ⊆ Kⁿ, the linear independence of the differentials is the independence of the derivatives of the functions (HasIndependentDifferentialsAt, in terms of mfderiv).