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.SphericalVarietyToric.Mathlib.RingTheory.AdjoinRoot- chore(Data/Quot): deprecate
ind*'APIs #16314 - feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers #26101
- Development branch (1) #27863
- chore(RingTheory): process porting notes, part 1 #29112
- feat(AdjoinRoot): bundle operations as
AlgHoms #29132 - weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
- chore(Data/Quot): deprecate
Toric.Mathlib.CategoryTheory.Monoidal.Grp_Toric.Mathlib.CategoryTheory.Monoidal.Mon_- feat(CategoryTheory/Monoidal): premonoidal categories #21488
- refactor: simplify
(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)to(f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)#26448 - chore: rename
Mon_ClasstoMonObj#28406 - WIP: experiment: bench
:= rflvs:= by rfl#29004 - feat: transfer
Mon_Classalong isomorphisms #29098 - feat: tensor product of group objects #29134
- feat:
(asIso f).homis a monoid hom iffis #29135 - feat(CategoryTheory/Monoidal):
mapMonof a lax-braided functor is lax-braided #29136
Toric.Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_Toric.Mathlib.RingTheory.TensorProduct.Basic- feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product #22898
- feat(RingTheory/Finiteness/Small): tensor product of the system of small submodules #22908
- feat(RingTheory/Pure): pure submodules #22909
- feat(LinearAlgebra):
tensor_inductionmacro #25208 - chore: refactor Algebra.TensorProduct.rightAlgebra #25481
- feat(RingTheory): meta properties of bijective ring homomorphisms #28695
- feat(TensorProduct):
lTensoras anAlgHomand other lemmas #28973 - chore: deprime
inductionin some ofRingTheory#29127 - chore: make
SMulCommClass A A BandSMulCommClass A B Bhigher priority #7875
Toric.Mathlib.RingTheory.Coalgebra.GroupLikeToric.Mathlib.RingTheory.Coalgebra.SimpAttrToric.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: enable the flexible linter in mathlib #28962
Toric.Mathlib.Algebra.AffineMonoid.IrreducibleToric.Mathlib.Algebra.AffineMonoid.EmbeddingToric.Mathlib.Algebra.Category.CommBialgCatToric.Mathlib.Algebra.MonoidAlgebra.ModuleToric.Mathlib.Algebra.MonoidAlgebra.Basic- chore(Algebra.Polynomial): split
Polynomial/Basic.leaninto smaller files #19097 - chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in
Basic.lean#19281 - chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
- feat: Lindemann-Weierstrass Theorem #28013
- feat(MonoidAlgebra):
mapRangeas anAlgHom#28956 - chore(Algebra/MonoidAlgebra): use
to_additiveforAddMonoidAlgebra#29036 - refactor: make the algebra hierarchy use flat structures #3171
- chore: use
open scoped#4960 - fix: deduplicate variables #6079
- chore: make
SMulCommClass A A BandSMulCommClass A B Bhigher priority #7875 - refactor: allow non-unital
AlgEquiv#8686
- chore(Algebra.Polynomial): split
Toric.Mathlib.Algebra.Group.TypeTags.HomToric.Mathlib.Geometry.Convex.Cone.Pointed
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