## Stream: new members

### Topic: strange deterministic timeout

#### Amelia Livingston (Nov 24 2020 at 23:52):

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_smul' := sorry, }


#### Johan Commelin (Nov 25 2020 at 05:15):

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

#### Kenny Lau (Nov 25 2020 at 05:22):

which branch is this from? I get this error:

type mismatch at application
multilinear_map.curry_left
term
h1
has type
but is expected to have type


#### Amelia Livingston (Nov 25 2020 at 15:51):

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 (Nov 25 2020 at 16:07):

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_smul' := sorry, }


#### Floris van Doorn (Nov 25 2020 at 17:51):

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_smul' := sorry, } }
end


#### Amelia Livingston (Nov 25 2020 at 21:05):

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

#### Kenny Lau (Nov 25 2020 at 21:47):

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_smul' := λ r g₁, by simp only [linear_map.map_smul, linear_equiv.map_smul,
linear_map.comp_smul, linear_map.smul_comp] }


#### Kenny Lau (Nov 25 2020 at 21:47):

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

#### Kenny Lau (Nov 25 2020 at 21:48):

(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 (Nov 25 2020 at 21:49):

Kenny Lau said:

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

Why?

I have no idea

#### Kenny Lau (Nov 25 2020 at 22:14):

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 (Nov 25 2020 at 22:19):

thank you very much Kenny!

#### Eric Wieser (Nov 25 2020 at 23:08):

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 (Nov 25 2020 at 23:47):

@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 (Nov 25 2020 at 23:49):

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

#### Kevin Buzzard (Nov 25 2020 at 23:50):

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 (Nov 25 2020 at 23:50):

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 (Nov 25 2020 at 23:52):

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 (Nov 25 2020 at 23:52):

I would be OK with a finiteness assumption.

#### Kevin Buzzard (Nov 25 2020 at 23:53):

You mean you're assuming iota is a fintype?

#### Kevin Buzzard (Nov 25 2020 at 23:53):

In that case I'm happy.

Yes.

#### Frédéric Dupuis (Nov 25 2020 at 23:54):

Does the tensor power only approach not have this restriction?

#### Kevin Buzzard (Nov 25 2020 at 23:54):

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

#### Kevin Buzzard (Nov 25 2020 at 23:55):

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 (Nov 25 2020 at 23:56):

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

Oh dear.

#### Frédéric Dupuis (Nov 25 2020 at 23:58):

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

#### Kevin Buzzard (Nov 26 2020 at 00:02):

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.

Last updated: May 09 2021 at 19:11 UTC