Kernels of pulled-back smooth two-forms #
If the derivative of a smooth map is surjective, the kernel of a pulled-back two-form is the
preimage of the original kernel under that derivative
(TauCeti.SmoothTwoForm.ker_bilinFormAt_mpullback). This identity supports the nondegeneracy
criterion for descended symplectic forms.
theorem
TauCeti.SmoothTwoForm.ker_bilinFormAt_mpullback
{E : Type u_1}
{H : Type u_2}
{Z : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{Q : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace Z]
[ChartedSpace H Z]
[IsManifold I (↑⊤) Z]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
[TopologicalSpace Q]
[ChartedSpace H' Q]
[IsManifold J (↑⊤) Q]
{p : Z → Q}
(hp : ContMDiff I J (↑⊤) p)
(η : SmoothTwoForm J Q)
{z : Z}
(hdp : Function.Surjective ⇑(mfderiv% p z))
:
LinearMap.ker (((SmoothForm.mpullback p hp) η).bilinFormAt z) = Submodule.comap (↑(mfderiv% p z)) (LinearMap.ker (SmoothForm.bilinFormAt η (p z)))
If the derivative of p at z is surjective, the null space of the pullback p^* η at z
is the preimage under dp_z of the null space of η at p z.