Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

CategoryTheory.ObjectProperty.FullSubcategory structure

Full source

/--
A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use
actual subtypes since the simp-normal form `↑X` of `X.val` does not work well for full
subcategories. -/
@[ext, stacks 001D "We do not define 'strictly full' subcategories."]
structure FullSubcategory where
  /-- The category of which this is a full subcategory -/
  obj : C
  /-- The predicate satisfied by all objects in this subcategory -/
  property : P obj

Full subcategory defined by an object property

Informal description

The structure representing the full subcategory of a category $\mathcal{C}$ consisting of objects satisfying a given property $P$. Morphisms in this subcategory are the same as in $\mathcal{C}$, ignoring the property $P$. This structure is used instead of actual subtypes to avoid issues with simp-normal forms when working with full subcategories.

CategoryTheory.ObjectProperty.FullSubcategory.category instance

: Category.{v} P.FullSubcategory

Full source

instance FullSubcategory.category : Category.{v} P.FullSubcategory :=
  InducedCategory.category FullSubcategory.obj

Category Structure on Full Subcategory Defined by Object Property

Informal description

For any category $\mathcal{C}$ and object property $P$ on $\mathcal{C}$, the full subcategory of objects satisfying $P$ forms a category where the morphisms are inherited from $\mathcal{C}$.

CategoryTheory.ObjectProperty.FullSubcategory.id_def theorem

(X : P.FullSubcategory) : 𝟙 X = 𝟙 X.obj

Full source

lemma FullSubcategory.id_def (X : P.FullSubcategory) : 𝟙 X = 𝟙 X.obj := rfl

Identity Morphism Preservation in Full Subcategory

Informal description

For any object $X$ in the full subcategory defined by property $P$, the identity morphism $\mathrm{id}_X$ in the subcategory is equal to the identity morphism $\mathrm{id}_{X.obj}$ in the original category $\mathcal{C}$.

CategoryTheory.ObjectProperty.FullSubcategory.comp_def theorem

