!4#3710 LinearAlgebra.Matrix.SpecialLinearGroup

Stream: mathlib4

[Jeremy Tan]

What is the correct syntax to express coercion to a fixed type as a prefix, so that the following example will work?

import Mathlib.LinearAlgebra.GeneralLinearGroup
import Mathlib.LinearAlgebra.Matrix.Adjugate
import Mathlib.LinearAlgebra.Matrix.ToLin

namespace Matrix

universe u v

open Matrix LinearMap

section

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

def SpecialLinearGroup :=
  { A : Matrix n n R // A.det = 1 }

end

namespace SpecialLinearGroup

variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R]

instance hasCoeToMatrix : Coe (SpecialLinearGroup n R) (Matrix n n R) := ⟨fun A => A.val⟩

/- In this file, Lean often has a hard time working out the values of `n` and `R` for an expression
like `det ↑A`. Rather than writing `(A : Matrix n n R)` everywhere in this file which is annoyingly
verbose, or `A.val` which is not the simp-normal form for subtypes, we create a local notation
`↑ₘA`. This notation references the local `n` and `R` variables, so is not valid as a global
notation. -/
local prefix:1024 "↑ₘ" => @coe _ (Matrix n n R) _

theorem ext_iff (A B : SpecialLinearGroup n R) : A = B ↔ ∀ i j, ↑ₘA i j = ↑ₘB i j :=
  Subtype.ext_iff.trans Matrix.ext_iff.symm

[Jeremy Tan]

Here I want to have ↑ₘA mean (A : Matrix n n R)

[Eric Wieser]

What goes wrong with the above?

[Jeremy Tan]

unknown identifier 'coe' at quotation precheck; you can use set_option quotPrecheck false to disable this check.

[Jeremy Tan]

And I don't know what to replace coe by – (↑) certainly doesn't work

[Eric Wieser]

Subtype.val will work here

[Eric Wieser]

The comment about .val in the docstring no longer applies in Lean 4, since the two are now the same thing

[Jeremy Tan]

Now in this piece of code Lean is complaining about

failed to synthesize instance
  Inv { A // det A = 1 }

despite the hasInv instance being in plain sight of it. How do I get coe_inv to compile?

import Mathlib.LinearAlgebra.GeneralLinearGroup
import Mathlib.LinearAlgebra.Matrix.Adjugate
import Mathlib.LinearAlgebra.Matrix.ToLin

universe u v

open Matrix LinearMap

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

def SpecialLinearGroup :=
  { A : Matrix n n R // A.det = 1 }

instance hasCoeToMatrix : Coe (SpecialLinearGroup n R) (Matrix n n R) := ⟨fun A => A.val⟩

local prefix:1024 "↑ₘ" => Subtype.val

instance hasInv : Inv (SpecialLinearGroup n R) :=
  ⟨fun A => ⟨adjugate A, by rw [det_adjugate, A.prop, one_pow]⟩⟩

variable (A B : SpecialLinearGroup n R)

@[simp]
theorem coe_inv : ↑ₘA⁻¹ = adjugate A :=
  rfl

[Eric Wieser]

Ah, this indeed isn't going to work

[Eric Wieser]

The problem is that Subtype.val has the wrong type

[Jeremy Tan]

This is part of porting PR !4#3710, LinearAlgebra.Matrix.SpecialLinearGroup. Have a look

[Eric Wieser]

local notation "↑ₘ" A:1024 => ((A : SpecialLinearGroup n R) : Matrix n n R) seems to work

[Jeremy Tan]

Eric Wieser said:

local notation "↑ₘ" A:1024 => ((A : SpecialLinearGroup n R) : Matrix n n R) seems to work

But then I have to put brackets around all the ↑ₘAs and ↑ₘBs to prevent a syntax error in the earlier ext_iff lemma, i.e.

theorem ext_iff (A B : SpecialLinearGroup n R) : A = B ↔ ∀ i j, (↑ₘA) i j = (↑ₘB) i j :=
  Subtype.ext_iff.trans Matrix.ext_iff.symm

[Eric Wieser]

It sounds like I have the precedence wrong

[Eric Wieser]

I unfortunately don't know the Lean4 syntax, and I can't use #print notation like I could in Lean 3 to learn it

[Eric Wieser]

Pushed a commit that fixes it

[Jeremy Tan]

Right, I might have to call @Scott Morrison to fix the eta-related errors left in this file

[Jeremy Tan]

toLin' is proving tough, even with the new eta_experiment% (local eta) feature

[Kevin Buzzard]

unknown identifier 'coe' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.

[Notification Bot]

4 messages were moved here from #mathlib4 > Expressing coercion in a prefix by Eric Wieser.

[Eric Wieser]

Sorry @Kevin Buzzard, this thread ended up split