ModuleCat.mk slowness

Stream: mathlib4

[Kevin Buzzard]

Here's an interesting, and initially quite confusing, slowdown, which I think might be one cause of the slowness in Mathlib.RepresentationTheory.GroupCohomology.Basic (and which I don't have a strategy to fix):

import Mathlib.RepresentationTheory.GroupCohomology.Basic

universe u

variable {k G : Type u} [CommRing k] [Group G] (n : ℕ) (A : Rep k G)

example : (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) =
  (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) := rfl -- quick

set_option maxHeartbeats 400000 in
example : ModuleCat.mk (R := k) (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) =
    ModuleCat.mk (R := k) (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) := by
  rfl -- sloooow

So we have X = Y with a quick rfl proof, and then T X = T Y and the rfl proof is slow! (8+ seconds on a decent machine). How can that be? Well here's the signature of ModuleCat.mk:

ModuleCat.mk.{v, u} {R : Type u} [inst✝ : Ring R] (carrier : Type v) [isAddCommGroup : AddCommGroup carrier]
  [isModule : Module R carrier] : ModuleCat R

and here's the relevant trace:

[Meta.isDefEq] [8.076313s] ✅ ModuleCat.mk
      (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶
        A) =?= ModuleCat.mk (HomologicalComplex.X (GroupCohomology.resolution k G) n ⟶ A) ▼
  [] [0.133820s] ✅ Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A =?= HomologicalComplex.X (GroupCohomology.resolution k G) n ⟶ A ▶
  [] [4.588565s] ✅ CategoryTheory.Preadditive.homGroup (Rep.ofMulAction k G (Fin (n + 1) → G))
        A =?= CategoryTheory.Preadditive.homGroup
        (HomologicalComplex.X (GroupCohomology.resolution k G) n) A ▶
  [] [3.353870s] ✅ CategoryTheory.Linear.homModule (Rep.ofMulAction k G (Fin (n + 1) → G))
        A =?= CategoryTheory.Linear.homModule (HomologicalComplex.X (GroupCohomology.resolution k G) n) A ▶

So it's taking only 0.1 second to check that X = Y, but typeclass inference has been used to find abelian group and k-module structures on X and Y and it's taking a long time to verify that these are equal too. You can explicitly verify that the group instance is slow:

import Mathlib.RepresentationTheory.GroupCohomology.Basic

universe u

variable {k G : Type u} [CommRing k] [Group G] (n : ℕ) (A : Rep k G)

example : (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) =
  (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) := rfl -- very quick

