Exterior.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ArnoldCounterexample.Forms.pairForm line 23
Source documentation
The alternating product of a bilinear form and an n-form, with an integer normalization convenient for the six-dimensional obstruction.
```
def pairForm {n : ℕ} (B : E →L[ℝ] E →L[ℝ] ℝ)
    (η : E [⋀^Fin n]→L[ℝ] ℝ) : E [⋀^Fin (n + 2)]→L[ℝ] ℝ :=
…
```
lemma OAI.ArnoldCounterexample.Forms.pairForm_apply line 28

lemma OAI.ArnoldCounterexample.Forms.pairForm_radical line 39

Source documentation

If all contractions of each factor vanish in a direction, so does their alternating product. Restricting to the unit-sphere tangent gives basicness.

lemma pairForm_radical {n : ℕ} (B : E →L[ℝ] E →L[ℝ] ℝ)
    (η : E [⋀^Fin (n + 1)]→L[ℝ] ℝ) (u : E)
    (hleft : ∀ v, B u v = 0) (hright : ∀ v, B v u = 0)
    (hη : ∀ v : Fin n → E, η (Matrix.vecCons u v) = 0)
    (v : Fin (n + 2) → E) :
    pairForm B η (Matrix.vecCons u v) = 0 := by
…

Mentions: OAI.ArnoldCounterexample.Forms.pairForm

lemma OAI.ArnoldCounterexample.Forms.pairForm_pullback line 65
def OAI.ArnoldCounterexample.Forms.squareForm line 74
def OAI.ArnoldCounterexample.Forms.cubeForm line 77
lemma OAI.ArnoldCounterexample.Forms.cubeForm_pullback line 80
lemma OAI.ArnoldCounterexample.Forms.cubeForm_radical line 91
lemma OAI.ArnoldCounterexample.Forms.cubeForm_radical_on line 102
Source documentation
The third symplectic power vanishes when one input lies in the radical of the bilinear form on the span of all six inputs.
```
lemma cubeForm_radical_on (B : E →L[ℝ] E →L[ℝ] ℝ)
    (hskew : ∀ u v, B u v = - B v u) (u : E) (v : Fin 5 → E)
    (horth : ∀ i, B u (v i) = 0) : cubeForm B (Matrix.vecCons u v) = 0 := by
…
```
Mentions: OAI.ArnoldCounterexample.Forms.cubeForm
lemma OAI.ArnoldCounterexample.Forms.squareForm_apply line 124