{X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = (f ≫ g : X.obj ⟶ Z.obj)

Full source

lemma FullSubcategory.comp_def {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) :
    f ≫ g = (f ≫ g : X.obj ⟶ Z.obj) := rfl

Composition in Full Subcategory Equals Composition in Original Category

Informal description

For any objects $X, Y, Z$ in the full subcategory defined by property $P$ and morphisms $f : X \to Y$, $g : Y \to Z$, the composition $f \gg g$ in the subcategory is equal to the composition $f \gg g$ in the original category $\mathcal{C}$ (viewed as a morphism from $X.obj$ to $Z.obj$).

CategoryTheory.ObjectProperty.ι definition

: P.FullSubcategory ⥤ C

Full source

/-- The forgetful functor from a full subcategory into the original category
("forgetting" the condition).
-/
def ι : P.FullSubcategory ⥤ C :=
  inducedFunctor FullSubcategory.obj

Forgetful functor from full subcategory

Informal description

The forgetful functor from the full subcategory of objects satisfying property $P$ in category $\mathcal{C}$ to the original category $\mathcal{C}$, which maps each object $X$ in the subcategory to its underlying object in $\mathcal{C}$ and each morphism $f$ to itself.

CategoryTheory.ObjectProperty.ι_obj theorem

{X} : P.ι.obj X = X.obj

Full source

@[simp]
theorem ι_obj {X} : P.ι.obj X = X.obj :=
  rfl

Forgetful Functor Preserves Objects in Full Subcategory

Informal description

For any object $X$ in the full subcategory defined by property $P$, the underlying object of $X$ in the original category $\mathcal{C}$ is equal to $X.obj$, i.e., $\iota(X) = X.obj$.

CategoryTheory.ObjectProperty.ι_map theorem

{X Y} {f : X ⟶ Y} : P.ι.map f = f

Full source

@[simp]
theorem ι_map {X Y} {f : X ⟶ Y} : P.ι.map f = f :=
  rfl

Forgetful Functor Preserves Morphisms in Full Subcategory

Informal description

For any objects $X$ and $Y$ in the full subcategory defined by property $P$ and any morphism $f : X \to Y$ in this subcategory, the image of $f$ under the forgetful functor $\iota$ is equal to $f$ itself, i.e., $\iota(f) = f$.

CategoryTheory.ObjectProperty.fullyFaithfulι abbrev

: P.ι.FullyFaithful

Full source

/-- The inclusion of a full subcategory is fully faithful. -/
abbrev fullyFaithfulι :
    P.ι.FullyFaithful :=
  fullyFaithfulInducedFunctor _

Forgetful Functor from Full Subcategory is Fully Faithful

Informal description

The forgetful functor $\iota$ from the full subcategory of objects satisfying property $P$ in a category $\mathcal{C}$ to $\mathcal{C}$ itself is fully faithful. That is, for any two objects $X$ and $Y$ in the full subcategory, the map $\text{Hom}(X, Y) \to \text{Hom}(\iota(X), \iota(Y))$ induced by $\iota$ is bijective.

CategoryTheory.ObjectProperty.full_ι instance

: P.ι.Full

Full source

instance full_ι : P.ι.Full := P.fullyFaithfulι.full

Forgetful Functor from Full Subcategory is Full

Informal description

The forgetful functor $\iota$ from the full subcategory of objects satisfying property $P$ in a category $\mathcal{C}$ to $\mathcal{C}$ itself is full. That is, for any two objects $X$ and $Y$ in the full subcategory, the map $\text{Hom}(X, Y) \to \text{Hom}(\iota(X), \iota(Y))$ induced by $\iota$ is surjective.

CategoryTheory.ObjectProperty.faithful_ι instance

: P.ι.Faithful

Full source

instance faithful_ι : P.ι.Faithful := P.fullyFaithfulι.faithful

Faithfulness of the Forgetful Functor from Full Subcategory

Informal description

The forgetful functor from the full subcategory of objects satisfying property $P$ in a category $\mathcal{C}$ to $\mathcal{C}$ itself is faithful. That is, for any two objects $X$ and $Y$ in the full subcategory, the map $\text{Hom}(X, Y) \to \text{Hom}(\iota(X), \iota(Y))$ induced by $\iota$ is injective.

CategoryTheory.ObjectProperty.isoMk definition

{X Y : P.FullSubcategory} (e : P.ι.obj X ≅ P.ι.obj Y) : X ≅ Y

Full source

/-- Constructor for isomorphisms in `P.FullSubcategory` when
`P : ObjectProperty C`. -/
@[simps]
def isoMk {X Y : P.FullSubcategory} (e : P.ι.obj X ≅ P.ι.obj Y) : X ≅ Y where
  hom := e.hom
  inv := e.inv
  hom_inv_id := e.hom_inv_id
  inv_hom_id := e.inv_hom_id

Isomorphism in full subcategory induced by underlying isomorphism

Informal description

Given a category $\mathcal{C}$ with an object property $P$, and two objects $X$ and $Y$ in the full subcategory of $\mathcal{C}$ defined by $P$, an isomorphism $e$ between the underlying objects of $X$ and $Y$ in $\mathcal{C}$ induces an isomorphism between $X$ and $Y$ in the full subcategory. The morphisms and their inverses are inherited from $e$, and the isomorphism conditions are preserved.

CategoryTheory.ObjectProperty.ιOfLE definition

(h : P ≤ P') : P.FullSubcategory ⥤ P'.FullSubcategory

Full source

/-- If `P` and `P'` are properties of objects such that `P ≤ P'`, there is
an induced functor `P.FullSubcategory ⥤ P'.FullSubcategory`. -/
@[simps]
def ιOfLE (h : P ≤ P') : P.FullSubcategory ⥤ P'.FullSubcategory where
  obj X := ⟨X.1, h _ X.2⟩
  map f := f

Inclusion functor between full subcategories induced by implication of object properties

Informal description

Given a category $\mathcal{C}$ and two object properties $P$ and $P'$ such that $P$ implies $P'$ (i.e., $P \leq P'$), there is an induced functor from the full subcategory of objects satisfying $P$ to the full subcategory of objects satisfying $P'$. This functor acts as the identity on morphisms and maps an object $X$ in the $P$-subcategory to the same object in the $P'$-subcategory (since $P(X)$ implies $P'(X)$ by assumption).

CategoryTheory.ObjectProperty.fullyFaithfulιOfLE definition

(h : P ≤ P') : (ιOfLE h).FullyFaithful

Full source

/-- If `h : P ≤ P'`, then `ιOfLE h` is fully faithful. -/
def fullyFaithfulιOfLE (h : P ≤ P') :
    (ιOfLE h).FullyFaithful where
  preimage f := f

Fully faithful inclusion of full subcategories under implication of object properties

Informal description

Given a category $\mathcal{C}$ and two object properties $P$ and $P'$ such that $P$ implies $P'$ (i.e., $P \leq P'$), the inclusion functor $\iota_{\text{ofLE}} h$ from the full subcategory of objects satisfying $P$ to the full subcategory of objects satisfying $P'$ is fully faithful. This means it is both full (surjective on morphisms between any two objects) and faithful (injective on morphisms between any two objects).

CategoryTheory.ObjectProperty.full_ιOfLE instance

(h : P ≤ P') : (ιOfLE h).Full

Full source

instance full_ιOfLE (h : P ≤ P') : (ιOfLE h).Full := (fullyFaithfulιOfLE h).full

Fullness of the Inclusion Functor Between Full Subcategories

Informal description

For any category $\mathcal{C}$ and object properties $P$ and $P'$ on $\mathcal{C}$ such that $P$ implies $P'$, the inclusion functor $\iota_{\text{ofLE}}(h) \colon P.\text{FullSubcategory} \to P'.\text{FullSubcategory}$ is full. That is, for any two objects $X$ and $Y$ in the full subcategory defined by $P$, the map on morphisms induced by $\iota_{\text{ofLE}}(h)$ is surjective.

CategoryTheory.ObjectProperty.faithful_ιOfLE instance

(h : P ≤ P') : (ιOfLE h).Faithful

Full source

instance faithful_ιOfLE (h : P ≤ P') : (ιOfLE h).Faithful := (fullyFaithfulιOfLE h).faithful

Faithfulness of Inclusion Functor Between Full Subcategories

Informal description

Given a category $\mathcal{C}$ and two object properties $P$ and $P'$ such that $P$ implies $P'$ (i.e., $P \leq P'$), the inclusion functor $\iota_{\text{ofLE}} h$ from the full subcategory of objects satisfying $P$ to the full subcategory of objects satisfying $P'$ is faithful. This means that for any two objects $X$ and $Y$ in the $P$-subcategory, the map on morphisms $\text{Hom}(X, Y) \to \text{Hom}(\iota_{\text{ofLE}} h(X), \iota_{\text{ofLE}} h(Y))$ is injective.

CategoryTheory.ObjectProperty.FullSubcategory.map_inclusion theorem

(h : P ≤ P') : ιOfLE h ⋙ P'.ι = P.ι

Full source

@[deprecated "use ιOfLECompιIso" (since := "2025-03-04")]
theorem FullSubcategory.map_inclusion (h : P ≤ P') :
  ιOfLEιOfLE h ⋙ P'.ι = P.ι := rfl

Compatibility of Inclusion and Forgetful Functors for Full Subcategories

Informal description

Given a category $\mathcal{C}$ and two object properties $P$ and $P'$ such that $P$ implies $P'$ (i.e., $P \leq P'$), the composition of the inclusion functor $\iota_{\text{ofLE}}(h) \colon P.\text{FullSubcategory} \to P'.\text{FullSubcategory}$ (induced by $h$) with the forgetful functor $P'.\iota \colon P'.\text{FullSubcategory} \to \mathcal{C}$ is equal to the forgetful functor $P.\iota \colon P.\text{FullSubcategory} \to \mathcal{C}$.

CategoryTheory.ObjectProperty.ιOfLECompιIso definition

(h : P ≤ P') : ιOfLE h ⋙ P'.ι ≅ P.ι

Full source

/-- If `h : P ≤ P'` is an inequality of properties of objects,
this is the obvious isomorphism `ιOfLE h ⋙ P'.ι ≅ P.ι`. -/
def ιOfLECompιIso (h : P ≤ P') : ιOfLEιOfLE h ⋙ P'.ιιOfLE h ⋙ P'.ι ≅ P.ι := Iso.refl _

Natural isomorphism between composed inclusion functors for full subcategories

Informal description

Given a category $\mathcal{C}$ and two object properties $P$ and $P'$ such that $P$ implies $P'$ (i.e., $P \leq P'$), the composition of the inclusion functor $\iota_{\text{ofLE}} h$ from the full subcategory of objects satisfying $P$ to the full subcategory of objects satisfying $P'$, followed by the forgetful functor $\iota$ from the $P'$-subcategory to $\mathcal{C}$, is naturally isomorphic to the forgetful functor $\iota$ from the $P$-subcategory directly to $\mathcal{C}$.

CategoryTheory.ObjectProperty.lift definition

: C ⥤ FullSubcategory P

Full source

/-- A functor which maps objects to objects satisfying a certain property induces a lift through
    the full subcategory of objects satisfying that property. -/
@[simps]
def lift : C ⥤ FullSubcategory P where
  obj X := ⟨F.obj X, hF X⟩
  map f := F.map f

Lift of a functor to a full subcategory defined by an object property

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a property $P$ on objects of $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the lift of $F$ is a functor from $\mathcal{C}$ to the full subcategory of $\mathcal{D}$ consisting of objects satisfying $P$. The lift acts on objects by $X \mapsto \langle F(X), hF(X) \rangle$ and on morphisms by $f \mapsto F(f)$.

CategoryTheory.ObjectProperty.FullSubcategory.lift_comp_inclusion_eq theorem

: P.lift F hF ⋙ P.ι = F

Full source

@[deprecated "use liftCompιIso" (since := "2025-03-04")]
theorem FullSubcategory.lift_comp_inclusion_eq :
    P.lift F hF ⋙ P.ι = F :=
  rfl

Composition of Lift and Inclusion Functors Equals Original Functor

Informal description

Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and an object property $P$ on $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the composition of the lifted functor $P.\text{lift} F hF$ with the forgetful functor $P.\iota$ is equal to $F$.

CategoryTheory.ObjectProperty.liftCompιIso definition

: P.lift F hF ⋙ P.ι ≅ F

Full source

/-- Composing the lift of a functor through a full subcategory with the inclusion yields the
    original functor. This is actually true definitionally. -/
def liftCompιIso : P.lift F hF ⋙ P.ιP.lift F hF ⋙ P.ι ≅ F := Iso.refl _

Isomorphism between lifted functor composition and original functor

Informal description

The natural isomorphism between the composition of the lift of a functor $F \colon \mathcal{C} \to \mathcal{D}$ through the full subcategory defined by property $P$ and the inclusion functor, and the original functor $F$. This isomorphism is definitionally the identity isomorphism.

CategoryTheory.ObjectProperty.ι_obj_lift_obj theorem

(X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X

Full source

@[simp]
lemma ι_obj_lift_obj (X : C) :
    P.ι.obj ((P.lift F hF).obj X) = F.obj X := rfl

Forgetful Functor Preserves Lifted Objects: $\iota \circ (P.\text{lift}~F~hF) = F$ on Objects

Informal description

For any object $X$ in category $\mathcal{C}$, the application of the forgetful functor $\iota$ to the lifted object $(P.\text{lift}~F~hF)(X)$ in the full subcategory defined by property $P$ equals the application of the functor $F$ to $X$, i.e., $\iota((P.\text{lift}~F~hF)(X)) = F(X)$.

CategoryTheory.ObjectProperty.ι_obj_lift_map theorem

{X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f

Full source

@[simp]
lemma ι_obj_lift_map {X Y : C} (f : X ⟶ Y) :
    P.ι.map ((P.lift F hF).map f) = F.map f := rfl

Forgetful Functor Preserves Lifted Morphisms

Informal description

For any morphism $f \colon X \to Y$ in category $\mathcal{C}$, the image of the lifted morphism $(P.\text{lift} F hF).\text{map}(f)$ under the forgetful functor $P.\iota$ is equal to $F.\text{map}(f)$ in $\mathcal{D}$. That is, $P.\iota.\text{map}((P.\text{lift} F hF).\text{map}(f)) = F.\text{map}(f)$.

CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift instance

[F.Faithful] : (P.lift F hF).Faithful

Full source

instance [F.Faithful] : (P.lift F hF).Faithful :=
  Functor.Faithful.of_comp_iso (P.liftCompιIso F hF)

Faithfulness of Lifted Functor to Full Subcategory

Informal description

Given a faithful functor $F \colon \mathcal{C} \to \mathcal{D}$ and an object property $P$ on $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the lifted functor $P.\text{lift}~F~hF$ from $\mathcal{C}$ to the full subcategory of $\mathcal{D}$ defined by $P$ is also faithful.

CategoryTheory.ObjectProperty.instFullFullSubcategoryLift instance

[F.Full] : (P.lift F hF).Full

Full source

instance [F.Full] : (P.lift F hF).Full :=
  Functor.Full.of_comp_faithful_iso (P.liftCompιIso F hF)

Fullness of Lifted Functors to Full Subcategories

Informal description

Given a full functor $F \colon \mathcal{C} \to \mathcal{D}$ and an object property $P$ on $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the lifted functor $P.\text{lift}~F~hF$ from $\mathcal{C}$ to the full subcategory of $\mathcal{D}$ defined by $P$ is also full.

CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift_1 instance

[F.Faithful] : (P.lift F hF).Faithful

Full source

instance [F.Faithful] : (P.lift F hF).Faithful :=
  Functor.Faithful.of_comp_iso (P.liftCompιIso F hF)

Faithfulness of Lifted Functors to Full Subcategories

Informal description

For any faithful functor $F \colon \mathcal{C} \to \mathcal{D}$ and object property $P$ on $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the lifted functor $P.\text{lift} F hF$ from $\mathcal{C}$ to the full subcategory of $\mathcal{D}$ defined by $P$ is also faithful.

CategoryTheory.ObjectProperty.instFullFullSubcategoryLift_1 instance

[F.Full] : (P.lift F hF).Full

Full source

instance [F.Full] : (P.lift F hF).Full :=
  Functor.Full.of_comp_faithful_iso (P.liftCompιIso F hF)

Fullness of Lifted Functors to Full Subcategories

Informal description

For any full functor $F \colon \mathcal{C} \to \mathcal{D}$ and object property $P$ on $\mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, the lifted functor $P.\text{lift} F hF$ from $\mathcal{C}$ to the full subcategory of $\mathcal{D}$ defined by $P$ is also full.

CategoryTheory.ObjectProperty.liftCompιOfLEIso definition

(h : P ≤ Q) : P.lift F hF ⋙ ιOfLE h ≅ Q.lift F (fun X ↦ h _ (hF X))

Full source

/-- When `h : P ≤ Q`, this is the canonical isomorphism
`P.lift F hF ⋙ ιOfLE h ≅ Q.lift F _`. -/
def liftCompιOfLEIso (h : P ≤ Q) :
    P.lift F hF ⋙ ιOfLE hP.lift F hF ⋙ ιOfLE h ≅ Q.lift F (fun X ↦ h _ (hF X)) := Iso.refl _

Canonical isomorphism between lifts of functors to full subcategories under implication of object properties

Informal description

Given a category $\mathcal{C}$, an object property $P$ on $\mathcal{C}$, and a functor $F \colon \mathcal{C} \to \mathcal{D}$ such that for every object $X$ in $\mathcal{C}$, $F(X)$ satisfies $P$ (i.e., $hF(X) : P(F(X))$ holds), and given another object property $Q$ such that $P$ implies $Q$ (i.e., $h : P \leq Q$), there is a canonical isomorphism between the composition of the lift functor $P.lift F hF$ followed by the inclusion functor $\iotaOfLE h$ and the lift functor $Q.lift F (\lambda X, h (F X) (hF X))$.

CategoryTheory.ObjectProperty.FullSubcategory.lift_comp_map theorem

(h : P ≤ Q) : P.lift F hF ⋙ ιOfLE h = Q.lift F (fun X ↦ h _ (hF X))

Full source

@[deprecated "Use liftCompιOfLEIso" (since := "2025-03-04")]
theorem FullSubcategory.lift_comp_map (h : P ≤ Q) :
    P.lift F hF ⋙ ιOfLE h =
      Q.lift F (fun X ↦  h _ (hF X)) :=
  rfl

Compatibility of Lift Functors with Inclusion of Full Subcategories

Informal description

Given a category $\mathcal{C}$, an object property $P$ on $\mathcal{C}$, and a functor $F \colon \mathcal{C} \to \mathcal{D}$ such that $F(X)$ satisfies $P$ for every object $X$ in $\mathcal{C}$, then for any implication $h \colon P \leq Q$ between object properties, the composition of the lift functor $P.\text{lift} F hF$ with the inclusion functor $\iotaOfLE h$ is equal to the lift functor $Q.\text{lift} F (\lambda X, h (F X) (hF X))$.