feat(Matrix): extracting entries as a linear map #17535
Conversation
PR summary 6f3aca5ef8
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Matrix.Basic | 806 | 808 | +2 (+0.25%) |
Import changes for all files
| Files | Import difference |
|---|---|
13 filesMathlib.Data.Matrix.Auto Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Data.Matrix.Basis Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Coxeter.Basic Mathlib.Data.Matrix.Reflection Mathlib.LinearAlgebra.Matrix.Trace Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.Data.Matrix.Hadamard Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Data.Matrix.Notation Mathlib.Combinatorics.SimpleGraph.AdjMatrix |
1 |
14 filesMathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.PEquiv Mathlib.Data.Matrix.CharP Mathlib.Data.Matrix.Block Mathlib.CategoryTheory.Preadditive.Mat Mathlib.Topology.UniformSpace.Matrix Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.Data.Matrix.RowCol Mathlib.Data.Matrix.DualNumber Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Orthogonal |
2 |
Declarations diff
+ entryAddHom
+ entryAddHom_comp_mapMatrix
+ entryAddHom_eq_comp
+ entryAddMonoidHom
+ entryAddMonoidHom_comp_mapMatrix
+ entryAddMonoidHom_eq_comp
+ entryAddMonoidHom_toAddHom
+ entryLinearMap
+ entryLinearMap_eq
+ entryLinearMap_toAddHom
+ entryLinearMap_toAddMonoidHom
+ evalAddMonoidHom_comp_diagAddMonoidHom
+ mapMatrix_toLinearMap
+ proj_comp_diagLinearMap
++ entryLinearMap_comp_mapMatrix
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
(Oops, putting this back to WIP because I realised I want to add a bit more to it!) |
Mathlib/Data/Matrix/Basic.lean
Outdated
| @[simp] lemma elemLinearMap_toAddMonoidHom {i : m} {j : n} : | ||
| (elemLinearMap R α i j).toAddMonoidHom = elemAddMonoidHom α i j := rfl | ||
|
|
||
| @[simp] lemma elemLinearMap_toAddHom {i : m} {j : n} : | ||
| (elemLinearMap R α i j).toAddHom = elemAddHom α i j := rfl |
There was a problem hiding this comment.
Is there a reason to have these as opposed to the versions utilizing the hom class coercions?
There was a problem hiding this comment.
Oops, the first one gets elaborated to the hom class coercions but the second doesn't, that's a mistake on my part. Will amend.
There was a problem hiding this comment.
Oh, actually they are all utilizing the hom class coercions already. Could you clarify what you meant then?
There was a problem hiding this comment.
I changed the spelling for clarity.
Mathlib/Data/Matrix/Basic.lean
Outdated
| @[simp] lemma elemAddMonoidHom_toAddHom {i : m} {j : n} : | ||
| (elemAddMonoidHom α i j).toAddHom = Matrix.elemAddHom α i j := rfl |
Mathlib/Data/Matrix/Basic.lean
Outdated
|
|
||
| -- The type ascription on the RHS is necessary for unification to succeed on the composition. | ||
| lemma elemAddHom_eq_comp {i : m} {j : n} : | ||
| elemAddHom α i j = (Pi.evalAddHom _ j).comp (Pi.evalAddHom _ i : AddHom _ (n → α)) := |
There was a problem hiding this comment.
Arguably you should launder through of here to avoid needing the type ascription.
There was a problem hiding this comment.
I'm not quite sure I follow - of is for building matrices, but both sides here are maps out of a matrix space. I'm happy to use of, but I don't see how it fits here.
Oops, didn't realise of was an equiv. I'm still not sure how to make it fit though, because it doesn't give me a linear map
There was a problem hiding this comment.
You could add an ofLinearEquiv as a linear version of of.
There was a problem hiding this comment.
Sounds potentially helpful but a can of worms I'd rather not open here (AddEquiv; LinearEquiv; RingEquiv; AlgebraEquiv...). Would you be happy with a todo instead?
There was a problem hiding this comment.
I think it's fine to just add the bundling you need; the simp-normal form would remain of
Strictly speaking, something like this was available as
LinearMap.proj, but actually using it in practice is awkward as unification struggles (see line 1227 in this PR).I'm happy to take name suggestions, as well as ideas for other generalities.