3.8. Full subcategories
If C is a category, there is a type ObjectProperty C of properties
of objects of C, i.e. predicates C → Prop. For example, if X is an
object of a category C, one may define the property of objects of C
that are isomorphic to X, show that this property is closed
under isomorphisms, and that it is the closure under isomorphisms of
the property of objects that is only satisfied by X:
variable (X : C)
def isIsomorphicTo : ObjectProperty C :=
fun Y ↦ Nonempty (X ≅ Y)
instance :
(isIsomorphicTo X).IsClosedUnderIsomorphisms where
of_iso := C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ ∀ {X_1 Y : C} (x : X_1 ≅ Y), isIsomorphicTo X X_1 → isIsomorphicTo X Y
C:Type u_1inst✝:Category.{v_1, u_1} CX:CX✝:CY✝:Ce₁:X✝ ≅ Y✝e₂:X ≅ X✝⊢ isIsomorphicTo X Y✝
All goals completed! 🐙
example :
isIsomorphicTo X =
(ObjectProperty.singleton X).isoClosure := C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ isIsomorphicTo X = (ObjectProperty.singleton X).isoClosure
C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ isIsomorphicTo X ≤ (ObjectProperty.singleton X).isoClosureC:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ (ObjectProperty.singleton X).isoClosure ≤ isIsomorphicTo X
C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ isIsomorphicTo X ≤ (ObjectProperty.singleton X).isoClosure C:Type u_1inst✝:Category.{v_1, u_1} CX:Ci✝:Ce:X ≅ i✝⊢ (ObjectProperty.singleton X).isoClosure i✝
exact ⟨X, C:Type u_1inst✝:Category.{v_1, u_1} CX:Ci✝:Ce:X ≅ i✝⊢ ObjectProperty.singleton X X All goals completed! 🐙, ⟨e.symm⟩⟩
C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ (ObjectProperty.singleton X).isoClosure ≤ isIsomorphicTo X C:Type u_1inst✝:Category.{v_1, u_1} CX:C⊢ ObjectProperty.singleton X ≤ isIsomorphicTo X
C:Type u_1inst✝:Category.{v_1, u_1} CX:Ci✝¹:Ci✝:Unit⊢ isIsomorphicTo X X
All goals completed! 🐙
The full subcategory of C consisting of objects X : C satisfying
a given property P : ObjectProperty C is P.FullSubcategory and
the inclusion functor P.FullSubcategory ⥤ C is P.ι:
#synth Category (isIsomorphicTo X).FullSubcategory
example : (isIsomorphicTo X).FullSubcategory ⥤ C :=
(isIsomorphicTo X).ι
Similarly to the type ObjectProperty C of properties of objects of C,
we have the type MorphismProperty C of properties of morphisms in C
(which resembles the type ObjectProperty (Arrow C) of properties
of objects in the category of arrows in C). Similarly, certain typeclasses
express that W : MorphismProperty C is stable under composition
(MorphismProperty.IsStableUnderComposition), is stable under
base change (MorphismProperty.IsStableUnderBaseChange), etc.
If W : MorphismProperty C is multiplicative (MorphismProperty.IsMultiplicative),
i.e. contains identities and is stable under composition, then we may also
consider the widesubcategory of C consisting of the morphisms satisfying W:
variable (W : MorphismProperty C) [W.IsMultiplicative]
#synth Category (WideSubcategory W)