LinearAlgebra.Dual

Stream: mathlib4

[Yury G. Kudryashov]

Quite a few proofs in !4#3659 fail for the same reason: simp can't apply lemmas about LinearMap to Module.Dual. What should we do? Duplicate API? Write a tactic to automate this? Something else?

[Kevin Buzzard]

Not for the same reason, but ext is weaker in lean 4 and to compensate I've been adding extra lemmas.

[Yury G. Kudryashov]

Ping here

[Eric Wieser]

Shouldn't docs#module.dual be reducible?

[Eric Wieser]

I don't see what the point is in having it not be; are there any instances that disagree between the dual and underlying map?

[Yury G. Kudryashov]

Let me try to make it reducible in Lean 3.

[Eric Wieser]

docs#weak_dual should be reducible too I think

[Yury G. Kudryashov]

Why? It has a different topology.

[Yury G. Kudryashov]

UPD: You mean, wek_dual should reducibly unfold to weak_bilin. Probably, yes. I wrote the previous comment before reading the source.

[Eric Wieser]

I made the same assumption in another thread!

[Yury G. Kudryashov]

I tried to make it reducible and I get a timeout in the same file.

[Yury G. Kudryashov]

(I'm talking about module.dual)

[Yury G. Kudryashov]

See branch#YK-dual

[Tchsurvives]

i was looking at this, and it seems to compile fine in lean4. just that there are linting issues. is all that is left a simple clean up? or are you guys still working on it. i would be happy to attempt the clean up

[Eric Wieser]

The timeout seems to be a problem in simps

[Eric Wieser]

I pushed a fix, the rest of that file is now happy on branch#YK-dual

[Yury G. Kudryashov]

@Eric Wieser Thanks! @Tchsurvives I think that we should merge #18963, wait for mathport, then sync !4#3659

[Matthew Ballard]

I forward ported the changes from #18963. If this thing ever built, it surely does not now. Issues

• broken dot notation on LinearMap
• timeouts
• universe issues stemming from Cardinal.lift.{max v u, u}

[Kevin Buzzard]

My understanding is that broken dot notation on LinearMap is issue lean4#1910 .

[Matthew Ballard]

I see. Thanks! I will do the dumb workaround until then.

[Matthew Ballard]

That is if my computer doesn't melt through the desk after turning off heartbeats on one of these timeouts :hot:

[Matthew Ballard]

This files drains all my happiness at the speed bump from

[Eric Wieser]

I forward ported the changes from #18963.

It might have been a better idea to start fresh; I think the old PR has quite a few hacks that should no longer be necessary as of #18963

[Matthew Ballard]

I’ll step back and try this.

[Matthew Ballard]

Did this. Did help with some timeouts. Added one. Currently working on this on a different branch. Will merge soon

[Matthew Ballard]

Thanks to @Chris Hughes for clearing one timeout. For the second (and third), W.dualPairing is exceptional slow for [Field K] and W : Subspace K V. For example,

example (W : Submodule R M) : Module.Dual R M ⧸ dualAnnihilator W →ₗ[R] Module.Dual R W := Submodule.dualPairing W

is instantaneous while

example (W : Subspace K V) : Module.Dual K V ⧸ dualAnnihilator W →ₗ[K] Module.Dual K W :=
    W.dualPairing

times out to the order of 400000 heartbeats

[Matthew Ballard]

Replacing W.dualPairing with sorry is instantaneous

[Eric Wieser]

docs#submodule.dual_pairing

[Eric Wieser]

Does adding by exact to the start of either spelling change the duration?

[Matthew Ballard]

Let me check

[Eric Wieser]

There was some weirdness in Lean3 where the value of the definition would fill in the metavariables in its type

[Matthew Ballard]

Eric Wieser said:

Does adding by exact to the start of either spelling change the duration?

No improvement in time

[Kevin Buzzard]

Changing (K : Type _) (V : Type _) to (K : Type u) (V : Type v) makes it not time out (but it's still slow). I find this quite surprising!

[Matthew Ballard]

Aha!

[Matthew Ballard]

Suggestively I already had to do some universe triage

[Kevin Buzzard]

(K : Type _) (V : Type v) times out

[Matthew Ballard]

It is K

[Matthew Ballard]

It is a rather brutal time out without that. Over 9000000

[Eric Wieser]

Kevin Buzzard said:

Changing (K : Type _) (V : Type _) to (K : Type u) (V : Type v) makes it not time out (but it's still slow). I find this quite surprising!

We should definitely do this then. When we write Type _ we almost always mean Type new_u and we're just lazy. In Lean3 these were basically identical, but lean 4 goes on a unification wild goose chase in every lemma

[Eric Wieser]

Can we have a macro %Type such that K : %Type just means universes uK, K : Type uK?

[Matthew Ballard]

Matthew Ballard said:

It is a rather brutal time out without that. Over 9000000

dualPairing_eq goes down to 400000 now

[Matthew Ballard]

There is some universe gymnastics with Cardinal.lift and max u v already in the file

[Kevin Buzzard]

theorem dualPairing_eq (W : Subspace K V₁) :
    W.dualPairing = W.quotAnnihilatorEquiv.toLinearMap := by
  ext
  rfl

takes longer if you make the universes explicit?! ext takes 11.8 seconds not 7.79 on my machine shrug

[Matthew Ballard]

I couldn't get past the declaration without explicit universes and didn't profile yet

[Kevin Buzzard]

Here is the behaviour of Type u behaving better than Type _ on mathlib master:

import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.LinearAlgebra.Projection
import Mathlib.LinearAlgebra.SesquilinearForm
import Mathlib.RingTheory.Finiteness
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic

noncomputable section

namespace Module

universe u v

variable (R : Type u) (M : Type v)

variable [CommSemiring R] [AddCommMonoid M] [Module R M]

/-- The dual space of an R-module M is the R-module of linear maps `M → R`. -/
@[reducible]
def Dual :=
  M →ₗ[R] R
#align module.dual Module.Dual

/-- The canonical pairing of a vector space and its algebraic dual. -/
def dualPairing (R M) [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Module.Dual R M →ₗ[R] M →ₗ[R] R :=
  LinearMap.id
#align module.dual_pairing Module.dualPairing

end Module

namespace Submodule

universe u v

variable {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M]

variable {W : Submodule R M}

def dualRestrict (W : Submodule R M) : Module.Dual R M →ₗ[R] Module.Dual R W :=
  LinearMap.domRestrict' W

def dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M]
    (W : Submodule R M) : Submodule R <| Module.Dual R M :=
  LinearMap.ker W.dualRestrict

end Submodule

section CommRing

variable {R M M' : Type _}

variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M']

namespace Submodule

def dualPairing (W : Submodule R M) : Module.Dual R M ⧸ W.dualAnnihilator →ₗ[R] W →ₗ[R] R :=
  W.dualAnnihilator.liftQ W.dualRestrict le_rfl
#align submodule.dual_pairing Submodule.dualPairing

end Submodule

end CommRing

section test -- fun starts here

open Submodule

variable (R : Type _) (M : Type _) [CommRing R] [AddCommGroup M] [Module R M]

-- instant for rings.
example (W : Submodule R M) : Module.Dual R M ⧸ dualAnnihilator W →ₗ[R] Module.Dual R W :=
  W.dualPairing

-- But for fields it's slow. And how slow it is depends on whether you named your
-- universes!

-- Ku and Vu have explicit named universes
variable (Ku : Type u) (Vu : Type v) [Field Ku] [AddCommGroup Vu] [Module Ku Vu]

-- This is much slower than the ring example
example (W : Submodule Ku Vu) : Module.Dual Ku Vu ⧸ dualAnnihilator W →ₗ[Ku] Module.Dual Ku W :=
  W.dualPairing

-- But without explicit named universes...
variable (K : Type _) (V : Type _) [Field K] [AddCommGroup V] [Module K V]

-- this times out!
--set_option maxHeartbeats 1000000 in
example (W : Submodule K V) : Module.Dual K V ⧸ dualAnnihilator W →ₗ[K] Module.Dual K W :=
  W.dualPairing

end test

[Kevin Buzzard]

Note that this doesn't help with answering the question of why fields are slower than rings.

[Matthew Ballard]

This is slow but does not need bumps

def comp_dualPairing_mkQ_eq (W : Subspace K V₁) :
    LinearMap.comp W.dualPairing (mkQ W.dualAnnihilator) =
    LinearMap.comp W.quotAnnihilatorEquiv.toLinearMap (mkQ W.dualAnnihilator) := by
  ext
  rfl

Trying to stick this into dualPairing_eq is as bad as not

[Kevin Buzzard]

Here is the relevant trace for

variable (R : Type _) (M : Type _) [CommRing R] [AddCommGroup M] [Module R M]

example (W : Submodule R M) : Module.Dual R M ⧸ dualAnnihilator W →ₗ[R] Module.Dual R W :=
  W.dualPairing

:

(pp.all off)
[Meta.isDefEq] [0.003974s] ✅ Module.Dual R M ⧸ Submodule.dualAnnihilator W →ₗ[R]
      Module.Dual R { x // x ∈ W } =?= Module.Dual R M ⧸ Submodule.dualAnnihilator W →ₗ[R] { x // x ∈ W } →ₗ[R] R ▶

(pp.all on)
@LinearMap.{?u.18485, ?u.18485, max ?u.18488 ?u.18485, max ?u.18488 ?u.18485} R R
      (@CommSemiring.toSemiring.{?u.18485} R (@CommRing.toCommSemiring.{?u.18485} R inst✝²))
...
=?=
@LinearMap.{?u.18485, ?u.18485, max (max ?u.18485 ?u.18488) ?u.18488 ?u.18485,
          max ?u.18485 ?u.18488}
      R R (@CommSemiring.toSemiring.{?u.18485} R (@CommRing.toCommSemiring.{?u.18485} R inst✝²))
...

The universes don't quite match up, but the terms (which are huge) at least start off the same, and it wouldn't surprise me if they are very close to being the same modulo universe issues. Here in contrast is the trace for the fields, when we include the universes:

variable (Ku : Type u) (Vu : Type v) [Field Ku] [AddCommGroup Vu] [Module Ku Vu]

example (W : Submodule Ku Vu) : Module.Dual Ku Vu ⧸ dualAnnihilator W →ₗ[Ku] Module.Dual Ku W :=
  W.dualPairing

:

(pp.all off)
[Meta.isDefEq] [2.535892s] ✅ Module.Dual Ku Vu ⧸ Submodule.dualAnnihilator W →ₗ[Ku]
      Module.Dual Ku { x // x ∈ W } =?= Module.Dual Ku Vu ⧸ Submodule.dualAnnihilator W →ₗ[Ku] { x // x ∈ W } →ₗ[Ku] Ku ▼

(pp.all on)
LinearMap.{u, u, max v u, max v u} Ku Ku
      (@DivisionSemiring.toSemiring.{u} Ku (@Semifield.toDivisionSemiring.{u} Ku (@Field.toSemifield.{u} Ku inst✝²)))
...
=?=
@LinearMap.{u, u, max (max u v) v u, max u v} Ku Ku
      (@CommSemiring.toSemiring.{u} Ku
...

It takes a while to reconcile. It is not one big long thing, it's a huge tree of fairly quick things. Making the universes explicit means that Lean does not have to contemplate questions like ?u.18485 =?= ?u.18488 but allowing fields seems to make the total number of questions Lean asks rocket up. There are questions like AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup which in the ring case are just rfl and closed in 0.0000... seconds, but in the field case involve a lot of unfolding.

Making universes implicit as well just pushes it over the edge. But there are two independent issues here.

[Matthew Ballard]

Yeah it goes into the quotient many times each with a decent cost.

[Matthew Ballard]

I don't see a good near-term solution other than merge with the bumps in place for the moment so I've marked in awaiting-review

[Matthew Ballard]

Advert for !4#4124 LinearAlgebra.Contraction. It is almost across the line but I will be preparing/traveling this weekend. Please finish it off