feat(RingTheory): define Frobenius equations (Coalgebra.IsFrobenius)

[themathqueen]

A coalgebra with an algebra structure A is said to be Frobenius when it satisfies the Frobenius equation:
(id ⊗ mul) ∘ assoc ∘ (comul ⊗ id) = comul ∘ mul = (mul ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul),
which in diagrams looks like

|    |                           |    |
|    μ           |   |           μ    |
|   / \           \ /           / \   |
 \ /   |    =    δ ∘ μ    =    |   \ /
  δ    |          / \          |    δ
  |    |         |   |         |    |

where μ stands for multiplication and δ for comultiplication.
It suffices to show that the left and right diagrams are equal, i.e.,
(id ⊗ mul) ∘ assoc ∘ (comul ⊗ id) = (mul ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul), so this is the only equality in the class.

Because of how long and complicated the names would be, we add abbreviations for the left and right equations, IsFrobenius.left and IsFrobenius.right. So the Frobenius equation is literally left_eq_right : IsFrobenius.left = IsFrobenius.right.

A Frobenius coalgebra is necessarily finite and projective. Also, the bilinear form (LinearMap.mul R A).compr₂ counit is nondegenerate and bijective.

A Bialgebra R A that is Frobenius must have R isomorphic to A.

---

• depends on: [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Associator): add lid_tensor and assoc_tensor #27567
• depends on: [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Associator): lTensor rTensor ∘ assoc = assoc ∘ rTensor lTensor #27569
• depends on: [Merged by Bors] - feat(RingTheory): the coassoc_simps simp set #32245

[github-actions]

PR summary 5eadc834fa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Coalgebra.IsFrobenius (new file)	1166

---

Declarations diff (regex)

+ Coalgebra.IsFrobenius
+ Coalgebra.IsFrobenius.left
+ Coalgebra.IsFrobenius.left_def
+ Coalgebra.IsFrobenius.right
+ Coalgebra.IsFrobenius.right_def
+ LinearMap.mul'_comp_map_lid_comp
+ algebraMap_counit_of_isFrobenius
+ bijective_algebraMap_of_isFrobenius
+ bijective_compr₂_mul_counit
+ bijective_counit_of_isFrobenius
+ comul_apply_eq_of_isFrobenius
+ comul_eq_of_isFrobenius
+ forall_counit_mul_left_eq_zero_iff
+ forall_counit_mul_right_eq_zero_iff
+ instFinite
+ instProjective
+ instance _root_.CommSemiring.toIsFrobenius : IsFrobenius R R
+ lTensor_counit_comp_left_comp_rTensor_algebraLinearMap
+ left_eq_comul_comp_mul'
+ nondegenerate_compr₂_mul_counit
+ nonempty_algEquiv_of_isFrobenius
+ rTensor_counit_comp_right_comp_lTensor_algebraLinearMap
+ right_eq_comul_comp_mul'
+ sum_counit_mul_left_smul_of_comul_one
+ sum_counit_mul_right_smul_of_comul_one

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5eadc83).

• +31 new declarations
• −0 removed declarations

+Bialgebra.algebraMap_counit_of_isFrobenius
+Bialgebra.bijective_algebraMap_of_isFrobenius
+Bialgebra.bijective_counit_of_isFrobenius
+Bialgebra.comul_apply_eq_of_isFrobenius
+Bialgebra.comul_eq_of_isFrobenius
+Bialgebra.nonempty_algEquiv_of_isFrobenius
+Coalgebra.IsFrobenius
+Coalgebra.IsFrobenius.bijective_compr₂_mul_counit
+Coalgebra.IsFrobenius.casesOn
+Coalgebra.IsFrobenius.congr_simp
+Coalgebra.IsFrobenius.forall_counit_mul_left_eq_zero_iff
+Coalgebra.IsFrobenius.forall_counit_mul_right_eq_zero_iff
+Coalgebra.IsFrobenius.instFinite
+Coalgebra.IsFrobenius.instProjective
+Coalgebra.IsFrobenius.lTensor_counit_comp_left_comp_rTensor_algebraLinearMap
+Coalgebra.IsFrobenius.left
+Coalgebra.IsFrobenius.left.congr_simp
+Coalgebra.IsFrobenius.left_def
+Coalgebra.IsFrobenius.left_eq_comul_comp_mul'
+Coalgebra.IsFrobenius.left_eq_right
+Coalgebra.IsFrobenius.mk
+Coalgebra.IsFrobenius.nondegenerate_compr₂_mul_counit
+Coalgebra.IsFrobenius.rTensor_counit_comp_right_comp_lTensor_algebraLinearMap
+Coalgebra.IsFrobenius.rec
+Coalgebra.IsFrobenius.recOn
+Coalgebra.IsFrobenius.right
+Coalgebra.IsFrobenius.right.congr_simp
+Coalgebra.IsFrobenius.right_def
+Coalgebra.IsFrobenius.right_eq_comul_comp_mul'
+CommSemiring.toIsFrobenius
+LinearMap.mul'_comp_map_lid_comp

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 5eadc834fa
Reference commit 3bc2a1801c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[themathqueen]

@Julian-Kuelshammer, the definition of a Frobenius algebra (the version with the bilinear form) is now in #42067, and the equivalence between the definitions is there too.