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 the keyword sorry or not.
Files ready to upstream
The following files are sorry-free and do not depend on any other Toric file, meaning they can be readily PRed to Mathlib.
Toric.ImportsToric.SphericalVarietyToric.Mathlib.RingTheory.AdjoinRoot- chore(Data/Quot): deprecate
ind*'APIs #16314 - refactor(Algebra/Algebra/Equiv): allow for non-unital
AlgEquiv#29354 - chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas #31817
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
- chore(Data/Quot): deprecate
Toric.Mathlib.RingTheory.Coalgebra.SimpAttrToric.Mathlib.RingTheory.TensorProduct.Maps- refactor(Algebra/Algebra/Equiv): allow for non-unital
AlgEquiv#29354 - feat(Algebra/Category/Ring): equalizers of pushout maps of tensor product inclusions #29960
- feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ #30204
- feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes #30811
- refactor(Algebra/Algebra/Equiv): allow for non-unital
Toric.Mathlib.Algebra.Polynomial.Bivariate- feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
- feat(EllipticCurve): the universal elliptic curve #13847
- feat: Group scheme structure on Weierstrass curve #14167
- refactor(Polynomial/Bivariate): swap
XandYfor improved notation #27196 - chore: tidy flexible linter exceptions #32232
Files easy to unlock
The following files do not depend on any other Toric file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.
Toric.ToricIdeal3 sorries