Zulip Chat Archive

Stream: mathlib4

Topic: LinearEquiv.finrank_eq : typeclass instance problem is stuck


Utensil Song (Nov 16 2023 at 10:22):

For this #mwe

import Mathlib.RingTheory.FiniteType
import Mathlib.Tactic

open FiniteDimensional

example (R: Type uR) (A B: Type uA) [CommRing R] [AddCommGroup A] [AddCommGroup B]
  [Module R A] [Module R B] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B)  finrank R A = finrank R B := by
  intro ha
  have hl := ha.toLinearEquiv
  /-
    typeclass instance problem is stuck, it is often due to metavariables

    Module ?m.2272 ?m.2274
  -/
  -- have hf := LinearEquiv.finrank_eq hl

  /-
    application type mismatch
      LinearEquiv.finrank_eq hl
    argument
      hl
    has type
      @LinearEquiv R R CommSemiring.toSemiring CommSemiring.toSemiring (RingHom.id R) (RingHom.id R)
        (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) A B
        NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule
        Algebra.toModule : Type uA
    but is expected to have type
      @LinearEquiv R R Ring.toSemiring Ring.toSemiring (RingHom.id R) (RingHom.id R)
        (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) (_ : RingHomInvPair (RingHom.id R) (RingHom.id R)) A B
        AddCommGroup.toAddCommMonoid AddCommGroup.toAddCommMonoid inst✝⁵ inst✝⁴ : Type uA
  -/
  have hf' := @LinearEquiv.finrank_eq R A B _ _ _ _ _ hl

I can't see why the types mismatch. Any ideas?

Eric Rodriguez (Nov 16 2023 at 11:43):

can you try by convert hl to see what the diamond is?

Eric Wieser (Nov 16 2023 at 11:43):

You put two additive structures on A and B

Eric Wieser (Nov 16 2023 at 11:44):

[AddCommGroup A] [Semiring A] is bad as it defines + twice; it should be [Ring A]

Utensil Song (Nov 16 2023 at 11:55):

They come from the process trying to meet the need for both the ≃ₐ and finrank. Changing the statement to

example (R: Type uR) (A B: Type uA) [CommRing R] [Ring A] [Ring B]
  [Module R A] [Module R B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B)  finrank R A = finrank R B :=

gives me almost identical error.

Utensil Song (Nov 16 2023 at 11:56):

Eric Rodriguez said:

can you try by convert hl to see what the diamond is?

Thanks, I don't understand where can I put this, tried a few places, none type checks.

Eric Wieser (Nov 16 2023 at 11:57):

[Module R A] [Algebra R A] is bad for the same reason, the latter implies the former

Eric Wieser (Nov 16 2023 at 11:57):

With both, you're giving two unrelated scalar multiplication actions

Utensil Song (Nov 16 2023 at 11:59):

Utensil Song said:

Eric Rodriguez said:

can you try by convert hl to see what the diamond is?

Thanks, I don't understand where can I put this, tried a few places, none type checks.

If I write convert LinearEquiv.finrank_eq, Lean hangs forever.

Utensil Song (Nov 16 2023 at 12:06):

Eric Wieser said:

[Module R A] [Algebra R A] is bad for the same reason, the latter implies the former

Thanks! That's probably the cause. Before merging into Ring, Algebra complains can't synth Module, and adding Module to address the complaint caused the stuck.

Utensil Song (Nov 16 2023 at 12:06):

It now becomes the one-liner it should be:

example (R: Type uR) (A B: Type uA) [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] :
  (A ≃ₐ[R] B)  finrank R A = finrank R B := fun ha => LinearEquiv.finrank_eq ha.toLinearEquiv

Utensil Song (Nov 16 2023 at 12:18):

And this was the motive:

import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
import Mathlib.RingTheory.FiniteType
import Mathlib.Tactic

open FiniteDimensional

local notation "Clℂ" => CliffordAlgebra CliffordAlgebraComplex.Q

example : finrank  Clℂ = finrank   := LinearEquiv.finrank_eq CliffordAlgebraComplex.equiv.toLinearEquiv

Last updated: Dec 20 2023 at 11:08 UTC