The linear map $V \to E^*$ sending $v \mapsto (e \mapsto \Omega(v, e))$, where $\Omega$ is a bilinear form on $V$ and $E \subseteq V$ a subspace.
Instances For
The kernel of symplecticToDual Ω E is the symplectic orthogonal complement
$E^{\perp_\Omega} = \{v \in V : \Omega(v, e) = 0 \text{ for all } e \in E\}$.
A Lagrangian subspace $E$ is contained in the kernel of symplecticToDual Ω E,
since $E = E^{\perp_\Omega}$.
For $E \subseteq V$ Lagrangian, the descent of symplecticToDual Ω E to
a linear map $V/E \to E^*$ given by $[v] \mapsto \Omega(v, \cdot)|_E$.
Instances For
The induced map $V/E \to E^*$ is injective for $E$ Lagrangian, because the kernel of the original map is exactly $E^{\perp_\Omega} = E$.
For $E$ a Lagrangian subspace, $\dim(V/E) = \dim E^* = \dim E$, since $\dim E = \tfrac12 \dim V$.
Linear Lagrangian normal bundle identification. For $E$ a Lagrangian subspace of a symplectic vector space $(V, \Omega)$, there is a natural linear isomorphism $V/E \xrightarrow{\sim} E^*$, identifying the "normal space" to $E$ with $T^*E$.
Instances For
Surjectivity on cohomology from a retraction. If $\pi : U \to X$ is a retraction of $i : X \hookrightarrow U$ (so $i^* \pi^* = \mathrm{id}$), then $i^*$ is surjective on all forms: every $\alpha \in \Omega^p(X)$ lifts to $\beta = \pi^*\alpha \in \Omega^p(U)$ with $i^*\beta = \alpha$.
A relative homotopy operator for an inclusion $i : X \hookrightarrow U$ packages the chain-level data showing that $i^*$ is a homotopy equivalence: a retraction $\pi : U \to X$, a chain homotopy $K : \Omega^{p+1}(U) \to \Omega^p(U)$ satisfying $dK + Kd = \mathrm{id} - \pi^* i^*$, and the additional condition $i^* K = 0$ (so that primitives vanish on $X$).
- π : DFSMorphism Ω VF Ω_X VF_X
Instances For
Cartan's magic formula applied to a chosen "scaling" vector field $V$: $d\iota_V \beta + \iota_V d\beta = \mathcal{L}_V \beta$.
Derivation of the chain homotopy formula $dK + Kd = \mathrm{id} - \pi^* i^*$ from Cartan's formula together with a "fundamental theorem of calculus" identity $\Phi(\mathcal{L}_V \beta) = \beta - \pi^*(i^*\beta)$, where $K := \Phi \circ \iota_V$.
$\mathbb{R}$-linearity of $K = \Phi \circ \iota_V$ in its argument, derived from the linearity of $\iota_V$ and the scalar-multiplicativity of $\Phi$.
$K\beta = \Phi(\iota_V \beta)$ pulls back to zero on $X$, since $\iota_V$ already does and $\Phi$ preserves vanishing on $X$.
Tubular homotopy primitives for an inclusion $i : X \hookrightarrow U$: the data of a retraction $\pi$, an Euler-like vector field $V$, and a "radial integration" operator $\Phi$ satisfying additivity, scalar-multiplicativity, commutation with $d$, an "FTC" identity $\Phi(\mathcal{L}_V \beta) = \beta - \pi^* i^*\beta$, and the conditions $i^*(\iota_V \beta) = 0$ and $i^* \Phi = i^*$.
Such primitives canonically produce a relative homotopy operator via $K := \Phi \circ \iota_V$.
- π : DFSMorphism Ω VF Ω_X VF_X
- V : VF
- Φ {p : ℕ} : Ω p → Ω p
- Φ_d {p : ℕ} (γ : Ω p) : DifferentialFormSpace.d VF (self.Φ γ) = self.Φ (DifferentialFormSpace.d VF γ)
Instances For
If $i^*\gamma = 0$ and $\Phi$ fixes pullbacks to $X$, then $i^*(\Phi \gamma) = 0$.
Construct a HasRelativeHomotopyOperator from the more granular tubular
homotopy primitives, via $K := \Phi \circ \iota_V$.
Instances For
Relative Poincaré lemma. Given a relative homotopy operator for $i : X \hookrightarrow U$, every closed $(\ell+1)$-form $\beta \in \Omega^{\ell+1}(U)$ whose pullback $i^*\beta = 0$ vanishes admits a primitive $\mu \in \Omega^\ell(U)$ with $d\mu = \beta$ and $i^*\mu = 0$.
Variant of the relative Poincaré lemma stated directly in terms of
HasTubularHomotopyPrimitives: the explicit primitive is $\mu = \Phi(\iota_V \beta)$.
An algebraic deformation retract of $U$ onto $X$: a relative homotopy operator together with an injectivity condition at degree 0 (forms of degree 0 with vanishing differential and vanishing pullback are zero).
- π : DFSMorphism Ω_U VF_U Ω_X VF_X
- deg0_injectivity (β : Ω_U 0) : DifferentialFormSpace.d VF_U β = 0 → i.pullback β = 0 → β = 0
Instances For
Relative Poincaré lemma packaged for the HasDeformationRetract interface.
Injectivity on cohomology from a deformation retract. If $\beta \in \Omega^{p+1}(U)$ is closed and its restriction $i^*\beta$ is exact on $X$ (i.e. $i^*\beta = d\gamma$), then $\beta$ itself is exact on $U$.
Cohomology isomorphism. A deformation retract of $U_1$ onto $X$ gives the three algebraic statements together asserting that $i^* : H^*(U_1, \mathbb{R}) \to H^*(X, \mathbb{R})$ is an isomorphism: surjectivity on forms, injectivity on cohomology in positive degree, and injectivity in degree $0$.
Abstract data for the normal bundle $NX \to X$ at the level of differential forms: a zero-section morphism $X \to NX$ and a projection $NX \to X$ whose composition pulled back to forms is the identity on $\Omega^*(X)$.
- zeroSection : DFSMorphism Ω_X VF_X Ω_NX VF_NX
- projection : DFSMorphism Ω_NX VF_NX Ω_X VF_X
Instances For
Predicate that the DFS morphism $i : X \hookrightarrow M$ comes from a smooth submanifold inclusion of dimensions $\dim X \le \dim M$.
Instances For
Compatibility predicate stating that $U \subseteq N$ is an open neighborhood of $X \subseteq N$: the inclusion $X \hookrightarrow N$ factors as $X \hookrightarrow U \hookrightarrow N$ on differential forms.
Instances For
A pair of DFS morphisms $\varphi, \varphi^{-1}$ form a DFS diffeomorphism if their pullbacks are mutually inverse on all differential forms.
Instances For
The data of an exponential map used in proving the tubular neighborhood theorem: an open neighborhood $U_0$ of $X$ in $NX$ together with a smooth map $\exp : U_0 \to M$ whose restriction to the zero section is $i : X \hookrightarrow M$.
- VF_U₀ : Type u_8
- inst_U₀ : DifferentialFormSpace (Ω_U₀ nb hSubmfd) (VF_U₀ nb hSubmfd)
- exp_map : DFSMorphism (Ω_U₀ nb hSubmfd) (VF_U₀ nb hSubmfd) Ω_M VF_M
- j₀ : DFSMorphism (Ω_U₀ nb hSubmfd) (VF_U₀ nb hSubmfd) Ω_NX VF_NX
- s₀ : DFSMorphism Ω_X VF_X (Ω_U₀ nb hSubmfd) (VF_U₀ nb hSubmfd)
- hU₀_nbhd : IsOpenNeighborhoodOf nb.zeroSection j₀ s₀
Instances
The output of the inverse function theorem applied to the exponential map: a DFS-diffeomorphism $\varphi : U_0 \xrightarrow{\sim} U_1$ where $U_1 \subseteq M$, together with the factorization $\exp = \mathrm{incl}_{U_1 \hookrightarrow M} \circ \varphi$.
- VF_U₁ : Type u_10
- inst_U₁ : DifferentialFormSpace (Ω_U₁ hU₀_nbhd hd_exp_id) (VF_U₁ hU₀_nbhd hd_exp_id)
- φ : DFSMorphism Ω_U₀ VF_U₀ (Ω_U₁ hU₀_nbhd hd_exp_id) (VF_U₁ hU₀_nbhd hd_exp_id)
- φ_inv : DFSMorphism (Ω_U₁ hU₀_nbhd hd_exp_id) (VF_U₁ hU₀_nbhd hd_exp_id) Ω_U₀ VF_U₀
- incl_U₁_M : DFSMorphism (Ω_U₁ hU₀_nbhd hd_exp_id) (VF_U₁ hU₀_nbhd hd_exp_id) Ω_M VF_M
- hDiffeo : IsDFSDiffeomorphism φ φ_inv
Instances
Packaging of the conclusion of the tubular neighborhood theorem: open neighborhoods $U_0$ of $X$ in $NX$ and $U_1$ of $X$ in $M$, a DFS-diffeomorphism $\varphi : U_0 \xrightarrow{\sim} U_1$ that restricts to the identity on $X$, together with the relevant inclusions and the open-neighborhood data on both sides.
- VF_U₀ : Type u_8
- inst_U₀ : DifferentialFormSpace self.Ω_U₀ self.VF_U₀
- VF_U₁ : Type u_10
- inst_U₁ : DifferentialFormSpace self.Ω_U₁ self.VF_U₁
- φ : DFSMorphism self.Ω_U₀ self.VF_U₀ self.Ω_U₁ self.VF_U₁
- φ_inv : DFSMorphism self.Ω_U₁ self.VF_U₁ self.Ω_U₀ self.VF_U₀
- j₀ : DFSMorphism self.Ω_U₀ self.VF_U₀ Ω_NX VF_NX
- s₀ : DFSMorphism Ω_X VF_X self.Ω_U₀ self.VF_U₀
- j₁ : DFSMorphism Ω_X VF_X self.Ω_U₁ self.VF_U₁
- incl_U₁_M : DFSMorphism self.Ω_U₁ self.VF_U₁ Ω_M VF_M
- hDiffeo : IsDFSDiffeomorphism self.φ self.φ_inv
- hU₀_nbhd : IsOpenNeighborhoodOf nb.zeroSection self.j₀ self.s₀
- hU₁_nbhd : IsOpenNeighborhoodOf i self.incl_U₁_M self.j₁
Instances For
Tubular neighborhood theorem (assembly). Given an exponential map data and the output of the inverse function theorem, this assembles the full tubular neighborhood data: $X \subseteq M$ admits a tubular neighborhood $U_1 \cong U_0 \subseteq NX$.
Instances For
Existence of exponential-map data for a submanifold inclusion (axiomatic; ultimately to be supplied by Riemannian or local-coordinate methods).
Instances For
Existence of the inverse-function-theorem data from exponential-map data (axiomatic; the proof goes through the IFT applied to the differential of $\exp$ which is the identity on the zero section).
Instances For
Tubular neighborhood theorem (DFS version). For any submanifold inclusion $i : X \hookrightarrow M$ with normal-bundle data $nb$, there exist open neighborhoods $U_0$ of $X$ in $NX$ and $U_1$ of $X$ in $M$, and a DFS-diffeomorphism $\varphi : U_0 \xrightarrow{\sim} U_1$ that is the identity on $X$.
Instances For
Cartan-formula computation underlying Moser's trick: if $\omega$ is closed and $\iota_v \omega = -\mu$, then $\mathcal{L}_v \omega = -d\mu$.
Moser's cancellation identity: with $\omega$ closed, $\iota_v\omega = -\mu$, and $d\mu = \sigma$, one has $\mathcal{L}_v\omega + \sigma = 0$, the time-derivative of the family $\omega_t$ along the Moser flow.
If $\omega_0, \omega_1$ are closed 2-forms with the same pullback to $X$, then their difference $\omega_1 - \omega_0$ is closed and vanishes when pulled back to $X$.
The interpolated 2-form $\omega_t = (1-t)\omega_0 + t\omega_1$ is closed whenever both $\omega_0, \omega_1$ are.
The 2-form $\omega$ has the property that contraction $v \mapsto \iota_v \omega$ hits every 1-form — equivalently, $\omega^\flat : TM \to T^*M$ is surjective.
Instances For
If contraction with $\omega$ is surjective, the Moser equation $\iota_v \omega = -\mu$ has a solution $v$.
Local Moser theorem (algebraic core). Given closed nondegenerate 2-forms $\omega_0, \omega_1$ that agree on $X$ (in the strong sense that $i^*(\iota_V \omega_0) = i^*(\iota_V \omega_1)$ for all vector fields $V$), and given a relative homotopy operator, the surjectivity of contraction with $\omega_0$, and an ODE flow existence assumption, there exists a diffeomorphism $\varphi$ with $\varphi^*\omega_1 = \omega_0$ that is the identity on $X$.
The DFS morphism $i : U \hookrightarrow M$ comes from a proper open inclusion $U \subsetneq M$: pullback on smooth functions is not surjective.
Instances For
A global Moser flow $\varphi_M : M \to M$ matching $\omega_1$ to $\omega_0$ and fixing $X$ restricts to a local diffeomorphism between open neighborhoods $U_0, U_1$ of $X$.
Existence of the Moser ODE flow (axiomatic). Given the data of the Moser equation $\iota_v\omega_0 = -\mu$ and Cartan's cancellation $\mathcal{L}_v\omega_0 + (\omega_1-\omega_0) = 0$ with $\mu$ vanishing on $X$, the time-1 flow of $v$ yields a diffeomorphism $\varphi$ with $\varphi^*\omega_1 = \omega_0$ that is the identity on $X$.
If $\iota_V \omega_0$ and $\iota_V \omega_1$ have the same pullback to $X$ for every $V$, then $\omega_0$ and $\omega_1$ themselves have the same pullback.
A 2-form $\omega_0$ for which contraction is injective is also nondegenerate in the sense that contraction is surjective (in finite dimension; here taken axiomatically).
Axiomatic existence of tubular homotopy primitives for any submanifold inclusion $i : X \hookrightarrow U$ (universe-polymorphic version).
Instances For
Local Moser theorem (Theorem 4 in the book). For a submanifold $X \hookrightarrow M$ and two closed nondegenerate 2-forms $\omega_0, \omega_1$ on $M$ that agree to first order along $X$, there exist open neighborhoods $U_0, U_1$ of $X$ in $M$ and a diffeomorphism $\varphi : U_0 \xrightarrow{\sim} U_1$ with $\varphi^*\omega_1 = \omega_0$ and $\varphi|_X = \mathrm{id}$.
$i : X \hookrightarrow M$ is a closed submanifold inclusion: every differential form on $X$ extends to a form on $M$ (i.e. $i^* : \Omega^*(M) \to \Omega^*(X)$ is surjective).
Instances For
All the geometric data produced by combining the tubular neighborhood theorem with the Lagrangian normal-bundle identification $NX \cong T^*X$: a common neighborhood $U$ of $X$ carrying two symplectic forms $\omega_0$ (from $T^*X$) and $\omega_1$ (from $M$) that agree on $X$, together with the auxiliary inclusions and a $V$-side neighborhood diffeomorphic to $U$ identifying $\omega_1$ with the symplectic form on $M$.
- VF_U : Type u_8
- inst_U : DifferentialFormSpace self.Ω_U self.VF_U
- j : DFSMorphism Ω_X VF_X self.Ω_U self.VF_U
- ω₀ : self.Ω_U 2
- ω₁ : self.Ω_U 2
- hnd₀ : Function.Injective fun (X : self.VF_U) => DifferentialFormSpace.ι X self.ω₀
- hnd₁ : Function.Injective fun (X : self.VF_U) => DifferentialFormSpace.ι X self.ω₁
- VF_V : Type u_10
- inst_V : DifferentialFormSpace self.Ω_V self.VF_V
- ψ : DFSMorphism self.Ω_U self.VF_U self.Ω_V self.VF_V
- ψ_inv : DFSMorphism self.Ω_V self.VF_V self.Ω_U self.VF_U
- S_V : SymplecticManifold self.Ω_V self.VF_V
- j_V : DFSMorphism Ω_X VF_X self.Ω_V self.VF_V
- ι_U : DFSMorphism self.Ω_U self.VF_U Ω_TX VF_TX
- ι_V : DFSMorphism self.Ω_V self.VF_V Ω_M VF_M
Instances For
Axiomatic existence of TubularNeighborhoodGeometricData for any closed
Lagrangian submanifold $X$ of a symplectic manifold $(M, \omega)$.
Instances For
First-order agreement on $X$. A Whitney-extension argument shows that the two candidate symplectic forms $\omega_0$ and $\omega_1$ supplied by the geometric data agree on $X$ at first order, i.e. $j^*(\iota_V\omega_0) = j^*(\iota_V\omega_1)$ for every vector field $V$.
Axiomatic existence of tubular homotopy primitives for $j : X \hookrightarrow U$ (unrestricted universe version).
Instances For
Moser transport. On a single ambient $U$ containing $X$, given closed 2-forms $\omega_0, \omega_1$ with $\omega_0$ nondegenerate that agree to first order on $X$, together with a relative homotopy operator, there exists a DFS-diffeomorphism $\varphi : U \to U$ with $\varphi^*\omega_1 = \omega_0$ fixing $X$.
Typeclass-style bundle of all the Moser-transport infrastructure for an inclusion $i : X \hookrightarrow U$: tubular homotopy primitives plus an existence statement for the Moser diffeomorphism given the standard hypotheses.
- homotopyPrimitives : HasTubularHomotopyPrimitives Ω VF Ω_X VF_X i
- moserTransportData (ω₀ ω₁ : Ω 2) (hclosed₀ : DifferentialFormSpace.d VF ω₀ = 0) (hclosed₁ : DifferentialFormSpace.d VF ω₁ = 0) (hnd₀ : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ω₀) (hagree : ∀ (V : VF), i.pullback (DifferentialFormSpace.ι V ω₀) = i.pullback (DifferentialFormSpace.ι V ω₁)) (hH : HasRelativeHomotopyOperator Ω VF Ω_X VF_X i) : ∃ (φ : DFSMorphism Ω VF Ω VF) (φ_inv : DFSMorphism Ω VF Ω VF), φ.pullback ω₁ = ω₀ ∧ (∀ {p : ℕ} (α : Ω p), φ_inv.pullback (φ.pullback α) = α) ∧ (∀ {p : ℕ} (α : Ω p), φ.pullback (φ_inv.pullback α) = α) ∧ ∀ {p : ℕ} (α : Ω p), i.pullback (φ.pullback α) = i.pullback α
Instances
All the geometric and Moser-flow data needed to prove Weinstein's Lagrangian neighborhood theorem: a common neighborhood $U$ of $X$ with two symplectic forms $\omega_0$ (induced from $T^*X$) and $\omega_1$ (induced from $M$), a $V$-side neighborhood diffeomorphic to $U$ realizing $\omega_1$ as a pullback of the symplectic form on $M$, and a Moser flow $\varphi$ on $U$ matching $\omega_1$ to $\omega_0$ that fixes $X$.
- VF_U : Type u_8
- inst_U : DifferentialFormSpace (Ω_U hLag) (VF_U hLag)
- j : DFSMorphism Ω_X VF_X (Ω_U hLag) (VF_U hLag)
- ω₀ : Ω_U hLag 2
- ω₁ : Ω_U hLag 2
- hagree (V : VF_U hLag) : j.pullback (DifferentialFormSpace.ι V ω₀) = j.pullback (DifferentialFormSpace.ι V ω₁)
- hnd₀ : Function.Injective fun (X : VF_U hLag) => DifferentialFormSpace.ι X ω₀
- hnd₁ : Function.Injective fun (X : VF_U hLag) => DifferentialFormSpace.ι X ω₁
- VF_V : Type u_10
- inst_V : DifferentialFormSpace (Ω_V hLag) (VF_V hLag)
- ψ : DFSMorphism (Ω_U hLag) (VF_U hLag) (Ω_V hLag) (VF_V hLag)
- ψ_inv : DFSMorphism (Ω_V hLag) (VF_V hLag) (Ω_U hLag) (VF_U hLag)
- S_V : SymplecticManifold (Ω_V hLag) (VF_V hLag)
- j_V : DFSMorphism Ω_X VF_X (Ω_V hLag) (VF_V hLag)
- ι_U : DFSMorphism (Ω_U hLag) (VF_U hLag) Ω_TX VF_TX
- ι_V : DFSMorphism (Ω_V hLag) (VF_V hLag) Ω_M VF_M
- φ : DFSMorphism (Ω_U hLag) (VF_U hLag) (Ω_U hLag) (VF_U hLag)
- φ_inv : DFSMorphism (Ω_U hLag) (VF_U hLag) (Ω_U hLag) (VF_U hLag)
Instances
Weinstein's Lagrangian neighborhood theorem (core, from data). From a
HasLagrangianTubularData package, one constructs the symplectomorphism
$\Phi := \psi \circ \varphi$ from the local model $(U, \omega_0)$ to $(V, S_V.\omega)$
that is the identity on $X$ in the appropriate sense.
Existence of HasLagrangianTubularData: combine the geometric tubular neighborhood
data with the first-order agreement of $\omega_0$ and $\omega_1$ on $X$, then apply
the local Moser theorem to produce the required diffeomorphism $\varphi$.
Instances For
Weinstein's Lagrangian neighborhood theorem (book form). For a symplectic manifold $(M, \omega)$ and a closed Lagrangian submanifold $i : X \hookrightarrow M$, there exist a neighborhood $U_0 \subseteq T^*X$ of the zero section, a neighborhood $V \subseteq M$ of $X$, and a symplectomorphism $\Phi : (U_0, \omega_0) \to (V, \omega)$ that intertwines the inclusion of $X$ into both.
Abstract "pointwise evaluation" for 1-forms on $X$ at points of an underlying point set: a predicate "$\mu$ vanishes at $x$" used to phrase critical-point arguments.
- isZeroAt : Ω_X 1 → X → Prop
Instances For
Axiomatic vanishing of $H^1(X, \mathbb{R})$: every closed 1-form on $X$ is exact, i.e. $\mu = dh$ for some smooth $h : X \to \mathbb{R}$.
- exact_of_closed (μ : Ω_X 1) : DifferentialFormSpace.d VF_X μ = 0 → ∃ (h : Ω_X 0), μ = DifferentialFormSpace.d VF_X h
Instances For
On a compact (Hausdorff) manifold $X$, every smooth function $h : X \to \mathbb{R}$ has at least two critical points (achieving its max and min).
The data witnessing that a $C^1$-close Lagrangian deformation $Y$ of $X$ is encoded by a closed 1-form $\mu \in \Omega^1(X)$ such that $X \cap Y$ corresponds to the zero set of $\mu$ in the Weinstein chart.
- μ : Ω_X 1
Instances For
Mathlib-flavored predicate that $i : X \to M$ is a Lagrangian embedding: $i$ is smooth and injective.
- injective : Function.Injective i
Instances
Mathlib-flavored axiomatization of $H^1(X, \mathbb{R}) = 0$ on a connected manifold: any smooth function with zero differential is constant.
- connected : ConnectedSpace X
Instances
The Mathlib analog of C1CloseLagrangian: data of a smooth function
$h : X \to \mathbb{R}$ whose critical points correspond exactly to intersection points
of $X$ with a $C^1$-close submanifold $Y$.
Instances For
Combining Weinstein's theorem with $H^1(X) = 0$ produces a smooth primitive $h$ on $X$ whose critical points coincide with the intersection points of $X$ and $Y$.
A slimmer variant of C1CloseSubmanifold_mfld carrying only the smooth function $h$
on $X$ and the intersection-vs-critical-point equivalence.
Instances For
Extreme value theorem giving $\ge 2$ critical points. On a compact nontrivial manifold $X$, every smooth $h : X \to \mathbb{R}$ has at least two distinct critical points.
Lagrangian intersection theorem for $C^1$-close deformations. If $X$ is compact, $H^1(X) = 0$, and $Y$ is a $C^1$-close Lagrangian deformation of $X$ in $M$, then $X$ and $Y$ intersect in at least two distinct points.
Mathlib version of $H^1$ vanishing on a normed space $E$: every closed alternating 1-form on $E$ is the exterior derivative of an alternating 0-form.
Instances For
Mathlib-style packaging of the Weinstein tubular neighborhood: open sets $U \subseteq M$ containing $X$ and $U_0 \subseteq E \times E$ containing the zero section, with a diffeomorphism $\Phi : U_0 \xrightarrow{\sim} U$ taking the zero section into $X$ and (placeholder) preserving the symplectic structure.
- U : TopologicalSpace.Opens M
- U₀ : TopologicalSpace.Opens (E × E)
- Φ : Diffeomorph (modelWithCornersSelf ℝ (E × E)) I ↥self.U₀ ↥self.U ⊤
- hΦ_symplectic : True
Instances For
Mathlib-style packaging of the (non-symplectic) tubular neighborhood theorem: neighborhoods $U_1 \ni X$ in $M$ and $U_0 \ni$ zero section in $E \times E$, and a diffeomorphism $\varphi : U_0 \to U_1$ mapping the zero section into $X$.
- U₁ : TopologicalSpace.Opens M
- U₀ : TopologicalSpace.Opens (E × E)
- φ : Diffeomorph (modelWithCornersSelf ℝ (E × E)) I ↥self.U₀ ↥self.U₁ ⊤
Instances For
Existence of an exponential-like map in the Mathlib setting (axiomatic). For any smooth injective $i : X \to M$, there exists an open set $U_0 \subseteq E_X \times E_N$ containing the zero section and a smooth map $\exp : U_0 \to M$ such that the zero section lands in $i(X)$, $\exp$ is locally injective, and $i(X) \subseteq \mathrm{im}(\exp)$.
IFT-based local diffeomorphism (axiomatic, Mathlib version). Starting from an exponential-like map $\exp : U_0 \to M$ with the standard properties, the inverse function theorem produces a smaller diffeomorphism $\varphi : U_0 \xrightarrow{\sim} U_1$ preserving the zero section, with $U_1 \supseteq i(X)$ and $U_0$ bounded in the "normal" direction.
Tubular neighborhood theorem (Mathlib formulation). For any smooth injective
$i : X \hookrightarrow M$, there exist open neighborhoods $U_0$ of the zero section of
$E_X \times E_N$ and $U_1$ of $i(X)$ in $M$, and a diffeomorphism
$\varphi : U_0 \xrightarrow{\sim} U_1$ preserving the zero section, with the normal
factor of $U_0$ bounded. Combines expMap_exists_Mathlib and ift_localDiffeo_Mathlib.
Lightweight Mathlib structure recording the input data for the intersection
problem: a chart $X \to E$, a closed 1-form $\mu$ on $E$, and a predicate isZeroAt
on $X$ that is equivalent to $\mu$ vanishing at the chart image.
- chart : X → E
- isZeroAt : X → Prop
Instances For
Lagrangian intersection theorem (Mathlib version). Given $H^1$ vanishing on $E$, a $C^1$-close Lagrangian data $Y$, and an EVT-type hypothesis providing two distinct critical points of any function on $X$, we conclude that $X$ has at least two distinct intersection points with $Y$.