Charts of an analytic manifold: coordinate swaps, pullback of germs, cotangent classes

Three definitions used by the chart lemmas of Hironaka/Manifold/Chart/:

• IsCoordinateSwap e e' p Φ: Φ is the coordinate-swap isomorphism φ_p = e'⁻¹ ∘ e from the chart e to the chart e' at p — a PartialDiffeomorph of M with p in its source, source inside the source of e, target inside the source of e', and e' ∘ Φ = e on the source. Its source is Kollár's neighbourhood U(p) and its target V(p), two neighbourhoods of p which need not coincide (the automorphism φ of [Kol07, 95], realised on a neighbourhood; the coordinate change φ_{uv} of [Wlo09, Lemma 5.5.3, proof, step (0)]).
• IsPullbackStalk Φ r: r : 𝒪_{M,p} →+* 𝒪_{M,p} is the pullback g ↦ g ∘ Φ on germs at p, read through stalkToGerm.
• cotangentClass a s: the class of s − s(a) in 𝔪_a / 𝔪_a², the cotangent space of 𝒪_{M,a}, a 𝕜-module through the 𝕜-algebra structure of the stalk.

The swaps are constructed in Hironaka/Manifold/Chart/Swap.lean; the cotangent classes are compared with differentials in Hironaka/Manifold/Chart/Cotangent.lean.

def Manifold.IsCoordinateSwap {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (e e' : OpenPartialHomeomorph M E) (p : M) (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤) : Prop

Φ is the coordinate-swap isomorphism from the chart e to the chart e' at p — an analytic isomorphism between two neighbourhoods U(p) = Φ.source ⊆ e.source and V(p) = Φ.target ⊆ e'.source of p with e' ∘ Φ = e on U(p), i.e. Φ = e'⁻¹ ∘ e (the automorphism of [Kol07, 95]; the coordinate change of [Wlo09, Lemma 5.5.3, proof, step (0)]).

Equations

• Manifold.IsCoordinateSwap E M e e' p Φ = (p ∈ Φ.source ∧ Φ.source ⊆ e.source ∧ Φ.target ⊆ e'.source ∧ ∀ x ∈ Φ.source, ↑e' (↑Φ.toPartialEquiv x) = ↑e x)

def Manifold.IsPullbackStalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (Φ : M → M) {p : M} (r : ↑((structureSheaf 𝕜 E M).presheaf.stalk p) →+* ↑((structureSheaf 𝕜 E M).presheaf.stalk p)) : Prop

r : 𝒪_{M,p} →+* 𝒪_{M,p} is the pullback of germs along a map Φ with Φ p = p (continuous at p): the germ of g goes to the germ of g ∘ Φ, read through stalkToGerm.

Equations

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

noncomputable def Manifold.cotangentClass {𝕜 : 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)) : (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)).Cotangent

The class of s − s(a) in the cotangent space 𝔪_a / 𝔪_a² of the stalk at a.

Equations

• Manifold.cotangentClass E a s = (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)).toCotangent ⟨s - (Manifold.const 𝕜 E M a) ((Manifold.eval 𝕜 E M a) s), ⋯⟩