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
• Toric.Mathlib.GroupTheory.FreeAbelianGroup
  • chore(Data/Quot): deprecate ind*' APIs #16314
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.LinearAlgebra.UnitaryGroup
  • feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group #12799
  • feat: trace of unitarily similar matrices #24793
  • refactor(*): migrate from Matrix.toLin' to Matrix.mulVecLin #25012
• Toric.Mathlib.AlgebraicGeometry.Scheme
  • Mr librarynote def 2b #23786
  • refactor: Make IsLocalHom take unbundled map #24965
  • feat(AlgebraicGeometry): building morphisms into Proj #25101
  • feat(AlgebraicGeometry): Add global preorder instance for schemes #26204
  • feat(AlgebraicGeometry): Add some minimal API for orders on schemes #26225
  • feat(AlgebraicGeometry): Definition of algebraic cycles #26304
• Toric.Mathlib.AlgebraicGeometry.GammaSpecAdjunction
• Toric.Mathlib.RingTheory.Finiteness.Finsupp
  • feat(LinearAlgebra/Contraction): bijectivity of dualTensorHom + generalize to CommSemiring #25284
• Toric.Mathlib.RingTheory.HopfAlgebra.Basic
  • feat: counit (antipode a) = counit a #25267
• Toric.Mathlib.RingTheory.Coalgebra.GroupLike
  • feat(RingTheory): group-like elements #24730
• Toric.Mathlib.RingTheory.Coalgebra.SimpAttr
• 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.Hom
• 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(RingTheory): degree of rational function field extension #26316
  • chore: make SMulCommClass A A B and SMulCommClass A B B higher priority #7875
• Toric.Mathlib.Geometry.Convex.Polytope
  • feat: polytopes #23940
• Toric.Mathlib.Geometry.Convex.Cone.Pointed
• Toric.Mathlib.Data.Finsupp.Single
  • chore(Algebra.Polynomial): split Polynomial/Basic.lean into smaller files #19097
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • chore(Algebra/Notation): separate very basic lemmas about Set.indicator and Pi.single #24998
  • chore(Finsupp): move order properties under Order #25002
  • feat(Data/Finsupp/Basic): Finsupp.optionElim' #25920
• Toric.Mathlib.CategoryTheory.Functor.FullyFaithful
  • feat(AlgebraicGeometry): relative gluing of schemes #18284
• Toric.Mathlib.CategoryTheory.Monoidal.Grp_
• Toric.Mathlib.CategoryTheory.Monoidal.Mod_
  • refactor(CategoryTheory/Monoidal/Mod_): refactor Mod_ using MonoidalLeftAction #25762
• Toric.Mathlib.CategoryTheory.Monoidal.CommMon_
  • feat: F.obj M is a commutative monoid object if M is #25327
  • refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure #26446
  • fix: deduplicate variables #6079
• Toric.Mathlib.CategoryTheory.Monoidal.Category
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
  • feat: notation for whisker(Left/Right)Iso #22698
  • 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.Monoidal.Functor
  • feat(CategoryTheory/Monoidal): premonoidal categories #21488
  • refactor: simplify (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) to (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) #26448
• Toric.Mathlib.CategoryTheory.Monoidal.Attr
  • feat: Mon_ C is cartesian-monoidal if C is #25326
• Toric.Mathlib.CategoryTheory.Comma.Over.Basic
  • 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
• Toric.Mathlib.CategoryTheory.Comma.Over.OverClass
  • Mr librarynote def 2b #23786
• 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.Over
• 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.Algebra.AffineMonoid.Embedding
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.AffineMonoid.Irreducible
  • feat: affine monoids #24912
• Toric.Mathlib.Algebra.Group.Finsupp
  • chore(Algebra/Notation): separate very basic lemmas about Set.indicator and Pi.single #24998
  • chore(Finsupp): move order properties under Order #25002
• Toric.Mathlib.Algebra.FreeAbelianGroup.Finsupp
• 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
  • Development branch (1) #26139
  • chore: make IsScalarTower A A B and IsScalarTower A B B higher priority #7874
• Toric.Mathlib.Algebra.Algebra.Equiv
  • feat(RingTheory/GradedAlgebra): homogeneous relation #22279
  • feat(RingTheory/Pure): pure submodules #22909
  • 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
  • feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
  • 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.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.Polynomial.AlgebraMap
  • chore(Algebra/{MonoidAlgebra,Polynomial}): algebra structure in Basic.lean #19281
  • chore(*): fix nmem vs not_mem names #24409
  • Development branch (1) #26139
• 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.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
• 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
• 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
• Toric.Mathlib.Algebra.Category.Grp.Basic
  • feat: multicoequalizers in the category of types #23872
  • refactor(CategoryTheory/Limits): colimits in Type #25823
• Toric.Mathlib.Algebra.Category.CommAlgCat.Monoidal
  • feat: CommAlgCat is cocartesian-monoidal #25365
• Toric.Mathlib.Algebra.Category.MonCat.Basic
  • feat: multicoequalizers in the category of types #23872
  • refactor(CategoryTheory/Limits): colimits in Type #25823
  • refactor: Use flat structures for morphisms #6791
• Toric.Mathlib.GroupTheory.FreeGroup.Basic
  • refactor: generalize MonoidHom.ker and MonoidHom.range to MonoidHomClass #10075
  • feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words #22639
  • chore(Algebra/Notation): separate very basic lemmas about Set.indicator and Pi.single #24998
• Toric.Mathlib.LinearAlgebra.PerfectPairing.Basic
  • refactor: redefine perfect pairings as a Prop-valued typeclass #25239
• Toric.Mathlib.LinearAlgebra.Finsupp.VectorSpace
  • refactor(*): migrate from Matrix.toLin' to Matrix.mulVecLin #25012
• Toric.Mathlib.LinearAlgebra.TensorProduct.Basic
  • chore: attribute [induction_eliminator] #12605
  • chore: semilinearize LinearAlgebra.TensorProduct.Basic #24208
  • feat(LinearAlgebra): tensor_induction macro #25208
  • feat(RingTheory/Regular): flat base change of weakly regular sequence #26106
  • feat(RingTheory): lemmas about TensorProduct and IsBaseChange #26297

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.Util.TrackSorry 17 sorries