Universe constraint problem in defining tensor bundles

Stream: new members

[Yuan Liao]

Hi I am new to here so hope my question make sense. I am trying to define tensor bundles based on Hom bundle and Tangent bundle in mathlib, and here is the code.

import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Topology.VectorBundle.Hom
import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

open Bundle

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {H M : Type*} [TopologicalSpace H] [TopologicalSpace M]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable (I : ModelWithCorners 𝕜 E H)
          [ChartedSpace H M]


abbrev TM (x : M) := TangentSpace I x          -- TₓM
abbrev Tstar (x : M) := TM I x →L[𝕜] 𝕜         -- Tₓ* M  (continuous dual)

abbrev Tensor11 (x : M) := TM I x →L[𝕜] TM I x

def TensorType : ℕ → ℕ → (M → Type _)
| 0,     0     => fun _ => 𝕜
| r,     s+1   => fun x => Tstar I x →L[𝕜] TensorType r s x
| r+1,   s     => fun x => TM I x    →L[𝕜] TensorType r s x

The info I got is that in the recusive definition, there is a error of "failed to solve universe constraint," I am wondering if anyone could put some light on this? Thanks!

[Aaron Liu]

𝕜 has type Type u_1 but Tstar I x →L[𝕜] 𝕜 has type Type (max u_1 u_4)

[Aaron Liu]

these don't match so you get a problem

[Aaron Liu]

maybe there's a way to do this not recursively

[Aaron Liu]

maybe instead of using recursion you can figure something out with docs#ContinuousMultilinearMap

[Yuan Liao]

Aaron Liu said:

maybe instead of using recursion you can figure something out with docs#ContinuousMultilinearMap

Thanks for that! It seems at least I can do similiar implementations, hopefully that would work out. Thanks again!