-- also all quick
noncomputable def i1 : AddCommGroup (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := inferInstance
noncomputable def i2 : AddCommGroup (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) :=
  inferInstance

set_option maxHeartbeats 600000 in -- 500000 not good enough
example : @i1 = @i2 := rfl -- sloooow

There's a bunch of these in the traces in RepresentationTheory.GroupCohomology.Basic. How might one proceed to speed these up?

[Eric Wieser]

I don't think that's a good test; you're asking lean to equate the fully quantified instances. This is fast:

example : @i1 k G _ _ n A = @i2 k G _ _ n A := rfl

[Kevin Buzzard]

But typeclass inference is doing that test tens of times in GroupCohomology.Basic. Or are you telling me it's not? What does the trace above mean?

[Kevin Buzzard]

The trace is taken from a proof in that file with elevated maxHeartbeats

[Eric Wieser]

I find it unlikely that it's equating the unapplied instance

[Kevin Buzzard]

wait -- I claim that on current master

import Mathlib.RepresentationTheory.GroupCohomology.Basic

universe u

variable {k G : Type u} [CommRing k] [Group G] (n : ℕ) (A : Rep k G)

example : (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) =
  (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) := rfl -- very quick

-- also all quick
noncomputable def i1 : AddCommGroup (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := inferInstance
noncomputable def i2 : AddCommGroup (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) :=
  inferInstance

-- set_option maxHeartbeats 300000 in -- this fixes it
example : @i1 k G _ _ n A = @i2 k G _ _ n A := rfl
/-
without the heartbeat bump I get
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
-/

the rfl is failing unless heartbeats are bumped (in particular it's not fast)

[Matthew Ballard]

What do i1 and i2 look like term-wise?

[Matthew Ballard]

Possibly related or not. But in AlgebraicGeometry.Morphisms.RingHomProperties there were way to many round trips between the type + instance and the object of the bundled category. These got layered and (I suspect) slowed things down

[Kevin Buzzard]

set_option maxHeartbeats 300000 in
example : i1 n A = i2 n A := by
  unfold i1
  unfold i2
  delta inferInstance
/-
⊢ CategoryTheory.Preadditive.homGroup (Rep.ofMulAction k G (Fin (n + 1) → G)) A =
  CategoryTheory.Preadditive.homGroup (HomologicalComplex.X (GroupCohomology.resolution k G) n) A
-/
  sorry

[Matthew Ballard]

What is homGroup finding?

[Kevin Buzzard]

Sorry for the delay. With pp.all on the two terms are

  (@CategoryTheory.Preadditive.homGroup.{u, u + 1}
    (@Rep.{u} k G (@CommRing.toRing.{u} k inst✝¹) (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
    (@Action.instCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))))
    (@Action.instPreadditiveActionInstCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
      (@ModuleCat.instPreadditiveModuleCatModuleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹)))
    (@Rep.ofMulAction.{u} k G inst✝¹ (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))
      (Fin
          (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
            (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) →
        G)
      (@Pi.mulAction.{0, u, u}
        (Fin
          (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))))
        (fun
            (a :
              Fin
                (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
                  (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) ↦
          G)
        G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))
        fun
          (i :
            Fin
              (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
                (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) ↦
        @Monoid.toMulAction.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))))
    A)

and

  (@CategoryTheory.Preadditive.homGroup.{u, u + 1}
    (@Rep.{u} k G (@CommRing.toRing.{u} k inst✝¹) (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
    (@Action.instCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))))
    (@Action.instPreadditiveActionInstCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
      (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
      (@ModuleCat.instPreadditiveModuleCatModuleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹)))
    (@HomologicalComplex.X.{u, u + 1, 0} Nat
      (@Rep.{u} k G (@CommRing.toRing.{u} k inst✝¹) (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
      (@Action.instCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
        (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
        (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))))
      (@CategoryTheory.Preadditive.preadditiveHasZeroMorphisms.{u, u + 1}
        (@Rep.{u} k G (@CommRing.toRing.{u} k inst✝¹)
          (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
        (@Action.instCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
          (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
          (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))))
        (@Action.instPreadditiveActionInstCategoryAction.{u} (@ModuleCat.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
          (@ModuleCat.moduleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))
          (@MonCat.of.{u} G (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝)))
          (@ModuleCat.instPreadditiveModuleCatModuleCategory.{u, u} k (@CommRing.toRing.{u} k inst✝¹))))
      (@ComplexShape.down.{0} Nat
        (@AddRightCancelMonoid.toAddRightCancelSemigroup.{0} Nat
          (@AddCancelMonoid.toAddRightCancelMonoid.{0} Nat
            (@AddCancelCommMonoid.toAddCancelMonoid.{0} Nat
              (@OrderedCancelAddCommMonoid.toCancelAddCommMonoid.{0} Nat
                (@StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring)))))
        (@CanonicallyOrderedCommSemiring.toOne.{0} Nat Nat.canonicallyOrderedCommSemiring))
      (@GroupCohomology.resolution.{u} k G inst✝¹ (@DivInvMonoid.toMonoid.{u} G (@Group.toDivInvMonoid.{u} G inst✝))) n)
    A)

[Kevin Buzzard]

Not sure if that's the answer to your question.

Is this a code smell? It's in RepresentationTheory.Rep.

