Typeclass inference help

Stream: new members

[Richard Copley]

Can you help me understand what's going wrong here? The theorem LinearMap.ker_eq_bot does apply to f (a linear map on the TensorProduct of two submodules of a TensorAlgebra), but it needs some cajoling.

X problem: Find a linear equivalence e : W₁ ⊗[R] W₂ ≃ₗ[R] W₁ * W₂
W problem: Find a basis for W₁ * W₂ given bases for W₁ and W₂ (idea : (Basis.tensorProduct ℰ₁ ℰ₂).map e)

import Mathlib.LinearAlgebra.TensorAlgebra.Basic
import Mathlib.LinearAlgebra.TensorProduct

set_option autoImplicit false

open TensorProduct

variable {R M P : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P]

example {W₁ W₂ : Submodule R (TensorAlgebra R M)} {f : W₁ ⊗[R] W₂ →ₗ[R] P} :
    LinearMap.ker f = ⊥ ↔ Function.Injective f :=
  LinearMap.ker_eq_bot
--~~~~~~~~~~~~~~~~~~~~
-- type mismatch
--   LinearMap.ker_eq_bot
-- has type
--   LinearMap.ker ?m.11471 = ⊥ ↔ Function.Injective ↑?m.11471 : Prop
-- but is expected to have type
--   LinearMap.ker f = ⊥ ↔ Function.Injective ↑f : Prop

-- Workaround 1
example {W₁ W₂ : Submodule R (TensorAlgebra R M)} {f : W₁ ⊗[R] W₂ →ₗ[R] P} :
    LinearMap.ker f = ⊥ ↔ Function.Injective f :=
  @LinearMap.ker_eq_bot _ _ _ _ _ _ (inferInstance : AddCommGroup (W₁ ⊗[R] W₂)) _ _ _ _ _

-- Workaround 2
theorem forgetful_ker_eq_bot {W₁ W₂ : Submodule R M} {f : W₁ ⊗[R] W₂ →ₗ[R] P} :
    LinearMap.ker f = ⊥ ↔ Function.Injective f :=
  LinearMap.ker_eq_bot

example {W₁ W₂ : Submodule R (TensorAlgebra R M)} {f : W₁ ⊗[R] W₂ →ₗ[R] P} :
    LinearMap.ker f = ⊥ ↔ Function.Injective f :=
  forgetful_ker_eq_bot

[Kevin Buzzard]

Here's another workaround:

example {W₁ W₂ : Submodule R (TensorAlgebra R M)} {f : W₁ ⊗[R] W₂ →ₗ[R] P} :
    LinearMap.ker f = ⊥ ↔ Function.Injective f :=
  letI : AddCommGroup (W₁ ⊗[R] W₂) := inferInstance
  LinearMap.ker_eq_bot

[Richard Copley]

Much better! I tried haveI, but not letI.
And with that, I suppose it's not worth worrying the underlying issue. Thanks.

[Kevin Buzzard]

haveI is for proofs, but this structure is data.

You can see the trace with set_option trace.Meta.synthInstance true in beforehand. I disagree that it's not worrying about the underlying issue -- something is broken here.

[Meta.synthInstance] ❌ AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▼
  [] new goal AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ❌ apply inst✝¹ to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ❌ apply inst✝³ to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ❌ apply @TensorProduct.addCommGroup to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▼
    [tryResolve] ❌ AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ≟ AddCommGroup (?m.6801 ⊗[?m.6799] ?m.6802) ▼
      [] ❌ AddCommGroup (↥W₁) ▼
        [] new goal AddCommGroup (↥W₁) ▶
        [] ❌ apply inst✝¹ to AddCommGroup (↥W₁) ▶
        [] ❌ apply inst✝³ to AddCommGroup (↥W₁) ▶
        [] ❌ apply @Submodule.addCommGroup to AddCommGroup (↥W₁) ▼
          [tryResolve] ❌ AddCommGroup (↥W₁) ≟ AddCommGroup (↥?m.6823)

[Kevin Buzzard]

I have no idea how to debug this. [tryResolve] is failing to find AddCommGroup (↥W₁) in your original failing example (see above), but in the letI calculation it succeeds (see below):

