Structure that recurses(?)

Stream: Is there code for X?

[The Leanest]

I want to do something like this:

structure inner_and_tensor_products (𝕜 : Type u_4) (E : Type u_5) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [has_tensor_product E] :
    Type (max u_4 u_5)

where has_tensor_product is some structure I haven't defined yet. The goal is to be able to, given the appropriate inner product and tensor product, be able to define a natural inner product on E ⊗ E, associativity axioms for ⊗, etc. Of course this runs into an inherent problem with E ⊗ E being a different, larger type than E, so how do I do this?

[Heather Macbeth]

@The Leanest Are you sure that's what you want? Why not

instance (𝕜 : Type*) (E : Type*) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :
    inner_product_space 𝕜 (E ⊗ E) :=
sorry

[The Leanest]

@Heather Macbeth Simply put, because I want this to work for arbitrary tensor products as long as it satisfies certain axioms.

[The Leanest]

Same as how inner_product_space doesn't demand the inner product based on the L2 norm be the one you use

[Kyle Miller]

Can you alter the definition of has_tensor_product, perhaps by splitting it up into a couple typeclasses, so that it can be defined before inner_and_tensor_products?

It can be useful having two sorts of typeclasses: ones that give the raw data of something, with few or no associated properties (for example, has_add), and ones that add additional properties to these.

Of course this runs into an inherent problem with E ⊗ E being a different, larger type than E, so how do I do this?

I'm not sure I follow -- are you putting the data of how to form tensor products into a structure for E itself? Could you give an #mwe for what you're observing?

[The Leanest]

@Kyle Miller By "some structure I haven't defined yet" I don't mean that it will be defined later in the file but rather that I haven't written it yet, as one basic axiom a tensor product should satisfy is associativity. Since that, at least to my knowledge, inherently requires the feature I'm requesting, I cannot write the structure until I know how to do this.

[Kyle Miller]

Is the problem you're trying to solve that you want strict associativity? I'm still not sure what you're going for -- even a minimal nonworking example using the feature that you wish were there might be helpful.

[Kyle Miller]

If it's about strict associativity, here's an example for making a strictly associative cartesian product. The main idea is that you create a new type that represents abstract products, and you only turn it into a type when you need it. (It uses typeclass and coercion trickery to make it appear seamless. Don't know how it holds up in practice.)

universes u v w

inductive strict_prod (α : Type u)
| one : strict_prod
| left_prod : strict_prod → strict_prod

namespace strict_prod

def prod {α : Type u} : strict_prod α → strict_prod α → strict_prod α
| one p := left_prod p
| (left_prod p) q := left_prod (p.prod q)

def to_type {α : Type u} : strict_prod α → Type u
| one := α
| (left_prod p) := α × p.to_type

instance {α : Type u} : has_coe_to_sort (strict_prod α) (Type u) :=
⟨to_type⟩

end strict_prod

class has_strict_prod {α : Type u} (x : α) (β : out_param (Type v)) :=
(prod : strict_prod β)

variables {α β γ : Type*}

@[priority 0]
instance strict_prod_lift : has_strict_prod α α :=
⟨strict_prod.one⟩

instance strict_prod_keep (p : (strict_prod α)) : has_strict_prod p α :=
⟨p⟩

def mk_strict_prod (p : β) (q : γ) {α : Type*} [has_strict_prod p α] [has_strict_prod q α] :
  strict_prod α :=
(has_strict_prod.prod p).prod (has_strict_prod.prod q)

infixr ` ×' `:35 := mk_strict_prod

example {α : Type*} (x : α ×' (α ×' α)) : (α ×' α) ×' α := x

example {α : Type*} (x : α × (α × α)) : (α × α) × α := x
/-
27:56: type mismatch, term
  x
has type
  α × α × α
but is expected to have type
  (α × α) × α
-/

[The Leanest]

Kyle Miller said:

If it's about strict associativity, here's an example for making a strictly associative cartesian product. The main idea is that you create a new type that represents abstract products, and you only turn it into a type when you need it. (It uses typeclass and coercion trickery to make it appear seamless. Don't know how it holds up in practice.)

Thank you! I'll look into this!