instance (V : Rep k G) : AddCommGroup V := by
  change AddCommGroup ((forget₂ (Rep k G) (ModuleCat k)).obj V); infer_instance

instance (V : Rep k G) : Module k V := by
  change Module k ((forget₂ (Rep k G) (ModuleCat k)).obj V)
  infer_instance

[Kevin Buzzard]

instance (V : Rep k G) : AddCommGroup V := ModuleCat.isAddCommGroup V.V

instance (V : Rep k G) : Module k V := ModuleCat.isModule V.V

doesn't seem to make much difference (in the declaration I'm profiling, at least)

[Kevin Buzzard]

OK so I am completely blocked on this one. Here's a summary.

There are some declarations in the group cohomology files which still take over a minute to compile. What this seems to boil down to is the initially contradictory fact that you can write a function $f$ in Lean and find elements $X$ and $Y$ such that $X=Y$ but $f(X)\not=f(Y)$! Here's how:

import Mathlib.Tactic

class foo (α : Type) where
  bar : α

def foobar (α : Type) [foo α] := foo.bar (α := α)

def X := ℕ
def Y := ℕ

instance : foo X := ⟨(0 : ℕ)⟩
instance : foo Y := ⟨(1 : ℕ)⟩

example : X = Y := rfl

example : foobar X ≠ foobar Y := zero_ne_one (α := ℕ)

This apparent contradiction comes about because even though X and Y are definitionally equal, they're not syntactically equal, so typeclass inference can find unequal terms of type foo X and foo Y.

So now imagine that X = (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) and Y = (((HomologicalComplex.X (GroupCohomology.resolution k G) n)) ⟶ A) as above. These two types are definitionally but not syntactically equal, and rfl is quick to show this. They are also both k-modules, and in particular AddCommGroups, and typeclass inference knows this. However, if we use ModuleCat.mk (R := k) to turn them both into terms of type ModuleCat k and now it is not so obvious that they are still defeq, precisely because of the phenomenon above: we checked they were defeq as types, but now we're claiming they're equal as k-modules so we need to check that e.g. the AddCommGroup structures on them are also defeq, and as the example above shows, this really does need to be checked. And this is exactly the sort of problem which Lean 4 is not very good at: big terms with algebra structures on top of them and definitional equality. Lean 4 wants to take absolutely everything apart and things get super-huge. On my machine Lean will spend 0.1 seconds checking X = Y but it will spend 3 seconds checking that the terms of type AddCommGroup X and AddCommGroup Y found by typeclass inference are also defeq (because it turns out that they are). The thing is, this is all over the group cohomology files and is I believe now the main reason that these files are slow.

So what to do about it? I wondered whether we could make the two AddCommGroup instances "more obviously defeq" but I really don't have a clue how to do it.

[Joël Riou]

Would it be possible to introduce an auxiliary explicit isomorphism (or AddEquiv, whatever structure we have), which would just be a kind of rfl, and prove equational lemmas for it. If this fails to improve the situation, the definition of this iso could be made irreducible.

[Kevin Buzzard]

Yes Mario also suggested that this might be the way to go. The take home message here seems to be that the following principle is wrong: "in category theory, you shouldn't talk about equality of objects, but actually you can make an exception when the proof is rfl."

[Matthew Ballard]

The original example is sped up significantly with the changes in #6759. It takes < 100000 heartbeats (for a bound) and the profiler time drops to ~3s instead of ~8s.

[Kevin Buzzard]

I came back to thinking about this. @Matthew Ballard what is the status of #6759?

@Joël Riou I tried to implement (my understanding of) your suggestion but the naive approach remains problematic:

import Mathlib.RepresentationTheory.GroupCohomology.Basic

noncomputable section

universe u

variable {k G : Type u} [Group G] [CommRing k] (A : Rep k G) (n : ℕ)

