mathlib4

mathlib4 copied to clipboard

chore (Algebra.PUnitInstances): split file into `Algebra`, `Order`, and `Module` instance files

1

When we need algebra structures on `PUnit`, we should be more surgical about what we are importing. --- [](https://gitpod.io/from-referrer/)

mattrobball

feat(CategoryTheory): triangulated functors are additive

1

--- [](https://gitpod.io/from-referrer/)

joelriou

feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem

1

This proves the first step of the proof of the Archimedean case of Ostrowski's Theorem, namely that a rational absolute value `f : MulRingNorm ℚ` that is not bounded, i.e....

amosturchet

Feat(AlgebraicGeometry/FromSpecStalk): Given a scheme `X` and a point `x : X`, the canonical scheme morphism from `Spec(O_x)` to `X`.

4

In this pull request, we define: Given a scheme `X` and a point `x : X.carrier`, `AlgebraicGeometry.Scheme.fromSpecStalk X x` is the canonical scheme morphism from `Spec(O_x)` to `X`. This is...

FMLJohn

feat(CategoryTheory): the monoidal category structure on graded objects

2

Under suitable conditions on a monoidal category `C`, we define an instance of `MonoidalCategory (GradedObject ℕ C)`. The construction is actually more general, and it shall be used in order...

joelriou

feat(CategoryTheory/Monoidal): Hopf monoids

2

Defines Hopf monoids in a braided category. Proves two facts (antipode is an antihomomorphism, morphisms intertwine antipode) that are not yet proved for unbundled Hopf algebras. Once we prove `Hopf_...

kim-em

feat: definition of Ext-groups in abelian categories

2

This PR defines Ext-groups in general abelian categories by shrinking types of morphisms in the derived category. (When this API is developed further, it shall replace the current definition which...

joelriou

feat: topology on ring of finite adeles.

1

Use `SubmodulesRingBasis` to put a topology on the finite adeles. --- Remark: when this work was WIP and depended on other PRs it was #13703 (with no reviewer comments). Now...

kbuzzard

feat(RingTheory): Surjective on stalks ring homomorphisms.

1

--- [](https://gitpod.io/from-referrer/)

erdOne

PR into lwithfield-Lie-theorem

1

--- [](https://gitpod.io/from-referrer/)

jcommelin