Mathlib/ folder upstreaming

Stream: FLT

[Ruben Van de Velde]

Kevin Buzzard said:

There is also the complex question of how to get some of this stuff into mathlib; FLT's Mathlib directory now stands at 548K and much of it is the background for this finiteness result. The stuff in the Mathlib directory is stuff which people felt was definitely mathlib-appropriate at the time. Quite how we're going to get it into mathlib I don't know but this problem needs to be solved.

Trying to review the work needed here, but only got up to LinearAlgebra/. I might continue tomorrow.

./FLT/Mathlib/Algebra/Algebra/Bilinear.lean
    1. Part about SemialgHom; depends on definition
    2. LinearEquiv.mulLeft, mulRight can be PRd now
./FLT/Mathlib/Algebra/Algebra/Hom.lean
    Defines SemialgHom. First step is probably getting mathlib consensus that this is desirable
./FLT/Mathlib/Algebra/Algebra/Pi.lean
    1. Part about SemialgHom; depends on definition
    2. AlgEquiv.piCongrFiberwise can be PRd now
./FLT/Mathlib/Algebra/Algebra/Tower.lean
    Defines AlgEquiv.extendScalars, AlgHom.changeScalars, AlgEquiv.changeScalars. Might need more API written about them.
./FLT/Mathlib/Algebra/Central/TensorProduct.lean
    Subalgebra and Submodule lemmas, culminating in Algebra.IsCentral A (A ⊗[k] B) instance. Should be ready to PR.
./FLT/Mathlib/Algebra/FixedPoints/Basic.lean
    New definitions Add/MulAction.FixedPoints. Probably ready to PR
./FLT/Mathlib/Algebra/IsDirectLimit.lean
    New definition IsDirectLimit for DirectedSystem. Probably ready to PR
./FLT/Mathlib/Algebra/IsQuaternionAlgebra.lean
    New definitions IsQuaternionAlgebra and IsTotallyDefinite. Minimal API in this file; might want to PR along with other code that uses them.
./FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
    LinearMap.finsum_apply: ready to PR but not in the corresponding file. Should it use LinearMapClass?
./FLT/Mathlib/Algebra/Module/Submodule/Basic.lean
    Subring.toSubmodule: needs API and might need to go into another file
./FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
    Looks like reasonable lemmas about AbsoluteValue. I thought I made a PR for these a while ago; will try to find out what happened.
./FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean
    1. WithAbs section seems fine
    2. Part about SemialgHom; depends on definition
./FLT/Mathlib/Data/Fin/Basic.lean
    Fin.pairwise_forall_two: seems fine, but probably in another file.
./FLT/Mathlib/Data/Real/Archimedean.lean
    1. Real.exists_floor': replace proof of existing Real.exists_floor (#33902)
    2. Int.eq_floor: might ne better to inline
./FLT/Mathlib/Data/Set/Countable.lean
    Countable.of_countable_fibres: ready to PR
./FLT/Mathlib/Data/Set/Prod.lean
    Set.pi_subset_pi_of_superset: ready to PR
./FLT/Mathlib/GroupTheory/DoubleCoset.lean
    1. group-theoretic lemmas are ready to PR
    2. two topological lemmas need to go elsewhere and depend on FLT.Mathlib.Topology.Algebra.Group.Quotient
./FLT/Mathlib/GroupTheory/Index.lean
    Cool notation and some todo's. Probably for Yaël to pursue
./FLT/Mathlib/LinearAlgebra/Countable.lean
    Ready to PR, but probably not in this file
./FLT/Mathlib/LinearAlgebra/Determinant.lean
    Mostly straightforward, but some parts depend on https://github.com/leanprover-community/mathlib4/pull/26377
./FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean
    New definition Module.Finite.equivPi, only lemma depends on FLT.Mathlib.RingTheory.TensorProduct.Pi
./FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
    1. New definition Matrix.GeneralLinearGroup.diagonal: ready to PR with a bit more API
    2. Matrix.GeneralLinearGroup.GL2.unipotent: redundant with Matrix.GeneralLinearGroup.upperRightHom
./FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean
    Seems ready to PR
./FLT/Mathlib/LinearAlgebra/Pi.lean
    New definition Pi.FiberwiseSMul and a small number of lemmas
./FLT/Mathlib/LinearAlgebra/Span/Defs.lean
    Seems to exist only to add simp/norm_cast attributes to the existing lemma
./FLT/Mathlib/LinearAlgebra/TensorProduct/Algebra.lean
    AlgHom.rTensor: ready to PR
./FLT/Mathlib/LinearAlgebra/TensorProduct/Basis.lean
    Nontrivial instances for tensor products. Will need a benchmark run
./FLT/Mathlib/LinearAlgebra/TensorProduct/FiniteFree.lean
    LinearEquiv.chooseBasis_piScalarRight: ready to PR, unless we want to try to generalize to semirings first

Seems like a reasonable amount of available work if people want to help

[Kevin Buzzard]

Thanks for this. I guess some of it will depend on the fact that we allow $A \otimes B$ to be a $B$-algebra in FLT? This would not be acceptable in mathlib.

[Ruben Van de Velde]

I don't think I've seen any opens in the files I've looked at yet, but I read pretty diagonally

[Bryan Wang]

Just a heads up that I have/will be working on some upstreaming, mainly the parts that I used/wrote. Is there some way for me to tag PRs with the FLT label?

[Michael Rothgang]

Post a comment here, so somebody knows the PR should be tagged? I don't think other options currently exist, good catch!

[Kevin Buzzard]

When I upstream something I typically write "From the FLT project." as the last sentence of the PR description, but that's just to give us some idea of which parts of mathlib are "coming from FLT" -- one of the main arguments for funding FLT was that it would make mathlib better. What is the point of the label by the way? Cool that we have it :-) but does it mean that PRs from FLT are supposed to be treated differently to other PRs?

[Michael Rothgang]

It allows seeing e.g. all FLT-related PRs at a glance. Writing this into the PR description does the same, but is less apparent.

[Bryan Wang]

Yeah I've been writing "from FLT" in the PR description, and I wasn't sure what the label is for either, but now I find it really helpful to be able to filter all PRs by the label (e.g. one can double-check if there are any open PRs upstreaming the same thing)

[Bryan Gin-ge Chen]

It would be easy to add FLT to the list of tags that anyone can add / remove via PR comments. The code is here. (I'm also happy to do it if people think it'd be useful).

[Kevin Buzzard]

I'm fine with this. We have been working hard for the last year on a project which has just successfully finished, and one of my motivations for the project was that it would force us to develop a bunch of API for things already in mathlib, so now is a good time for mathlib to start reaping the benefits.

[Harald Husum]

Michael Rothgang said:

It allows seeing e.g. all FLT-related PRs at a glance.

Bryan Wang said:

[...] but now I find it really helpful to be able to filter all PRs by the label (e.g. one can double-check if there are any open PRs upstreaming the same thing)

To clarify, what is meant by this in practice is this: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+label%3AFLT

[Bryan Wang]

Harald Husum said:

To clarify, what is meant by this in practice is this: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+label%3AFLT

yep!

[Ruben Van de Velde]

It's also easier if you want to get statistics out at some point

[Bryan Gin-ge Chen]

Bryan Gin-ge Chen said:

It would be easy to add FLT to the list of tags that anyone can add / remove via PR comments. The code is here. (I'm also happy to do it if people think it'd be useful).

#34296 does this for FLT and a bunch of other downstream project related tags.

[Jakub Nowak]

The list in #contrib should be updated too. It says "This list is exhaustive. If you would like to add a different label, please, bring it up on Zulip!".

[Michael Rothgang]

Would you like to make a PR changing this? Simply edit this file.

[Bryan Gin-ge Chen]

Thanks for the reminder! Done in website#775.