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.SphericalVariety
• Toric.Mathlib.RingTheory.FiniteType
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • feat(RingTheory/Presentation): core of a presentation #24794
  • feat(RingTheory): smooth algebras have smooth Noetherian models #25143
  • refactor: use Algebra.FiniteType as a class #27030
• Toric.Mathlib.CategoryTheory.Monoidal.Attr
• Toric.Mathlib.CategoryTheory.Monoidal.Grp_
  • refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure #26446
• Toric.Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  • feat: Mon_ C is cartesian-monoidal if C is #25326
  • refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure #26446
  • refactor: simplify (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) to (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) #26448
• Toric.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
  • feat(CategoryTheory/Limits/Preserves/Shapes): show that if a functor preserves limits, so does Over.post #24804
• Toric.Mathlib.Geometry.Convex.Polytope
  • feat: polytopes #23940
• Toric.Mathlib.Geometry.Convex.Cone.Pointed
• Toric.Mathlib.LinearAlgebra.PerfectPairing.Basic
  • refactor: redefine perfect pairings as a Prop-valued typeclass #25239
• Toric.Mathlib.RingTheory.Bialgebra.Hom
• Toric.Mathlib.RingTheory.Bialgebra.Equiv
  • refactor: deprecate MulEquivClass #18806
• Toric.Mathlib.RingTheory.Coalgebra.SimpAttr
• Toric.Mathlib.RingTheory.Coalgebra.GroupLike
  • feat(RingTheory): group-like elements #24730
• Toric.Mathlib.RingTheory.HopfAlgebra.Basic
  • feat: counit (antipode a) = counit a #25267
• 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_induction macro #25208
  • chore: refactor Algebra.TensorProduct.rightAlgebra #25481
  • feat: upgrade lflip to a LinearEquiv #27544
  • chore: make SMulCommClass A A B and SMulCommClass A B B higher priority #7875
• 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 X and Y for improved notation #27196
  • feat(Bivariate): aevalAeval and swap #27636
• Toric.Mathlib.Algebra.MonoidAlgebra.Defs
  • chore(Algebra/MonoidAlgebra): split Defs.lean further #19091
  • chore(Algebra.Polynomial): split Polynomial/Basic.lean into smaller files #19097
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • refactor: make MonoidAlgebra into a one-field structure #25273
  • chore: golf Algebra/ using grind #26726
  • chore: golf Algebra/ using exact #26782
  • linter indentation playground: do not merge #27490
• Toric.Mathlib.Algebra.AffineMonoid.Embedding
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.AffineMonoid.Irreducible
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.Category.CommBialgCat
  • feat: the category of commutative bialgebras #27120
• Toric.Mathlib.Algebra.Algebra.Equiv
  • feat(RingTheory/Pure): pure submodules #22909
  • Mr librarynote def 2b #23786
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
  • feat: add bundled versions of Equiv.cast #27182
  • feat(RingTheory/GradedAlgebra): homogeneous relation #27307
  • feat(FieldTheory/Finite): minimal polynomial of Frobenius #27368
  • feat(FieldTheory/Galois): normal basis theorem #27390
  • feat(Algebra/Algebra/Equiv): e (e⁻¹ x) = x #27433
  • refactor: make the algebra hierarchy use flat structures #3171
  • chore: use open scoped #4960
  • refactor: Use flat structures for morphisms #6791
  • refactor: allow non-unital AlgEquiv #8686
• Toric.Mathlib.Algebra.Group.Units.Hom
  • chore: get rid of generic hom coercions #21031
  • Mr librarynote def 2b #23786
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • refactor: Make IsLocalHom take unbundled map #24965
  • feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
  • feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
  • feat(Algebra/Group/Units/Hom): add map lemmas #25993
  • feat(Algebra/Group/Prod): Add API for inclusion and projection maps from and to the product of units. #26010
  • feat: MonoidHom.toHomUnits is a monoid hom #27210
• Toric.Mathlib.Algebra.Group.TypeTags.Hom
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
  • feat: MonoidHom.toAdditive'' as a MulEquiv #27047
• Toric.Mathlib.Algebra.Group.Equiv.Basic
  • refactor: deprecate MulEquivClass #18806
  • chore: get rid of generic hom coercions #21031
  • feat: (M →* N₁) ≃* (M →* N₂) if N₁ ≃* N₂ #25182
  • feat: Low-level derivatives of lifts on OneHom, MulHom and MonoidHom #26012
  • feat: Add high-level generalizations from MonoidHom lifts #26015
  • feat: some measure-theoretic properties of the unitInterval #27748
  • chore: further >6month old deprecations #27799

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.ToricIdeal 3 sorries
• Toric.Util.TrackSorry 17 sorries