[Meta.synthInstance] ✅ AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▼
  [] new goal AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ❌ apply inst✝¹ to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ❌ apply inst✝³ to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▶
  [] ✅ apply @TensorProduct.addCommGroup to AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▼
    [tryResolve] ✅ AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ≟ AddCommGroup ((↥W₁) ⊗[R] ↥W₂) ▼
      [] ✅ AddCommGroup (↥W₁) ▼
        [] new goal AddCommGroup (↥W₁) ▶
        [] ❌ apply inst✝¹ to AddCommGroup (↥W₁) ▶
        [] ❌ apply inst✝³ to AddCommGroup (↥W₁) ▶
        [] ✅ apply @Submodule.addCommGroup to AddCommGroup (↥W₁) ▼
          [tryResolve] ✅ AddCommGroup (↥W₁) ≟ AddCommGroup (↥W₁) ▼
            [] ✅ Ring R ▶
            [] ✅ AddCommGroup (TensorAlgebra R M) ▶

(oh -- somehow Lean could infer the type metavariable in the succeeding case?)

[Richard Copley]

((↥W₁) ⊗[R] ↥W₂) vs (?m.6801 ⊗[?m.6799] ?m.6802)

[Richard Copley]

I had been thinking the problem must be with finding two non-defeq instances of the same typeclass, which was why 'forgetting' about TensorAlgebra helped. Now I'm not sure.

[Kevin Buzzard]

Whatever it is, it's yet more evidence that computer scientists find it extremely hard to implement something which mathematicians do completely intuitively with zero overhead.

[Richard Copley]

Like e : W₁ ⊗[R] W₂ ≃ₗ[R] W₁ * W₂ -- just write it with an equals sign and move on :)

[Junyan Xu]

W₁ ⊗[R] W₂ ≃ₗ[R] W₁ * W₂ certainly isn't true in general, see my comment about flatness in the other thread.
However it's true if W₁ and W₂ are invertible modules over a domain R. W being invertible means there is another R-module whose R-tensor product with W is isomorphic to R, which implies that W is flat (in fact projective) and isomorphic to an ideal in R. The invertible modules (over a general CommRing) form a group under the tensor product operation, called the Picard group, and it's isomorphic to the docs#ClassGroup of invertible fractional ideals with the submodule product operation. (Invertibility as a fractional ideal is also equivalent to invertibility as a module.) This was on my to-do list because I had some argument about elliptic curves using it, but I later found a different argument, and I only made a measly start in Lean 3.

[Richard Copley]

Interesting! But how does it relate to the (scare quotes) "equivalence"?
Don't we have on the one hand (I⊕0)⊗(0+M)≃I⊗M≃0, and in TensorAlgebra(R,R⊕M) on the other hand, (I⊕0)*(0+M)≃I*M≃0?

[Junyan Xu]

Oh sorry, I didn't notice this is about submodules of the tensor algebra. (I was puzzled where you got the multiplication from!) Give me some time to think about your question in this setting.

[Junyan Xu]

I think in this setting we have a simpler counterexample: take a non-flat R-module M, take an ideal W₁ of R sitting in the 0th graded piece, and let W₂ = Msitting in the 1st graded piece of the tensor algebra. Then W₁*W₂ completely sits inside the 1st graded piece, and is the submodule W₁*M of M. However, since M is not flat, there is some ideal W₁ such that W₁ ⊗[R] M → W₁M isn't injective, so your e isn't injective and can't be a LinearEquiv.

[Junyan Xu]

I⊕0 and 0⊕M from my previous example are meant to both sit in the 1st graded piece, and you'd need to consider the tensor algebra of R⊕M over R for the example to apply. I did the example because @Eric Wieser extracted the special case of "1st x 1st -> 2nd graded piece" in the other thread. In your computations, I agree with (I⊕0)⊗(0⊕M)≃I⊗M and (I⊕0)*(0⊕M)≃I*M, but I don't see why they would be isomorphic to 0.

[Richard Copley]

Yes, those 0s are a mistake. Thanks for this. It's late here, I'll think about this more tomorrow

[Richard Copley]

Still thinking ...

[Richard Copley]

@Junyan Xu, did you just introduce me to homological algebra? Sneaky