## Stream: general

### Topic: typeclass for has_coe_to_fun is slow?

#### Kenny Lau (Apr 21 2020 at 05:21):

import group_theory.quotient_group

universes u v

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A →+ A)
(j : A →+ E)
(k : E →+ A)
(hij : ∀ x : A, (j (i x) : E) = 0)
(hji : ∀ y : A, (j y : E) = 0 → ∃ x : A, (i x : A) = y)


#### Kenny Lau (Apr 21 2020 at 05:21):

I can't profiler the time for some reason

#### Kenny Lau (Apr 21 2020 at 05:22):

but has_coe_to_fun (A →+ E) takes a long time to resolve according to trace.class_instances

#### Kenny Lau (Apr 21 2020 at 05:31):

are we ready for bundled morphisms?

#### Kenny Lau (Apr 21 2020 at 05:32):

looks like I didn't do the control, because somehow this is slow also:

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A → A) --[hi : is_add_group_hom i]
(j : A → E) --[hi : is_add_group_hom i]
(k : E → A) --[hi : is_add_group_hom i]
(hij : ∀ x : A, (j (i x) : E) = 0)
(hji : ∀ y : A, (j y : E) = 0 → ∃ x : A, (i x : A) = y)
(hjk : ∀ x : A, (k (j x) : A) = 0)
(hkj : ∀ y : E, (k y : A) = 0 → ∃ x : A, (j x : E) = y)
(hki : ∀ x : E, (i (k x) : A) = 0)
(hik : ∀ y : A, (i y : A) = 0 → ∃ x : E, (k x : A) = y)


#### Kenny Lau (Apr 21 2020 at 05:33):

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_sizeof (Type u) := @add_submonoid.has_sizeof_inst ?x_1 ?x_2
failed is_def_eq
[...]
[class_instances] (0) ?x_0 : has_sizeof (∀ (x : A), k (j x) = 0) := @is_lawful_traversable.has_sizeof_inst ?x_128 ?x_129
failed is_def_eq
[class_instances] (0) ?x_0 : has_sizeof (∀ (x : A), k (j x) = 0) := traversable.has_sizeof_inst ?x_130
failed is_def_eq
[class_instances] (0) ?x_
(message too long, truncated at 262144 characters)


#### Kenny Lau (Apr 21 2020 at 05:35):

does this mean I have to move everything to the left of the colon? I've never seen this before

#### Kenny Lau (Apr 21 2020 at 05:36):

but this is still slow:

structure exact_couple (A : Type u) [add_comm_group A] (E : Type v) [add_comm_group E]
(i : A → A) --[hi : is_add_group_hom i]
(j : A → E) --[hi : is_add_group_hom i]
(k : E → A) --[hi : is_add_group_hom i]
: Prop :=
(hij : ∀ x : A, (j (i x) : E) = 0)
(hji : ∀ y : A, (j y : E) = 0 → ∃ x : A, (i x : A) = y)
(hjk : ∀ x : A, (k (j x) : A) = 0)
(hkj : ∀ y : E, (k y : A) = 0 → ∃ x : A, (j x : E) = y)
(hki : ∀ x : E, (i (k x) : A) = 0)
(hik : ∀ y : A, (i y : A) = 0 → ∃ x : E, (k x : A) = y)


what's going on?

#### Kenny Lau (Apr 21 2020 at 05:57):

Lean is so slow, this is impossible to finish:

import group_theory.quotient_group

