Independent differentials and the cotangent space 𝔪_a / 𝔪_a²

For sections z_1, …, z_c of 𝒪_M near a, their differentials at a are linearly independent iff the classes of z_i − z_i(a) in 𝔪_a / 𝔪_a² are linearly independent over 𝕜 (hasIndependentDifferentialsAt_iff_linearIndependent_cotangentClass'). This is the identification of the differentials of functions with the cotangent space of the local ring, as in Kollár's local coordinates and their derivations [Kol07, Definition 73] and Bierstone–Milman's regular coordinate charts [BM97, (0.3)]. The bridge is the linear part of a germ in a chart — the degree-one coefficients of its Taylor series — a 𝕜-linear map 𝒪_{M,a} → 𝕜^n which kills the constants and 𝔪_a² and detects 𝔪_a² inside 𝔪_a (Hadamard: a germ vanishing at a with vanishing first derivatives has Taylor order ≥ 2, taylorHom_mem_maximalIdeal_pow_iff), so that a 𝕜-combination of classes vanishes iff the same combination of linear parts does; and the linear part of the germ of a section is the vector of values of its chart derivative on the basis ψ⁻¹(e_j) (eval_coordDerivStalk_germ), whose independence is the independence of the chart derivatives themselves (linearIndependent_fderiv_chart_iff'). This is the form in which the independence of differentials is passed to the analytic spaces (Hironaka/AnalyticSpace/Differential.lean) and to the common-chart constructions of maximal contact.

noncomputable def Manifold.linearPart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →ₗ[𝕜] Fin n → 𝕜

The linear part of a germ in the chart φ: the degree-one coefficients of its Taylor series, as a 𝕜-linear map 𝒪_{M,a} → 𝕜^n.

Equations

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

theorem Manifold.linearPart_apply {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (i : Fin n) : (linearPart E ψ φ hφ ha) s i = (MvPowerSeries.coeff (Finsupp.single i 1)) ((taylorHom E ψ φ ha hφ) s)

theorem Manifold.linearPart_const {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (c : 𝕜) : (linearPart E ψ φ hφ ha) ((const 𝕜 E M a) c) = 0

The linear part kills the constants.

theorem Manifold.linearPart_eq_zero_of_mem_sq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ 2) : (linearPart E ψ φ hφ ha) s = 0

The linear part kills 𝔪_a² (the Taylor series has order ≥ 2).

theorem Manifold.mem_sq_of_linearPart_eq_zero {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (h : (linearPart E ψ φ hφ ha) s = 0) : s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ 2

Hadamard: a germ vanishing at a with vanishing linear part lies in 𝔪_a².

noncomputable def Manifold.cotangentClassₗ {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →ₗ[𝕜] (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)).Cotangent

s ↦ [s − s(a)] ∈ 𝔪_a / 𝔪_a² as a 𝕜-linear map.

Equations

• Manifold.cotangentClassₗ E a = { toFun := fun (s : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) => Manifold.cotangentClass E a s, map_add' := ⋯, map_smul' := ⋯ }

theorem Manifold.cotangentClassₗ_apply {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (cotangentClassₗ E a) s = cotangentClass E a s

theorem Manifold.cotangentClass_eq_zero_iff_linearPart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : cotangentClass E a s = 0 ↔ (linearPart E ψ φ hφ ha) s = 0

The class of s − s(a) vanishes iff s − s(a) ∈ 𝔪_a² iff the linear part of s vanishes.

theorem Manifold.linearIndependent_cotangentClass_iff_linearPart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {ι : Type u_2} [Finite ι] (s : ι → ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : (LinearIndependent 𝕜 fun (i : ι) => cotangentClass E a (s i)) ↔ LinearIndependent 𝕜 fun (i : ι) => (linearPart E ψ φ hφ ha) (s i)

A family of germs has linearly independent cotangent classes iff it has linearly independent linear parts.

theorem ContinuousLinearMap.ext_of_symm_single {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {L L' : E →L[𝕜] 𝕜} (h : ∀ (j : Fin n), L (ψ.symm (Pi.single j 1)) = L' (ψ.symm (Pi.single j 1))) : L = L'

A continuous linear functional on E is determined by its values on the basis ψ⁻¹(e_j).

noncomputable def Manifold.evalBasis {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) : (E →L[𝕜] 𝕜) →ₗ[𝕜] Fin n → 𝕜

Evaluation of functionals on the basis ψ⁻¹(e_j), an injective 𝕜-linear map (E →L[𝕜] 𝕜) → 𝕜^n.

Equations

• Manifold.evalBasis E ψ = LinearMap.pi fun (j : Fin n) => ↑((ContinuousLinearMap.apply 𝕜 𝕜) (ψ.symm (Pi.single j 1)))

theorem Manifold.evalBasis_apply {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (L : E →L[𝕜] 𝕜) (j : Fin n) : (evalBasis E ψ) L j = L (ψ.symm (Pi.single j 1))

theorem Manifold.ker_evalBasis {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) : (evalBasis E ψ).ker = ⊥

theorem Manifold.hasIndependentDifferentialsAt_iff_linearIndependent_cotangentClass' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [FiniteDimensional 𝕜 E] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {U : TopologicalSpace.Opens M} {a : M} (ha : a ∈ U) {c : ℕ} (z : Fin c → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : HasIndependentDifferentialsAt E (fun (i : Fin c) => extendSection 𝕜 E (z i)) a ↔ LinearIndependent 𝕜 fun (i : Fin c) => cotangentClass E a ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a ha)) (z i))

For sections of 𝒪_M near a, independence of the differentials at a is the linear independence over 𝕜 of their classes in 𝔪_a / 𝔪_a² ([BM97, (0.3)]; [Kol07, Definition 73]).