feat(RingTheory/Coalgebra): classical adjacency matrices are quantum adjacency matrices

[themathqueen]

These are operator algebraic ways of describing a classical finite graph.

We show what the convolutive ring on m -> R looks like. In particular, that the convolutive product corresponds to the Hadamard product. That the convolutive unit 1 corresponds to the matrix of all 1s. And that a diagonal of a matrix A is 0 (resp., 1) iff id * A.toLin' = 0 (resp., = id).
As a result, we get that a matrix A is an adjacency matrix iff its linear map is convolutively idempotent, its intrinsic star is equal to its adjoint, and has id * A.toLin' = 0. With the complete simple graph corresponding to 1 - id.

Motivation:
A quantum adjacency matrix is a linear operator that is convolutively idempotent. One then says that it is "real" if it's intrinsically self-adjoint, self-adjoint if it's self-adjoint, and directed when star A = adjoint A. One also says it's "reflexive" if id * f = id and "irreflexive" if id * f = 0.

So, this PR is the first of many on non-commutative graphs. It says that all finite classical adjacency matrix operators are quantum adjacency matrix operators. In particular, a simple graph's adjacency matrix operator is an irreflexive, self-adjoint, directed, and real quantum adjacency matrix operator.

---

• depends on: [Merged by Bors] - feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra #30880
• depends on: [Merged by Bors] - feat(RingTheory/Coalgebra/Basic): Coalgebra R (Π i, A i) #34312

[github-actions]

PR summary a3a10db0e9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Coalgebra.PiLemmas (new file)	1468

---

Declarations diff

+ LinearMap.ConvolutionProduct.IsIdempotentElem.intrinsicStar_isSelfAdjoint
+ LinearMap.ConvolutionProduct.isIdempotentElem_iff
+ LinearMap.convMul_id_eq_id_iff_diag_toMatrix'_eq_one
+ LinearMap.convMul_id_eq_zero_iff_diag_toMatrix'_eq_zero
+ LinearMap.id_convMul_eq_id_iff_diag_toMatrix'_eq_one
+ LinearMap.id_convMul_eq_zero_iff_diag_toMatrix'_eq_zero
+ LinearMap.toMatrix'_convMul_eq_hadamard
+ LinearMap.toMatrix'_convOne
+ Matrix.ConvolutionProduct.isIdempotentElem_toLin'_iff
+ Matrix.id_convMul_toLin'_eq_id_iff
+ Matrix.id_convMul_toLin'_eq_zero_iff
+ Matrix.isAdjMatrix_iff_toLin'
+ Matrix.isSymm_iff_intrinsicStar_toLin'
+ Matrix.toLin'_convMul_id_eq_id_iff
+ Matrix.toLin'_convMul_id_eq_zero_iff
+ Matrix.toLin'_hadamard_eq_convMul
+ Pi.intrinsicStar_comul
+ SimpleGraph.card_dart_eq_dotProduct
+ SimpleGraph.convolutionProduct_isIdempotentElem_toLin'_adjMatrix
+ SimpleGraph.id_convMul_toLin'_adjMatrix_eq_zero
+ SimpleGraph.intrinsicStar_isSelfAdjoint_toLin'_adjMatrix
+ SimpleGraph.toLin'_adjMatrix_top
+ SimpleGraph.toLin'_convMul_id_adjMatrix_eq_zero
+ SimpleGraph.toMatrix'_convOne_sub_id_eq_adjMatrix_completeGraph
+ update_eq_ite

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[themathqueen]

The naming gets kinda weird because there's ConvolutionProduct and IntrinsicStar. I'm not sure how to best name them when IsSelfAdjoint and IsIdempotentElem are involved. They get long and difficult to remember.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Analysis/InnerProductSpace): finite-dimensional inner product space with an algebra implies a coalgebra #30880
• [Merged by Bors] - feat(RingTheory/Coalgebra/Basic): Coalgebra R (Π i, A i) #34312
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

I think you'll find you don't need this lemma after #34344 lands

[eric-wieser]

Can you now drop Pi.single from this call?