universes u v

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A → A) [hi : is_add_group_hom i]
(j : A → E) [hj : is_add_group_hom j]
(k : E → A) [hk : is_add_group_hom k]
(hij : ∀ x : A, (j (i x) : E) = 0)
(hji : ∀ y : A, (j y : E) = 0 → ∃ x : A, (i x : A) = y)
(hjk : ∀ x : A, (k (j x) : A) = 0)
(hkj : ∀ y : E, (k y : A) = 0 → ∃ x : A, (j x : E) = y)
(hki : ∀ x : E, (i (k x) : A) = 0)
(hik : ∀ y : A, (i y : A) = 0 → ∃ x : E, (k x : A) = y)
attribute [instance] exact_couple.Ag exact_couple.Eg exact_couple.hi exact_couple.hj exact_couple.hk

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
{ y | ∃ x : C.E, C.j (C.k x) = y.1 }
{ add_mem := by rintros ⟨_, h1⟩ ⟨_, h2⟩ ⟨x1, h3⟩ ⟨x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
neg_mem := by rintros ⟨_, h⟩ ⟨x, H⟩; dsimp only at H; subst H; use -x;


#### Kenny Lau (Apr 21 2020 at 05:57):

practically impossible

#### Kevin Buzzard (Apr 22 2020 at 11:37):

Why don't you factor out the construction of derived E? The derived E is just ker(d) over im(d), right? with d=j \circ k. This construction deserves a bit of API of its own I should think. You seem to be proving that the image of d is a normal subgroup of the kernel of d in the middle of things. I should think that if you're going for the spectral sequence of an exact couple then the fact that d^2=0 gives some magic new ker(d)/im(d) which is functorial in (A,d) is a pretty important thing which needs maybe to be done first.

#### Kevin Buzzard (Apr 22 2020 at 11:37):

Note also that everything should be done for R-modules (and Scott would say everything needs to be done for abelian categories, but at the minute this would be out of the frying pan...)

#### Kevin Buzzard (Apr 22 2020 at 11:41):

It takes 1 second on my home PC to compile the partial derived couple code, it's not practically impossible at all to work with the definition as it stands, I just wrote i := λ a, ⟨C.i a, a, rfl⟩, no problem at all. Do you have access to a faster computer? It's holding you back. Still I think that pulling out the definition of derived E is the correct thing to do.

#### Kevin Buzzard (Apr 22 2020 at 11:42):

link to what I think Kenny is doing

#### Kenny Lau (Apr 22 2020 at 11:44):

yes, there are work-arounds, but this shouldn't be slow is my point

#### Kenny Lau (Apr 22 2020 at 11:45):

particularly the definition of exact couple

#### Kenny Lau (Apr 22 2020 at 11:45):

"Nothing is more permanent than a temporary solution." -- Russian Proverb

#### Kevin Buzzard (Apr 22 2020 at 11:47):

I just filled in all the remaining fields with sorry and I think there's a problem with your code.

#### Kevin Buzzard (Apr 22 2020 at 11:48):

failed to synthesize type class instance for
C : exact_couple
(let _inst : is_add_group_hom (C.j ∘ C.k) := _
in quotient_add_group.quotient {y : ↥(is_add_group_hom.ker (C.j ∘ C.k)) | ∃ (x : C.E), C.j (C.k x) = y.val})


#### Kevin Buzzard (Apr 22 2020 at 11:48):

could the slowness be the time it's taking this to fail?

#### Kenny Lau (Apr 22 2020 at 11:48):

it isn't an instance the composition of group hom is a group hom

maybe that's why

#### Kenny Lau (Apr 22 2020 at 11:49):

so maybe I should really factor this out

#### Kenny Lau (Apr 22 2020 at 11:49):

but then why is the exact couple definition slow?

#### Kevin Buzzard (Apr 22 2020 at 11:49):

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
{ y | ∃ x : C.E, C.j (C.k x) = y.1 }
{ add_mem := by rintros ⟨_, h1⟩ ⟨_, h2⟩ ⟨x1, h3⟩ ⟨x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
neg_mem := by rintros ⟨_, h⟩ ⟨x, H⟩; dsimp only at H; subst H; use -x;
i := λ a, ⟨C.i a, a, rfl⟩,
hi := sorry,
j := sorry,
hj := sorry,
k := sorry,
hk := sorry,
hij := sorry,
hji := sorry,
hjk := sorry,
hkj := sorry,
hki := sorry,
hik := sorry
}


It's much faster for me now, when I fill in all the remaining fields

interesting

#### Kevin Buzzard (Apr 22 2020 at 11:50):

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
Ag := sorry,
{ y | ∃ x : C.E, C.j (C.k x) = y.1 }
{ add_mem := by rintros ⟨_, h1⟩ ⟨_, h2⟩ ⟨x1, h3⟩ ⟨x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
neg_mem := by rintros ⟨_, h⟩ ⟨x, H⟩; dsimp only at H; subst H; use -x;
Eg := sorry,
i := λ a, ⟨C.i a, a, rfl⟩,
hi := sorry,
j := sorry,
hj := sorry,
k := sorry,
hk := sorry,
hij := sorry,
hji := sorry,
hjk := sorry,
hkj := sorry,
hki := sorry,
hik := sorry
}


Try that.

thanks

#### Kevin Buzzard (Apr 22 2020 at 11:50):

it's much better

Last updated: May 08 2021 at 04:14 UTC