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.MvLaurentPolynomial
• Toric.Mathlib.GroupTheory.FreeAbelianGroup
  • chore(Data/Quot): deprecate ind*' APIs #16314
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.Geometry.Convex.Polytope
  • feat: polytopes #23940
• Toric.Mathlib.Geometry.Convex.Cone.Pointed
  • refactor(Convex/Cone): reorder, streamline #24149
  • chore: move pointed cones, proper cones #25251
• Toric.Mathlib.CategoryTheory.Monoidal.Functor
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
• Toric.Mathlib.CategoryTheory.Monoidal.Category
  • feat(CategoryTheory/Limits/Sifted): characterization of sifted categories #17781
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
  • feat: notation for whisker(Left/Right)Iso #22698
• Toric.Mathlib.CategoryTheory.Monoidal.CommMon_
  • feat: F.obj M is a commutative monoid object if M is #25327
  • fix: deduplicate variables #6079
• Toric.Mathlib.CategoryTheory.Functor.FullyFaithful
  • feat(AlgebraicGeometry): relative gluing of schemes #18284
• Toric.Mathlib.CategoryTheory.Monoidal.Cartesian.Over
• Toric.Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  • feat: Mon_ C is cartesian-monoidal if C is #25326
• 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.LinearAlgebra.TensorProduct.Basic
  • chore: attribute [induction_eliminator] #12605
  • chore: semilinearize LinearAlgebra.TensorProduct.Basic #24208
  • feat(LinearAlgebra): tensor_induction macro #25208
• Toric.Mathlib.LinearAlgebra.PerfectPairing.Basic
  • refactor: redefine perfect pairings as a Prop-valued typeclass #25239
• Toric.Mathlib.Algebra.AffineMonoid.Embedding
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.FreeAbelianGroup.Finsupp
• 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
  • feat: Finsupp.linearCombination MonoidAlgebra.of = id #25273
• Toric.Mathlib.Algebra.Algebra.Defs
  • feat(CategoryTheory/Subobject): add formalization of subobject classifier #22245
  • Mr librarynote def 2b #23786
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • chore: make IsScalarTower A A B and IsScalarTower A B B higher priority #7874
• Toric.Mathlib.Algebra.Algebra.Hom
  • Mr librarynote def 2b #23786
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat(Algebra/AlgHom): Unique if target is Subsingleton #24379
  • feat: promote an AlgEquiv preserving counit and comul to a BialgEquiv #25271
  • refactor: make the algebra hierarchy use flat structures #3171
  • chore: use open scoped #4960
  • refactor: Use flat structures for morphisms #6791
  • weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
• Toric.Mathlib.Algebra.Category.MonCat.Basic
  • refactor(CategoryTheory/Limits): colimits in Type #23364
  • feat: multicoequalizers in the category of types #23872
  • feat: CommGrp-valued Yoneda embedding #24778
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.Algebra.Category.Grp.Basic
  • refactor(CategoryTheory/Limits): colimits in Type #23364
  • feat: multicoequalizers in the category of types #23872
  • feat: CommGrp-valued Yoneda embedding #24778
• Toric.Mathlib.Algebra.Category.CommAlgCat.Monoidal
  • feat: CommAlgCat is cocartesian-monoidal #25365
• Toric.Mathlib.Algebra.Order.Nonneg.Module
  • feat(Algebra/Order/Nonneg): A finite module is finite over the nonnegative scalars #24450
• Toric.Mathlib.Algebra.Group.Irreducible.Defs
  • feat: affine monoids #24912
  • feat: if p = a * b is irreducible, then a = 1 or b = 1 #24913
• Toric.Mathlib.Algebra.Group.TypeTags.Hom
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat: add autoparams for proof fields of Equiv #25350
• 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 #25290
  • feat: Add high-level generalizations from MonoidHom lifts #25296
• Toric.Mathlib.RingTheory.Coalgebra.SimpAttr
• Toric.Mathlib.RingTheory.Bialgebra.Hom
• Toric.Mathlib.RingTheory.Bialgebra.Equiv
  • refactor: deprecate MulEquivClass #18806
  • feat: promote an AlgEquiv preserving counit and comul to a BialgEquiv #25271
• Toric.Mathlib.RingTheory.Bialgebra.GroupLike
  • feat(Bialgebra): group-like elements #24730
• Toric.Mathlib.RingTheory.HopfAlgebra.Basic
  • feat: counit (antipode a) = counit a #25267
• Toric.Mathlib.RingTheory.TensorProduct.Basic
  • feat: topology on Hom(R, S) in CommRingCat #21283
  • chore(RingTheory/TensorProduct): cleanup #22532
  • 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
  • refactor(RingTheory/RingHom): factor out proofs for Algebra.FinitePresentation #22930
  • feat(RingTheory): degree of rational function field extension #22966
  • 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

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