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.MvLaurentPolynomial
• Toric.SphericalVariety
• Toric.Hopf.CommAlg
• Toric.MonoidObjectAction.Basic
• Toric.ConvexAnalysis.Polytope
• Toric.ConvexAnalysis.PolyhedralCone
• Toric.Mathlib.CategoryTheory.ChosenFiniteProducts
  • feat(CategoryTheory/ChosenFiniteProducts): Added basic ChosenFiniteCoproducts class #21603
  • feat: the essential image of a finite product-preserving functor is cartesian-monoidal #23562
• Toric.Mathlib.CategoryTheory.Yoneda
  • feat(CategoryTheory/Sites): global sections functor on sheaves #22816
• Toric.Mathlib.CategoryTheory.Monoidal.Functor
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
  • chore(CategoryTheory/Monoidal/Functor): remove erws #23771
• Toric.Mathlib.CategoryTheory.Comma.Over.Basic
  • feat(CategoryTheory): ChosenFiniteProducts (Over X) #21399
  • feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) #21525
  • feat(CategoryTheory): Locally Cartesian Closed Categories (Sections Right Adjoint) #22319
  • feat(CategoryTheory): Locally Cartesian Closed Categories (Definition) #22321
  • feat(CategoryTheory): Locally Cartesian Closed Categories (Beck-Chevalley Conditions) #22340
  • feat: the category over a terminal object #23702
• Toric.Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
  • feat: a binary fan in Over X is the same thing as a pullback cone to X #23723
• Toric.Mathlib.RingTheory.Bialgebra.Basic
  • feat: bialgebra structure from algebra homs #23695
• Toric.Mathlib.RingTheory.Bialgebra.MonoidAlgebra
  • feat(Bialgebra/MonoidAlgebra): mapDomain as a BialgHom #23722
• Toric.Mathlib.Algebra.Group.Torsion
  • feat: torsion-free monoids #22962
• Toric.Mathlib.Algebra.Module.LinearMap.End
  • chore: move Module.End-related decls to the Module.End namespace #23705
  • chore: make SMulCommClass A A B and SMulCommClass A B B higher priority #7875
• Toric.Mathlib.Algebra.Category.Grp.Basic
  • chore: replace many occurrences of => arrows for anonymous functions #19576
  • refactor(CategoryTheory/Limits): colimits in Type #23364
• Toric.Mathlib.Algebra.Category.MonCat.Basic
  • refactor(CategoryTheory/Limits): colimits in Type #23364
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.Algebra.Group.TypeTags.Basic
  • feat: ℕ+ powers in semigroups #22517
• Toric.Mathlib.Algebra.Group.Irreducible.Defs
  • feat: additivise Irreducible #22904
• Toric.Mathlib.LinearAlgebra.LinearIndependent.Defs
  • chore(LinearIndependent): rename linearCombination lemmas #23045
  • chore(LinearAlgebra): generalize some lemmas #23729
• Toric.Mathlib.LinearAlgebra.FreeModule.Finite.Basic
• Toric.Mathlib.GroupTheory.MonoidLocalization.DivPairs
  • feat: submonoid of pairs with quotient in a submonoid #22635
• Toric.Mathlib.Data.Fintype.EquivFin
  • refactor: spell results using Minimal/MinimalWrt #23487

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.Mathlib.CategoryTheory.ChosenFiniteProducts.Over 1 sorry
• Toric.Mathlib.CategoryTheory.Limits.Preserves.Basic 2 sorries
• Toric.Mathlib.RingTheory.Bialgebra.Hom 4 sorries
• Toric.Mathlib.RingTheory.HopfAlgebra.Basic 1 sorry
• Toric.Mathlib.LinearAlgebra.TensorProduct.Basic 1 sorry