Christian Merten

feat(CategoryTheory/Action): category of continuous actions

4

Introduces the category `ContAction V G` for any concrete category `V` with a forgetful functor to `TopCat` and monoid `G`. It is realized as a full subcategory of `Action V...

feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups

1

We show that the automorphism group of a fiber functor is isomorphic to the limit of the automorphism groups of all Galois objects. From this we deduce that the automorphism...

feat(RingTheory/Localization): localization of algebra maps and commutation with kernels

2

Adds API for localizing algebra maps, in general form and specialized to `IsLocalization.Away`. Also shows that localization commutes with kernels. --- [](https://gitpod.io/from-referrer/)

feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API

2

Adds a `MorphismProperty.stalkwise` constructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for...

feat(CategoryTheory/Comma): limit properties of subcategories defined by morphism properties

2

We show that under suitable assumptions on `P` the full subcategory of `Over X` defined by `P` has terminal objects and pullbacks. --- - [x] depends on: #18088 [![Open in...

feat(CategoryTheory): criterion for `ObjectProperty.ind` in finitely accessible categories

3

We show that if `C` is finitely accessible and `P` implies finitely presentable, then `X` satisfies `ind P` if and only if every morphism `Z ⟶ X` from a finitely...