Commit 2024-10-24 04:49 c46a2f18

feat(CategoryTheory/Comma): subcategory defined by morphism properties (#18088) Given functors L : A ⥤ T and R : B ⥤ T and morphism properties P, Q and W on T, A and B respectively, we define the subcategory P.Comma L R Q W of Comma L R where

• objects are objects of Comma L R with the structural morphism satisfying P, and
• morphisms are morphisms of Comma L R where the left morphism satisfies Q and the right morphism satisfies W. For an object X : T, this specializes to P.Over Q X which is the subcategory of Over X where the structural morphism satisfies P and where the horizontal morphisms satisfy Q. Common examples of the latter are e.g. the category of schemes étale (finite, affine, etc.) over a base X. Here Q = ⊤.