Subcategories of Over

Stream: mathlib4

[Christian Merten]

A lot of categories appearing in algebraic geometry are full subcategories of Over X defined by some morphism property P, e.g. the category of schemes étale over X. I am thinking of what the best setup here is and I thought of the following:

import Mathlib.CategoryTheory.Comma.Over
import Mathlib.CategoryTheory.MorphismProperty.Basic

namespace CategoryTheory.MorphismProperty

section Comma

variable {A : Type*} [Category A] {B : Type*} [Category B] {T : Type*} [Category T]
  (L : A ⥤ T) (R : B ⥤ T)

/-- Given functors `L : A ⥤ T` and `R : B ⥤ T` and a morphism property `P` on `T`,
this is the predicate induced by `P` on objects of `Comma L R`. -/
def CommaPredicate (P : MorphismProperty T) (X : Comma L R) : Prop := P X.hom

/-- Given functors `L : A ⥤ T` and `R : B ⥤ T` and a morphism property `P` on `T`, this
is the full subcategory of `Comma L R` where `X : Comma L R` satisfies `P X.hom`. -/
protected def Comma (P : MorphismProperty T) : Type _ := FullSubcategory (P.CommaPredicate L R)

variable (P : MorphismProperty T)

instance : Category (P.Comma L R) := FullSubcategory.category (P.CommaPredicate L R)

/-- The forgetful functor from the full subcategory of `Comma L R` defined by `P` to `Comma L R`. -/
def Comma.forget : P.Comma L R ⥤ Comma L R :=
  fullSubcategoryInclusion (P.CommaPredicate L R)

end Comma

section Over

variable {C : Type*} [Category C]

/-- Given a morphism property `P` on a category `C` and an object `X : C`, this is the full
subcategory of `Over X` defined by `P`. -/
protected abbrev Over (P : MorphismProperty C) (X : C) : Type _ :=
  P.Comma (Functor.id C) (Functor.fromPUnit X)

variable (P : MorphismProperty C) (X : C)

/-- The forgetful functor from the full subcategory of `Over X` defined by `P` to `Over X`. -/
abbrev Over.forget : P.Over X ⥤ Over X :=
  MorphismProperty.Comma.forget (Functor.id C) (Functor.fromPUnit X) P

end Over

end CategoryTheory.MorphismProperty

A few thoughts on this:

• The reason why I think it is necessary to go via Comma is that, while in algebraic geometry we mostly consider Over X, this means in commutative algebra we will consider Under X. So to avoid doing everything twice, I suggest we do it in the generality of Comma.
• Can we get away with doing it via FullSubcategory or should we make the definition depend on two more morphism properties on A and B to carve out a not-necessarily full subcategory of Comma L R? In the common Over X case this would simply correspond to asking a second morphism property Q on the remaining morphism in the triangles. In AG it is quite common that the Ps we consider here have some cancellation property that automatically gives P for the third morphism in a triangle, so I am hoping FullSubcategory is sufficient. Of course we could also later restrict to a subcategory of P.Comma L R if we need it.

Any comments on the setup are very much appreciated.

[Johan Commelin]

FTR: I discussed this with Christian last Friday. Summary: let's start with FullSubcategory, and refactor if needed.