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
Toric.Mathlib.CategoryTheory.Monoidal.Attr
Toric.Mathlib.CategoryTheory.Monoidal.Grp_
Toric.Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Toric.Mathlib.CategoryTheory.Comma.Over.OverClass
Toric.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
Toric.Mathlib.Geometry.Convex.Polytope
Toric.Mathlib.Geometry.Convex.Cone.Pointed
Toric.Mathlib.LinearAlgebra.PerfectPairing.Basic
Toric.Mathlib.RingTheory.Bialgebra.Hom
Toric.Mathlib.RingTheory.Bialgebra.Equiv
Toric.Mathlib.RingTheory.Coalgebra.SimpAttr
Toric.Mathlib.RingTheory.Coalgebra.GroupLike
Toric.Mathlib.RingTheory.HopfAlgebra.Basic
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 - fix(LinearAlgebra/TensorProduct): fix
⊗ₜ[R]
precedence #27589 - fix(LinearAlgebra/TensorProduct): fix
⊗[R]
precedence #27590 - chore: make
SMulCommClass A A B
andSMulCommClass A B B
higher priority #7875
Toric.Mathlib.Algebra.Polynomial.Bivariate
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
Toric.Mathlib.Algebra.AffineMonoid.Irreducible
Toric.Mathlib.Algebra.Category.CommBialgCat
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 - chore: Clean up typos using OpenAI’s GPT-4.1 mini (verified by human) #27532
- 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
Toric.Mathlib.Algebra.Group.Equiv.Basic
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 sorriesToric.Util.TrackSorry
17 sorries