-- quick
example : ((Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop ⟶ A) =
    (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := rfl

-- 8 seconds on my fast machine
set_option trace.profiler true in
example : ((Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop ⟶ A) ≃ₗ[k]
  (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := LinearEquiv.refl k _

The proof that X and Y are equal is rfl and quick, but proving they're isomorphic is slow because typeclass inference finds different k-module structures (and different abelian group structures) on the two terms (which are definitionally isomorphic but not syntactically isomorphic). But perhaps one should just take this slowness on the chin once when creating the isomorphism, and then hope it's quick to use.

[Kevin Buzzard]

oh actually this does work: writing the post above forced me to collect my thoughts and in fact just putting in the isomorphism explicitly works straight out of the box. In Mathlib.RepresentationTheory.GroupCohomology from around line 117 one can do this:

variable [Group G] (n) (A : Rep k G)

-- we have to pay here, it takes 8 seconds on my fast machine but (just) doesn't require a maxheartbeats bump.
/-- hack -/
def foo : ((Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop ⟶ A) ≃ₗ[k]
  (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := LinearEquiv.refl k _

-- and now we reap the benefits:

-- no longer true
/- Porting note: linter says the statement doesn't typecheck, so we add `@[nolint checkType]` -/

-- no longer needed
-- set_option maxHeartbeats 700000 in

/-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is
morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains
and the homogeneous `linearYonedaObjResolution`. -/
theorem d_eq :
    d n A =
      -- adding (foo n A).trans makes everything quick and the same proof still works
      ((foo n A).trans (diagonalHomEquiv n A)).toModuleIso.inv ≫
        (linearYonedaObjResolution A).d n (n + 1) ≫
          -- also add it here
          ((foo (n + 1) A).trans (diagonalHomEquiv (n + 1) A)).toModuleIso.hom := by
  ext f g
  [rest of proof omitted]

Note that the proof still works :-)

[Kevin Buzzard]

Next problem in the file boils down to this:

example : (GroupCohomology.linearYonedaObjResolution A).2 (n + 1) (n + 1 + 1) =
    (GroupCohomology.linearYonedaObjResolution A).2 (n + 1) (n + 2) := rfl

(5 seconds on a fast machine). This is why erw is slow in the proof of inhomogeneousCochains causing a heartbeat bump to 2400000,

[Matthew Ballard]

#6759 is effectively #6965 and lean4#2478. I should put the first back on the rails momentarily.

[Mauricio Collares]

I was curious if Sebastian's recent caching improvements were relevant here. Kevin's example is still slow even on the whnf-cache-unfold branch (together with the whnf tracing improvements). It still takes 10s and nothing whnf-related appears in the trace, just lots of defeq checks:
flame_GroupCohomology.svg

[Junyan Xu]

Kevin Buzzard said:

-- we have to pay here, it takes 8 seconds on my fast machine but (just) doesn't require a maxheartbeats bump.
def foo : ((Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop ⟶ A) ≃ₗ[k]
  (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) := LinearEquiv.refl k _

The following is even faster, using 40664 heartbeats rather than 178352 for the version above.

def foo : ((Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop ⟶ A) ≃ₗ[k]
    (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) where
  toFun := id
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun := id
  left_inv _ := rfl
  right_inv _ := rfl

[Kevin Buzzard]

How am I as an end user supposed to spot or understand that this change will have any effect whatsoever?

[Eric Wieser]

That spelling is faster because for id lean only has to agree that the types are the same, but for the .refl it also needs to agree that the instances are the same

[Kevin Buzzard]

Surely the instance work just moves to proving that map_add' is rfl?

[Eric Wieser]

Indeed, but now we only have to check that the add fields are equal, not the whole instance

[Matthew Ballard]

Kevin Buzzard said:

Next problem in the file boils down to this:

example : (GroupCohomology.linearYonedaObjResolution A).2 (n + 1) (n + 1 + 1) =
    (GroupCohomology.linearYonedaObjResolution A).2 (n + 1) (n + 2) := rfl

~9500 heartbeats with lean4#2644 and lean4#2478 -- you can play with a working copy of mathlib at #7645