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.CategoryTheory.Monoidal.Attr
• 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.CategoryTheory.Monoidal.Cartesian.Basic
  • feat: Mon_ C is cartesian-monoidal if C is #25326
  • the homotopy category functor preserves products #25780
  • 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.Algebra.Category.CommBialgCat
  • feat: the category of commutative bialgebras #27120
• Toric.Mathlib.Algebra.MonoidAlgebra.Lift
  • chore(Algebra.Polynomial): split Polynomial/Basic.lean into smaller files #19097
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • feat(MonoidAlgebra): mapDomain and mapRange as ring homs #23999
• Toric.Mathlib.Algebra.MonoidAlgebra.Module
  • chore(Algebra.Polynomial): split Polynomial/Basic.lean into smaller files #19097
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
• 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: add bundled versions of Equiv.cast #27182
  • feat(RingTheory/GradedAlgebra): homogeneous relation #27307
  • refactor: make ⇑e⁻¹ = e.symm simp #27433
  • refactor: state hypotheses of BialgHom.ofAlgHom as equalities of AlgHoms #28142
  • chore(Mathlib): replace => by ↦ #28622
  • 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.AffineMonoid.Embedding
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.AffineMonoid.Irreducible
  • feat: affine monoids #24912
• 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
• Toric.Mathlib.Algebra.Group.TypeTags.Hom
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat: MonoidHom.toAdditive'' as a MulEquiv #27047
• Toric.Mathlib.RingTheory.Bialgebra.Equiv
  • refactor: deprecate MulEquivClass #18806
  • refactor: state hypotheses of BialgHom.ofAlgHom as equalities of AlgHoms #28142
• Toric.Mathlib.RingTheory.Bialgebra.Hom
  • chore: deprecate BialgHom.coe_toLinearMap #28141
  • refactor: state hypotheses of BialgHom.ofAlgHom as equalities of AlgHoms #28142
• 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
  • chore: make SMulCommClass A A B and SMulCommClass A B B higher priority #7875
• Toric.Mathlib.RingTheory.Coalgebra.SimpAttr
• Toric.Mathlib.RingTheory.Coalgebra.GroupLike
  • feat(RingTheory): group-like elements #24730
• Toric.Mathlib.Geometry.Convex.Polytope
  • feat: polytopes #23940
• Toric.Mathlib.Geometry.Convex.Cone.Pointed
  • refactor: make the cone explicit in ConvexCone.toPointedCone #28139
  • feat: a PointedCone-valued version of Submodule.span #28140

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