class HasTangentSpaces (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type (max (max (max u_1 u_2) (u_3 + 1)) (u_4 + 1))

Typeclass packaging a manifold $M$ with a pointwise tangent space $T_x M$ and the bridge between abstract $2$-forms in Ω 2 and their pointwise bilinear evaluations $\Omega_x$; also records how an almost complex structure lifts to vector fields and interacts with symplectic forms (compatibility, taming, $J^2 = -\mathrm{id}$).

• M : Type u_3
• TangentSpaceAt : M Ω VF → Type u_4
• instACG (x : M Ω VF) : AddCommGroup (TangentSpaceAt x)
• instMod (x : M Ω VF) : Module ℝ (TangentSpaceAt x)
• instFD (x : M Ω VF) : FiniteDimensional ℝ (TangentSpaceAt x)
• eval₂ (x : M Ω VF) : Ω 2 → LinearMap.BilinForm ℝ (TangentSpaceAt x)
• eval₂_add (x : M Ω VF) (α β : Ω 2) : eval₂ x (α + β) = eval₂ x α + eval₂ x β
• eval₂_smul (x : M Ω VF) (r : ℝ) (α : Ω 2) : eval₂ x (r • α) = r • eval₂ x α
• eval_is_symplectic (S : SymplecticManifold Ω VF) (x : M Ω VF) : SymplecticLinearAlgebra.IsSymplecticForm (eval₂ x S.ω)
• liftJ : ((x : M Ω VF) → TangentSpaceAt x →ₗ[ℝ] TangentSpaceAt x) → VF → VF
• lift_sq_neg (Jfam : (x : M Ω VF) → TangentSpaceAt x →ₗ[ℝ] TangentSpaceAt x) : (∀ (x : M Ω VF), SymplecticLinearAlgebra.IsComplexStructure (Jfam x)) → ∀ (X : VF) (α : Ω 1), DifferentialFormSpace.ι (liftJ Jfam (liftJ Jfam X)) α = -DifferentialFormSpace.ι X α
• lift_preserves (S : SymplecticManifold Ω VF) (Jfam : (x : M Ω VF) → TangentSpaceAt x →ₗ[ℝ] TangentSpaceAt x) : (∀ (x : M Ω VF) (u v : TangentSpaceAt x), ((eval₂ x S.ω) ((Jfam x) u)) ((Jfam x) v) = ((eval₂ x S.ω) u) v) → ∀ (u v : VF), DifferentialFormSpace.ι (liftJ Jfam u) (DifferentialFormSpace.ι (liftJ Jfam v) S.ω) = DifferentialFormSpace.ι u (DifferentialFormSpace.ι v S.ω)
• lift_taming (S : SymplecticManifold Ω VF) (Jfam : (x : M Ω VF) → TangentSpaceAt x →ₗ[ℝ] TangentSpaceAt x) : (∀ (x : M Ω VF) (v : TangentSpaceAt x), v ≠ 0 → ((eval₂ x S.ω) v) ((Jfam x) v) > 0) → Function.Injective fun (v : VF) => DifferentialFormSpace.ι (liftJ Jfam v) S.ω