feat: cardinality of `Field.Emb` for infinite extensions

[alreadydone]

A construction by transfinite recursion, fairly standard in set theory, but I have yet to see similar arguments in mathlib. See module docstring for more details.

I use some ad hoc category theoretical definitions: IsNatEquiv is (Nat)Iso in the functor category, and inverseLimit is Functor.sections, but it may makes things unnecessarily complicated to use the category library (OrderDual would be needed for example), as the construction is fairly down to earth.

Zulip

---

I think @digama0 @sterraf @YaelDillies @vihdzp might be interested to review this. Are you aware of other similar proofs formalized in mathlib or elsewhere? Is there anything general (about the transfinite recursion setup?) that can be extracted?

Lots of notations are introduced as shorthands in the file; if you see a way to improve them, please let me know.

I now incline to put the majority of defs in a namespace (tentatively Field.Emb.Cardinal) rather than making them private, but that means there are lots of docstrings to add.

• [x] depends on: #9488
• [x] depends on: #11290

[grunweg]

Feel free to label as ready for review, once you have fixed the build failures.

[github-actions[bot]]

PR summary c8f39fa79d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.CardinalEmb	1446

---

Declarations diff

+ Algebra.rank_adjoin_le + adjoin_basis_eq_top + adjoin_image_leastExt + cardinal_eq + cardinal_eq_of_isSeparable + cardinal_eq_two_pow_rank + cardinal_eq_two_pow_sepDegree + deg_lt_aleph0 + directed_filtration + embEquivPi + embFunctor + eq_bot_of_not_nonempty + equivLim + equivLim_coherence + equivSucc + equivSucc_coherence + factor + filtration + filtration_succ + iSup_adjoin_eq_top + iSup_filtration + instance (i : ι) : Algebra.IsSeparable (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) + instance (i : ι) : FiniteDimensional (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) + instance : InverseSystem (embFunctor F E) + isLeast_leastExt + leastExt + noMaxOrder_rank_toType + strictMono_filtration + strictMono_leastExt + succEquiv + succEquiv_coherence + two_le_deg + wellOrderedBasis

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-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#9488~~
• ~~leanprover-community/mathlib4#11290~~
• ~~leanprover-community/mathlib4#18067~~ By Dependent Issues (🤖). Happy coding!

[acmepjz]

Great work! Maybe you should change the title to "infinite algebraic extensions". Meanwhile I'm working on transcendental extensions (I only intend to prove Infinite but not going to compute the exact cardinality). (Edit: it's ready #18770)

I'll look at this more closely later.

[mathlib-bors[bot]]

:v: alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[alreadydone]

Thanks! bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style