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