mathlib

mathlib copied to clipboard

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint

1

--- - [x] depends on: #15796 - [x] depends on: #15797 - [x] depends on: #15858 [](https://gitpod.io/from-referrer/)

TwoFX

feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete

1

This corollary of the special adjoint functor theorem immediately implies that Grothendieck categories are complete, which, according to the Wikipedia article on Grothendieck categories, is "a rather deep result". ---...

TwoFX

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

Ruben-VandeVelde

feat(algebra/category): forgetful functors from modules/abelian groups preserve epis/monos

1

The corresponding `reflects` statements already follow from faithfulness. --- - [x] depends on: #14829 - [x] depends on: #15107 [](https://gitpod.io/from-referrer/)

TwoFX

--- This PR proves the L¹ martingale convergence theorem and as a corollary, also the Lévy upwards theorem. [](https://gitpod.io/from-referrer/)

kex-y

A few variables could be made implicit in some of the lemmas in `ring_theory/chain_of_divisors`. I also made a (very) minor stylistic change to a proof from one of my previous...

Paul-Lez

refactor(data/finset/fin): Delete `finset.fin_range`

11

`finset.fin_range n` is just `finset.univ`, so we inline its definition in the `fintype (fin n)` instance to avoid people trying to use it. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(category_theory/preadditive): inclusion functor from left exact functors to additive functors

1

--- - [x] depends on: #12014 - [x] depends on: #12330 - [x] depends on: #12336 [](https://gitpod.io/from-referrer/)

TwoFX

In this PR, we obtain the basic behaviour of lifting properties with respect to adjunctions. --- [](https://gitpod.io/from-referrer/)

joelriou

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group

2

In this file we define `lipschitz` , `pin_group` and `spin_group`. Here are some discussion about the latent ambiguity of definition : https://mathoverflow.net/q/427881/172242 and https://mathoverflow.net/q/251288/172242 The definition of the Lipschitz group...

Biiiilly