strange deterministic timeout

Stream: new members

[Amelia Livingston]

Hello. I am confused: if you uncomment both commented out proofs at once, you get deterministic timeout, but uncommenting either one on its own is fine. I've tried increasing the timeout and it didn't help. I tried factoring out the lemmas, and it didn't help, though I got different errors. Thanks in advance.

import linear_algebra.tensor_product linear_algebra.multilinear

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
  ℕ → Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := ⟨R, ⟨by apply_instance, by apply_instance⟩⟩
| (n+1) := ⟨@tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, ⟨by apply_instance, by apply_instance⟩⟩

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
add_comm_monoid (tpow_aux R M n).1 := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
semimodule R (tpow_aux R M n).1 := (tpow_aux R M n).2.2

@[reducible] def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :=
(tpow_aux R M n).1

def tpow_lift (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M]
  [semimodule R M] : Π (n : ℕ) (P : Type*) {h1 : add_comm_monoid P}, by exactI Π
  {h2 : semimodule R P}, by exactI
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R]
  tpow R M n →ₗ[R] P
| 0 P h1 h2 :=
{ to_fun := λ g, @linear_map.to_span_singleton R P _ h1 h2 $ g (default (fin 0 → M)),
  map_add' := sorry,
  map_smul' := sorry}
| (n + 1) P h1 h2 :=
{ to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ h1 _ _ h2 $
  { to_fun := λ m, tpow_lift n P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
    map_add' := sorry, -- λ x y, by {rw linear_map.map_add, exact (tpow_lift n P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
    map_smul' := sorry, -- λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
      },
  map_add' := sorry,
  map_smul' := sorry, }

[Johan Commelin]

this is scary and annoying. I'm sorry that I can't be more helpful

[Kenny Lau]

which branch is this from? I get this error:

type mismatch at application
  multilinear_map.curry_left
term
  h1
has type
  add_comm_monoid P : Type ?
but is expected to have type
  add_comm_group ?m_1 : Type ?

[Amelia Livingston]

oh whoops - I tried to test that it works on normal mathlib but I must have messed up. I'll make a new mwe

[Amelia Livingston]

okay, this should work

import linear_algebra.tensor_product linear_algebra.multilinear

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
  ℕ → Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := ⟨R, ⟨by apply_instance, by apply_instance⟩⟩
| (n+1) := ⟨@tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, ⟨by apply_instance, by apply_instance⟩⟩

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
add_comm_monoid (tpow_aux R M n).1 := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
semimodule R (tpow_aux R M n).1 := (tpow_aux R M n).2.2

@[reducible] def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :=
(tpow_aux R M n).1

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M]
  [module R M] : Π (n : ℕ) (P : Type*) {h1 : add_comm_group P}, by exactI Π
  {h2 : semimodule R P}, by exactI
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R] tpow R M n →ₗ[R] P
| 0 P h1 h2 :=
{ to_fun := λ g, @linear_map.to_span_singleton R P _ (@add_comm_group.to_add_comm_monoid P h1) h2 $ g (default (fin 0 → M)),
  map_add' := sorry,
  map_smul' := sorry}
| (n + 1) P h1 h2 :=
{ to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ (@add_comm_group.to_add_comm_monoid P h1) _ _ h2 $
  { to_fun := λ m, tpow_lift n P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
    map_add' := sorry, -- λ x y, by {rw linear_map.map_add, exact (tpow_lift n P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
    map_smul' := sorry, -- λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
      },
  map_add' := sorry,
  map_smul' := sorry, }

[Floris van Doorn]

In the last example I get an deterministic timeout if I uncomment map_add', even when not uncommenting map_smul'.

Would tactic mode work for you? I think that is a little more robust for complicated elaboration problems. This works for me:

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M]
  [module R M] (n : ℕ) (P : Type*) {h1 : add_comm_group P} {h2 : semimodule R P} :
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R] tpow R M n →ₗ[R] P :=
begin
  unfreezingI { induction n with n ih generalizing P h1 h2 },
  { exact { to_fun := λ g, @linear_map.to_span_singleton R P _ (@add_comm_group.to_add_comm_monoid P h1) h2 $ g (default (fin 0 → M)),
      map_add' := sorry,
      map_smul' := sorry} },
  { exact { to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ (@add_comm_group.to_add_comm_monoid P h1) _ _ h2 $
    { to_fun := λ m, ih P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
      map_add' := λ x y, by {rw linear_map.map_add, exact (ih P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
      map_smul' := λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
        },
    map_add' := sorry,
    map_smul' := sorry, } }
end

[Amelia Livingston]

thank you so much! Tactic mode works for me too, I'll keep that in mind.

[Kenny Lau]

import linear_algebra.tensor_product linear_algebra.multilinear

open_locale tensor_product

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
  ℕ → Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := ⟨R, ⟨by apply_instance, by apply_instance⟩⟩
| (n+1) := ⟨@tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, ⟨by apply_instance, by apply_instance⟩⟩

def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :=
(tpow_aux R M n).1

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
add_comm_monoid (tpow R M n) := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
semimodule R (tpow R M n) := (tpow_aux R M n).2.2

def tpow_zero (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] :
  tpow R M 0 ≃ₗ[R] R :=
{ to_fun := id,
  inv_fun := id,
  map_add' := λ _ _, rfl,
  map_smul' := λ _ _, rfl,
  left_inv := λ _, rfl,
  right_inv := λ _, rfl }

def tpow_succ (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ℕ) :
  tpow R M (n+1) ≃ₗ[R] M ⊗[R] tpow R M n :=
{ to_fun := id,
  inv_fun := id,
  map_add' := λ _ _, rfl,
  map_smul' := λ _ _, rfl,
  left_inv := λ _, rfl,
  right_inv := λ _, rfl }

local attribute [irreducible] tpow

open multilinear_map

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M] [module R M]
  (P : Type*) [add_comm_group P] [module R P]
  (n : ℕ) : multilinear_map R (λ _ : fin n, M) P →ₗ[R] tpow R M n →ₗ[R] P :=
nat.rec_on n
  { to_fun := λ g, linear_map.comp
        (linear_map.to_span_singleton R P $ g $ λ i, 0)
        (tpow_zero R M : tpow R M 0 →ₗ[R] R),
      map_add' := λ g₁ g₂, linear_map.ext $ λ r, smul_add _ _ _,
      map_smul' := λ r g, linear_map.ext $ λ r', smul_comm _ _ _ } $
λ n ih, { to_fun := λ g, linear_map.comp
      (tensor_product.lift.equiv _ _ _ _ $ ih.comp $
        (multilinear_curry_left_equiv _ _ _).symm g)
      (tpow_succ R M n : tpow R M (n+1) →ₗ[R] M ⊗[R] tpow R M n),
    map_add' := λ g₁ g₂, by simp only [linear_map.map_add, linear_equiv.map_add,
        linear_map.comp_add, linear_map.add_comp],
    map_smul' := λ r g₁, by simp only [linear_map.map_smul, linear_equiv.map_smul,
        linear_map.comp_smul, linear_map.smul_comp] }

[Kenny Lau]

it also helps to make things irreducible and use nat.rec_on instead of the equation compiler I think

[Kenny Lau]

(using by exact at the beginning would also speed up the code a lot, but I did not use it here as a proof of concept)

[Kevin Buzzard]

Kenny Lau said:

(using by exact at the beginning would also speed up the code a lot

Why?

[Kenny Lau]

I have no idea

[Kenny Lau]

to me it feels like (completely unverified claim) that tactics can store intermediate terms so that you don't produce a large term at once

[Amelia Livingston]

thank you very much Kenny!

[Eric Wieser]

The sigma type in tpow_aux is a clever way to avoid the difficulty I had when trying to define the tensor power and its typeclass instances at the same time with mutual def - thanks for the inspiration!

[Frédéric Dupuis]

@Amelia Livingston @Eric Wieser Are either of you planning to PR material on tensor powers? I'm also interested in this, in fact I was planning to write code for the tensor product of a set of states indexed by a type ι , so basically what would be denoted by ⨂ i : ι, f i with f : ι → Type*. This would be a bit more general than tensor powers, which we could recover by choosing fin n as ι and f a constant function.

[Kevin Buzzard]

What is the type of ⨂ i : ι, f i?

[Kevin Buzzard]

Amelia is working on another model for the free R-algebra on an R-module because she found the current one hard to work with, even with the universal property.

[Frédéric Dupuis]

I was planning to just copy the approach in tensor_product, so free_add_monoid (Π i, f i) quotiented by the appropriate equivalence relation.

[Kevin Buzzard]

I don't know how to do infinite tensor products. What is the appropriate equivalence relation? I have only ever seen restricted infinite tensor products which have some finiteness assumptions on them.

[Frédéric Dupuis]

I would be OK with a finiteness assumption.

[Kevin Buzzard]

You mean you're assuming iota is a fintype?

[Kevin Buzzard]

In that case I'm happy.

[Frédéric Dupuis]

Yes.

[Frédéric Dupuis]

Does the tensor power only approach not have this restriction?

[Kevin Buzzard]

Amelia is taking finite tensor powers of a fixed R-module M

[Kevin Buzzard]

but indexed by fin n and so now she's in fin hell, dealing with bijections fin a \coprod fin b -> fin (a + b)

[Kevin Buzzard]

although she has actually made a lot of progress recently -- I'm meeting her tomorrow and will get an update.

[Frédéric Dupuis]

Oh dear.

[Frédéric Dupuis]

In any case, it would be nice to coordinate on this.

[Kevin Buzzard]

While I'm here, the way I have seen infinite tensor products done is that you have a bunch of modules $M_i$ and fixed vectors $m_i\in M_i$ for all but finitely many $i$ and then the restricted infinite tensor product of the $M_i$ is generated by terms $\otimes_i n_i$ subject to the condition that $n_i=m_i$ for all but finitely many $i$. It's how you make a representation of the adelic group $G(\mathbb{A}_F)$ from representations of the local groups $G(F_v)$ for $v$ running the though the places of the global field $F$. The $m_i$ are unramified vectors.