Upstreaming dashboard

The eventual goal of the Toric project is to be fully upstreamed to Mathlib.

As such, it is crucial to continuously organise upstreaming from Toric to Mathlib. The way we organise this is with the following two lists, showing files with no Toric dependencies depending on whether they contain sorry or not.

Files ready to upstream

The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.

PRs are grouped as 'relevant' if they contain the following label: toric

Toric.Mathlib.Algebra.Polynomial.Bivariate

9 open pull requests (1 with relevant labels)

Relevant

• refactor(Polynomial/Bivariate): swap `X` and `Y` for improved notation #27196
  WIP, t-algebra, toric

Other

• feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
  t-algebra, t-number-theory, blocked-by-other-PR, merge-conflict, t-algebraic-geometry
• feat(EllipticCurve): the universal elliptic curve #13847
  merge-conflict, awaiting-author, t-algebra, t-algebraic-geometry
• feat: Group scheme structure on Weierstrass curve #14167
  merge-conflict, WIP, t-algebraic-geometry, workshop-AIM-AG-2024
• feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
  t-algebraic-geometry, blocked-by-other-PR
• ignore this: Lean pr testing 9124 #26581
  merge-conflict
• trying #28803 using lean#10178 #29741
  merge-conflict
• Nagell lutz #35863
  merge-conflict
• feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
  t-algebra, awaiting-author

Toric.Mathlib.RingTheory.AdjoinRoot

10 open pull requests (0 with relevant labels)

Other

• chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
  merge-conflict, WIP, t-algebra
• chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
  merge-conflict, awaiting-author, t-algebra
• feat: more linting of cdots #12411
  merge-conflict, t-linter
• Clean up quotient APIs #16210
  merge-conflict, tech debt, blocked-by-other-PR, t-data
• chore(Data/Quot): deprecate `ind*'` APIs #16314
  merge-conflict, t-data
• chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
  t-algebra, awaiting-author, merge-conflict
• feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
  t-algebraic-geometry, blocked-by-other-PR
• refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
  t-algebra, awaiting-author, merge-conflict
• feat(RingTheory/AdjoinRoot): add IsFractionRing for AdjoinRoot #35157
  t-ring-theory, t-algebra, awaiting-author
• feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
  t-algebra, awaiting-author

Toric.Mathlib.RingTheory.Coalgebra.SimpAttr

No open pull requests.

Toric.Mathlib.RingTheory.TensorProduct.Maps

2 open pull requests (0 with relevant labels)

Other

• feat(RingTheory): a finite étale algebra is étale locally finite split #36398
  t-ring-theory, large-import, blocked-by-other-PR
• feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to `1` #36399
  t-ring-theory

Files easy to unlock

The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.