functions in full subcategories

Stream: maths

[Matthew Ballard]

In docs#category_theory.full_subcategory, a function F : C → D is used to specify the objects of the subcategory. What is the use case for having this instead of a subtype?

[Reid Barton]

You might not want to set up the objects of C as a literal subtype for whatever technical reason, for example
https://github.com/leanprover-community/mathlib/blob/ae7a88d1bf0fbd4978e6e0d20000a25712b94284/src/topology/category/CompHaus/default.lean#L35-L49

[Matthew Ballard]

So C is perhaps carrying some extra structure which F loses but in general is helpful? So C packages data more efficiently than passing via F to D?

[Reid Barton]

Usually F will be an injective function I think (though it doesn't have to be), it's just that in Lean we cannot replace an injective function "for free" with the inclusion of a subtype (subtype.val) like in ordinary math, so since the definition works exactly the same way with F in place of subtype.val, we might as well state it in "extra generality".

[Reid Barton]

The point is you might already have an idea of what the objects of C are meant to be, and that might not happen to be literally a subtype of the objects of D.

[Matthew Ballard]

Thanks.

[Junyan Xu]

full_subcategory is realized as a special case of induced_category in that file. Induced category structures may not come up often in mathematics, but in Lean they can be quite convenient. For example, if the subtype is the range of a function, it's much easier to work with the function directly than working with the range, which involves an existential quantifier and an equality. This happens for the subcategory of basic open sets inside the category of all open sets in the spectrum of a ring R; the set of basic opens is the range of the function sending r : R to D(r). In #9802, I need to work with B-sheaves, which are (contravariant) functors from the basic opens to a value category, and it turned out it's much easier to work with functors from R to the value category, where R is equipped with the induced category structure (from the category of open sets).