CategoryTheory.FullSubcategory.property
theorem CategoryTheory.FullSubcategory.property :
∀ {C : Type u₁} {Z : C → Prop} (self : CategoryTheory.FullSubcategory Z), Z self.obj
This theorem states that for any category `C` and a proposition `Z` acting on objects in `C`, and for any full subcategory of `C` where the objects satisfy `Z`, then any object of this subcategory will satisfy the predicate `Z`. In other words, it confirms that all objects of a full subcategory defined by a certain condition do indeed satisfy that condition.
More concisely: If `Z` is a proposition acting on objects in a category `C`, and `SubC` is a full subcategory of `C` where all objects satisfy `Z`, then every object in `SubC` satisfies `Z`.
|
CategoryTheory.FullSubcategory.ext
theorem CategoryTheory.FullSubcategory.ext :
∀ {C : Type u₁} {Z : C → Prop} (x y : CategoryTheory.FullSubcategory Z), x.obj = y.obj → x = y
This theorem states that for any category `C` and any property `Z` defining a subcategory, if two objects `x` and `y` from the full subcategory defined by `Z` have the same underlying object in `C`, then `x` and `y` are equal in the full subcategory. This means that in the context of full subcategories, two objects are considered the same if and only if their underlying objects in the original category are the same.
More concisely: In any category and subcategory defined by a property, two objects having the same underlying object in the original category are equal in the subcategory.
|