Mathlib.CategoryTheory.Functor.FullyFaithful

CategoryTheory.Functor.Full structure

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective. -/
@[stacks 001C]
class Full (F : C ⥤ D) : Prop where
  map_surjective {X Y : C} : Function.Surjective (F.map (X := X) (Y := Y))

Full Functor

Informal description

A functor $ F : C \to D $ between categories $ C $ and $ D $ is called *full* if for every pair of objects $ X, Y $ in $ C $, the induced map on morphisms $ F.\text{map} : (X \to Y) \to (F(X) \to F(Y)) $ is surjective. In other words, every morphism $ g : F(X) \to F(Y) $ in $ D $ is the image under $ F $ of some morphism $ f : X \to Y $ in $ C $.

CategoryTheory.Functor.Faithful structure

(F : C ⥤ D)

Full source

/-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective. -/
@[stacks 001C]
class Faithful (F : C ⥤ D) : Prop where
  /-- `F.map` is injective for each `X Y : C`. -/
  map_injective : ∀ {X Y : C}, Function.Injective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) := by
    aesop_cat

Faithful Functor

Informal description

A functor $ F : C \to D $ is called *faithful* if for every pair of objects $ X, Y $ in $ C $, the induced map on morphisms $ F.\text{map} : (X \to Y) \to (F(X) \to F(Y)) $ is injective. This means that distinct morphisms in $ C $ are mapped to distinct morphisms in $ D $.

CategoryTheory.Functor.map_injective theorem

(F : C ⥤ D) [Faithful F] : Function.Injective <| (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y))

Full source

theorem map_injective (F : C ⥤ D) [Faithful F] :
    Function.Injective <| (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  Faithful.map_injective

Injectivity of Morphism Mapping for Faithful Functors

Informal description

For any faithful functor $F \colon C \to D$ between categories $C$ and $D$, the induced map on morphisms $F.\text{map} \colon (X \to Y) \to (F(X) \to F(Y))$ is injective for all objects $X, Y$ in $C$.

CategoryTheory.Functor.map_injective_iff theorem

(F : C ⥤ D) [Faithful F] {X Y : C} (f g : X ⟶ Y) : F.map f = F.map g ↔ f = g

Full source

lemma map_injective_iff (F : C ⥤ D) [Faithful F] {X Y : C} (f g : X ⟶ Y) :
    F.map f = F.map g ↔ f = g :=
  ⟨fun h => F.map_injective h, fun h => by rw [h]⟩

Faithful Functor Morphism Equality Criterion

Informal description

For any faithful functor $F \colon C \to D$ between categories $C$ and $D$, and for any morphisms $f, g \colon X \to Y$ in $C$, the equality $F(f) = F(g)$ holds if and only if $f = g$.

CategoryTheory.Functor.mapIso_injective theorem

(F : C ⥤ D) [Faithful F] : Function.Injective <| (F.mapIso : (X ≅ Y) → (F.obj X ≅ F.obj Y))

Full source

theorem mapIso_injective (F : C ⥤ D) [Faithful F] :
    Function.Injective <| (F.mapIso : (X ≅ Y) → (F.obj X ≅ F.obj Y))  := fun _ _ h =>
  Iso.ext (map_injective F (congr_arg Iso.hom h :))

Injectivity of Isomorphism Mapping for Faithful Functors

Informal description

For any faithful functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories $\mathcal{C}$ and $\mathcal{D}$, the induced map on isomorphisms $F.\text{mapIso} \colon (X \cong Y) \to (F(X) \cong F(Y))$ is injective. That is, if $F.\text{mapIso}(\alpha) = F.\text{mapIso}(\beta)$ for two isomorphisms $\alpha, \beta \colon X \cong Y$ in $\mathcal{C}$, then $\alpha = \beta$.

CategoryTheory.Functor.map_surjective theorem

(F : C ⥤ D) [Full F] : Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y))

Full source

theorem map_surjective (F : C ⥤ D) [Full F] :
    Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  Full.map_surjective

Surjectivity of Morphism Mapping for Full Functors

Informal description

For any full functor $F \colon C \to D$ between categories $C$ and $D$, the induced map on morphisms $F.\text{map} \colon (X \to Y) \to (F(X) \to F(Y))$ is surjective for all objects $X, Y$ in $C$. That is, every morphism $g \colon F(X) \to F(Y)$ in $D$ is of the form $g = F.\text{map}(f)$ for some morphism $f \colon X \to Y$ in $C$.

CategoryTheory.Functor.preimage definition

(F : C ⥤ D) [Full F] (f : F.obj X ⟶ F.obj Y) : X ⟶ Y

Full source

/-- The choice of a preimage of a morphism under a full functor. -/
noncomputable def preimage (F : C ⥤ D) [Full F] (f : F.obj X ⟶ F.obj Y) : X ⟶ Y :=
  (F.map_surjective f).choose

Preimage of a morphism under a full functor

Informal description

Given a full functor $ F \colon C \to D $ between categories $ C $ and $ D $, and a morphism $ f \colon F(X) \to F(Y) $ in $ D $, the function `preimage` selects a morphism $ g \colon X \to Y $ in $ C $ such that $ F(g) = f $.

CategoryTheory.Functor.map_preimage theorem

(F : C ⥤ D) [Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (preimage F f) = f

Full source

@[simp]
theorem map_preimage (F : C ⥤ D) [Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) :
    F.map (preimage F f) = f :=
  (F.map_surjective f).choose_spec

Preimage Property of Full Functors: $F(\text{preimage}_F(f)) = f$

Informal description

For any full functor $F \colon C \to D$ between categories $C$ and $D$, and any morphism $f \colon F(X) \to F(Y)$ in $D$, the image under $F$ of the preimage of $f$ equals $f$, i.e., $F(\text{preimage}_F(f)) = f$.

CategoryTheory.Functor.preimage_id theorem

: F.preimage (𝟙 (F.obj X)) = 𝟙 X

Full source

@[simp]
theorem preimage_id : F.preimage (𝟙 (F.obj X)) = 𝟙 X :=
  F.map_injective (by simp)

Preimage of Identity under Full Functor Equals Identity

Informal description

For any full functor $F \colon C \to D$ between categories $C$ and $D$, the preimage of the identity morphism on $F(X)$ under $F$ is the identity morphism on $X$, i.e., $F^{-1}(\text{id}_{F(X)}) = \text{id}_X$.

CategoryTheory.Functor.preimage_comp theorem

(f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g

Full source

@[simp]
theorem preimage_comp (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :
    F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g :=
  F.map_injective (by simp)

Preimage of Composition under Full Functor Equals Composition of Preimages

Informal description

For any full functor $F \colon C \to D$ between categories $C$ and $D$, and any composable morphisms $f \colon F(X) \to F(Y)$ and $g \colon F(Y) \to F(Z)$ in $D$, the preimage of the composition $f \circ g$ under $F$ equals the composition of the preimages of $f$ and $g$, i.e., \[ F^{-1}(f \circ g) = F^{-1}(f) \circ F^{-1}(g). \]

CategoryTheory.Functor.preimage_map theorem

(f : X ⟶ Y) : F.preimage (F.map f) = f

Full source

@[simp]
theorem preimage_map (f : X ⟶ Y) : F.preimage (F.map f) = f :=
  F.map_injective (by simp)

Preimage of Functor Image Equals Original Morphism

Informal description

For any full functor $F \colon C \to D$ between categories $C$ and $D$, and any morphism $f \colon X \to Y$ in $C$, the preimage of $F(f)$ under $F$ is equal to $f$, i.e., $F^{-1}(F(f)) = f$.

CategoryTheory.Functor.preimageIso definition

(f : F.obj X ≅ F.obj Y) : X ≅ Y

Full source

/-- If `F : C ⥤ D` is fully faithful, every isomorphism `F.obj X ≅ F.obj Y` has a preimage. -/
@[simps]
noncomputable def preimageIso (f : F.obj X ≅ F.obj Y) :
    X ≅ Y where
  hom := F.preimage f.hom
  inv := F.preimage f.inv
  hom_inv_id := F.map_injective (by simp)
  inv_hom_id := F.map_injective (by simp)

Preimage of an isomorphism under a fully faithful functor

Informal description

Given a fully faithful functor $ F \colon C \to D $ and an isomorphism $ f \colon F(X) \cong F(Y) $ in $ D $, the function `preimageIso` constructs an isomorphism $ g \colon X \cong Y $ in $ C $ such that $ F(g) = f $. Specifically, the morphisms of $ g $ are obtained by applying the preimage function to the morphisms of $ f $, and the isomorphism properties are preserved due to the faithfulness of $ F $.

CategoryTheory.Functor.preimageIso_mapIso theorem

(f : X ≅ Y) : F.preimageIso (F.mapIso f) = f

Full source

@[simp]
theorem preimageIso_mapIso (f : X ≅ Y) : F.preimageIso (F.mapIso f) = f := by
  ext
  simp

Preimage of Functor Image of Isomorphism Equals Original Isomorphism

Informal description

For any isomorphism $f \colon X \cong Y$ in a category $\mathcal{C}$ and a fully faithful functor $F \colon \mathcal{C} \to \mathcal{D}$, the preimage of the image of $f$ under $F$ is equal to $f$ itself, i.e., $F^{-1}(F(f)) = f$.

CategoryTheory.Functor.FullyFaithful structure

Full source

/-- Structure containing the data of inverse map `(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)` of `F.map`
in order to express that `F` is a fully faithful functor. -/
structure FullyFaithful where
  /-- The inverse map `(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)` of `F.map`. -/
  preimage {X Y : C} (f : F.obj X ⟶ F.obj Y) : X ⟶ Y
  map_preimage {X Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (preimage f) = f := by aesop_cat
  preimage_map {X Y : C} (f : X ⟶ Y) : preimage (F.map f) = f := by aesop_cat

Fully Faithful Functor Structure

Informal description

The structure `FullyFaithful` for a functor $F$ contains the data of an inverse map that sends any morphism $F(X) \to F(Y)$ back to a morphism $X \to Y$, ensuring that $F$ is both full and faithful. This means $F$ induces a bijection on morphism sets between any two objects $X$ and $Y$.

CategoryTheory.Functor.FullyFaithful.ofFullyFaithful definition

[F.Full] [F.Faithful] : F.FullyFaithful

Full source

/-- A `FullyFaithful` structure can be obtained from the assumption the `F` is both
full and faithful. -/
noncomputable def ofFullyFaithful [F.Full] [F.Faithful] :
    F.FullyFaithful where
  preimage := F.preimage

Construction of a fully faithful functor from fullness and faithfulness

Informal description

Given a functor $ F \colon C \to D $ that is both full and faithful, the structure `FullyFaithful` can be constructed, providing an inverse map that sends any morphism $ F(X) \to F(Y) $ back to a morphism $ X \to Y $. This ensures that $ F $ induces a bijection on morphism sets between any two objects $ X $ and $ Y $ in $ C $.

CategoryTheory.Functor.FullyFaithful.id definition

: (𝟭 C).FullyFaithful

Full source

/-- The identity functor is fully faithful. -/
@[simps]
def id : (𝟭 C).FullyFaithful where
  preimage f := f

Identity functor is fully faithful

Informal description

The identity functor on a category $C$ is fully faithful, meaning it induces a bijection between the morphism sets $\text{Hom}(X, Y)$ and $\text{Hom}(X, Y)$ for any objects $X, Y \in C$.

CategoryTheory.Functor.FullyFaithful.homEquiv definition

{X Y : C} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)

Full source

/-- The equivalence `(X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)` given by `h : F.FullyFaithful`. -/
@[simps]
def homEquiv {X Y : C} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y) where
  toFun := F.map
  invFun := hF.preimage
  left_inv _ := by simp
  right_inv _ := by simp

Morphism set equivalence induced by a fully faithful functor

Informal description

For a fully faithful functor $ F $, the equivalence $ (X \longrightarrow Y) \simeq (F(X) \longrightarrow F(Y)) $ is given by the functor's mapping on morphisms $ F.map $ as the forward direction and its preimage function as the inverse direction. This establishes a bijection between the morphism sets $ \text{Hom}(X, Y) $ and $ \text{Hom}(F(X), F(Y)) $.

CategoryTheory.Functor.FullyFaithful.map_injective theorem

{X Y : C} {f g : X ⟶ Y} (h : F.map f = F.map g) : f = g

Full source

lemma map_injective {X Y : C} {f g : X ⟶ Y} (h : F.map f = F.map g) : f = g :=
  hF.homEquiv.injective h

Injectivity of Morphism Map for Fully Faithful Functors

Informal description

For any objects $X$ and $Y$ in a category $C$, and any morphisms $f, g : X \to Y$, if the images of $f$ and $g$ under the functor $F$ are equal (i.e., $F(f) = F(g)$), then $f = g$.

CategoryTheory.Functor.FullyFaithful.map_surjective theorem

{X Y : C} : Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y))

Full source

lemma map_surjective {X Y : C} :
    Function.Surjective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  hF.homEquiv.surjective

Surjectivity of Morphism Map for Fully Faithful Functors

Informal description

For any objects $X$ and $Y$ in a category $C$, the map on morphisms induced by a fully faithful functor $F$, $F.\text{map} \colon (X \longrightarrow Y) \to (F(X) \longrightarrow F(Y))$, is surjective.

CategoryTheory.Functor.FullyFaithful.map_bijective theorem

(X Y : C) : Function.Bijective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y))

Full source

lemma map_bijective (X Y : C) :
    Function.Bijective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  hF.homEquiv.bijective

Bijectivity of Morphism Map for Fully Faithful Functors

Informal description

For any objects $X$ and $Y$ in a category $C$, the morphism map induced by a fully faithful functor $F$, $F.\text{map} \colon \text{Hom}(X, Y) \to \text{Hom}(F(X), F(Y))$, is bijective.

CategoryTheory.Functor.FullyFaithful.preimage_id theorem

{X : C} : hF.preimage (𝟙 (F.obj X)) = 𝟙 X

Full source

@[simp]
lemma preimage_id {X : C} :
    hF.preimage (𝟙 (F.obj X)) = 𝟙 X :=
  hF.map_injective (by simp)

Preimage of Identity Morphism under Fully Faithful Functor

Informal description

For any object $X$ in a category $C$, the preimage of the identity morphism on $F(X)$ under a fully faithful functor $F$ is the identity morphism on $X$, i.e., $F^{-1}(\mathrm{id}_{F(X)}) = \mathrm{id}_X$.

CategoryTheory.Functor.FullyFaithful.preimage_comp theorem

 {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : hF.preimage (f ≫ g) = hF.preimage f ≫ hF.preimage g

Full source

@[simp, reassoc]
lemma preimage_comp {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :
    hF.preimage (f ≫ g) = hF.preimage f ≫ hF.preimage g :=
  hF.map_injective (by simp)

Preimage of Composition under Fully Faithful Functor

Informal description

For a fully faithful functor $F \colon C \to D$ and morphisms $f \colon F(X) \to F(Y)$ and $g \colon F(Y) \to F(Z)$ in $D$, the preimage of the composition $f \circ g$ under $F$ is equal to the composition of the preimages of $f$ and $g$, i.e., $F^{-1}(f \circ g) = F^{-1}(f) \circ F^{-1}(g)$.

CategoryTheory.Functor.FullyFaithful.full theorem

: F.Full

Full source

lemma full : F.Full where
  map_surjective := hF.map_surjective

Fully Faithful Functors are Full

Informal description

A fully faithful functor $F \colon C \to D$ is full, meaning that for any objects $X$ and $Y$ in $C$, the induced map on morphisms $F.\text{map} \colon (X \to Y) \to (F(X) \to F(Y))$ is surjective.

CategoryTheory.Functor.FullyFaithful.faithful theorem

: F.Faithful

Full source

lemma faithful : F.Faithful where
  map_injective := hF.map_injective

Fully Faithful Functors are Faithful

Informal description

A fully faithful functor $F \colon C \to D$ is faithful, meaning that for any objects $X$ and $Y$ in $C$, the induced map on morphisms $F.\text{map} \colon (X \to Y) \to (F(X) \to F(Y))$ is injective.

CategoryTheory.Functor.FullyFaithful.instSubsingleton instance

: Subsingleton F.FullyFaithful

Full source

instance : Subsingleton F.FullyFaithful where
  allEq h₁ h₂ := by
    have := h₁.faithful
    cases h₁ with | mk f₁ hf₁ _ => cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

Uniqueness of Fully Faithful Structure

Informal description

For any fully faithful functor $F$, the structure `FullyFaithful F` is a subsingleton, meaning there is at most one such structure for $F$.

CategoryTheory.Functor.FullyFaithful.preimageIso definition

{X Y : C} (e : F.obj X ≅ F.obj Y) : X ≅ Y

Full source

/-- The unique isomorphism `X ≅ Y` which induces an isomorphism `F.obj X ≅ F.obj Y`
when `hF : F.FullyFaithful`. -/
@[simps]
def preimageIso {X Y : C} (e : F.obj X ≅ F.obj Y) : X ≅ Y where
  hom := hF.preimage e.hom
  inv := hF.preimage e.inv
  hom_inv_id := hF.map_injective (by simp)
  inv_hom_id := hF.map_injective (by simp)

Preimage of an isomorphism under a fully faithful functor

Informal description

Given a fully faithful functor $F$ and an isomorphism $e \colon F(X) \cong F(Y)$ between the images of two objects $X$ and $Y$ in the target category, this constructs the unique isomorphism $X \cong Y$ that maps to $e$ under $F$. The morphisms of this isomorphism are obtained by applying the inverse map provided by the fully faithful structure of $F$ to the morphisms of $e$, and the isomorphism properties follow from the injectivity of $F$ on morphisms.

CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map theorem

{X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f

Full source

lemma isIso_of_isIso_map {X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] :
    IsIso f := by
  simpa using (hF.preimageIso (asIso (F.map f))).isIso_hom

Fully Faithful Functor Reflects Isomorphisms

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a fully faithful functor between categories. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, if the image $F(f) \colon F(X) \to F(Y)$ is an isomorphism in $\mathcal{D}$, then $f$ is an isomorphism in $\mathcal{C}$.

CategoryTheory.Functor.FullyFaithful.isoEquiv definition

{X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)

Full source

/-- The equivalence `(X ≅ Y) ≃ (F.obj X ≅ F.obj Y)` given by `h : F.FullyFaithful`. -/
@[simps]
def isoEquiv {X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y) where
  toFun := F.mapIso
  invFun := hF.preimageIso
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of isomorphisms under a fully faithful functor

Informal description

Given a fully faithful functor $ F : \mathcal{C} \to \mathcal{D} $, the equivalence $ (X \cong Y) \simeq (F(X) \cong F(Y)) $ maps an isomorphism $ i : X \cong Y $ in $ \mathcal{C} $ to its image $ F(i) : F(X) \cong F(Y) $ under $ F $, and conversely, any isomorphism $ e : F(X) \cong F(Y) $ in $ \mathcal{D} $ has a unique preimage $ hF.preimageIso(e) : X \cong Y $ in $ \mathcal{C} $. This establishes a bijection between isomorphisms in the source and target categories.

CategoryTheory.Functor.FullyFaithful.comp definition

{G : D ⥤ E} (hG : G.FullyFaithful) : (F ⋙ G).FullyFaithful

Full source

/-- Fully faithful functors are stable by composition. -/
@[simps]
def comp {G : D ⥤ E} (hG : G.FullyFaithful) : (F ⋙ G).FullyFaithful where
  preimage f := hF.preimage (hG.preimage f)

Composition of fully faithful functors is fully faithful

Informal description

Given a fully faithful functor $ G : \mathcal{D} \to \mathcal{E} $, the composition $ F \circ G : \mathcal{C} \to \mathcal{E} $ is also fully faithful. Specifically, the preimage of a morphism $ f $ under $ F \circ G $ is obtained by first taking the preimage under $ G $ and then the preimage under $ F $.

CategoryTheory.Functor.FullyFaithful.ofCompFaithful definition

{G : D ⥤ E} [G.Faithful] (hFG : (F ⋙ G).FullyFaithful) : F.FullyFaithful

Full source

/-- If `F ⋙ G` is fully faithful and `G` is faithful, then `F` is fully faithful. -/
def ofCompFaithful {G : D ⥤ E} [G.Faithful] (hFG : (F ⋙ G).FullyFaithful) :
    F.FullyFaithful where
  preimage f := hFG.preimage (G.map f)
  map_preimage f := G.map_injective (hFG.map_preimage (G.map f))
  preimage_map f := hFG.preimage_map f

Fully faithfulness via composition with a faithful functor

Informal description

If the composition of functors $ F \circ G $ is fully faithful and $ G $ is faithful, then $ F $ is fully faithful.

CategoryTheory.isIso_of_fully_faithful theorem

(f : X ⟶ Y) [IsIso (F.map f)] : IsIso f

Full source

/-- If the image of a morphism under a fully faithful functor in an isomorphism,
then the original morphisms is also an isomorphism.
-/
theorem isIso_of_fully_faithful (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f :=
  ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩

Isomorphism reflection via fully faithful functors: $F(f)$ iso implies $f$ iso

Informal description

Let $F \colon C \to D$ be a fully faithful functor between categories $C$ and $D$. For any morphism $f \colon X \to Y$ in $C$, if the image $F(f)$ is an isomorphism in $D$, then $f$ is an isomorphism in $C$.

CategoryTheory.Functor.Full.id instance

: Full (𝟭 C)

Full source

instance Full.id : Full (𝟭 C) where map_surjective := Function.surjective_id

Fullness of the Identity Functor

Informal description

The identity functor $𝟭 C$ on a category $C$ is full. That is, for any objects $X, Y$ in $C$, the map $(𝟭 C).\text{map} : (X \to Y) \to (X \to Y)$ is surjective.

CategoryTheory.Functor.Faithful.id instance

: Functor.Faithful (𝟭 C)

Full source

instance Faithful.id : Functor.Faithful (𝟭 C) := { }

Faithfulness of the Identity Functor

Informal description

The identity functor $𝟭 C$ on a category $C$ is faithful. That is, for any objects $X, Y$ in $C$, the map $(𝟭 C).\text{map} : (X \to Y) \to (X \to Y)$ is injective.

CategoryTheory.Functor.Faithful.comp instance

[F.Faithful] [G.Faithful] : (F ⋙ G).Faithful

Full source

instance Faithful.comp [F.Faithful] [G.Faithful] :
    (F ⋙ G).Faithful where map_injective p := F.map_injective (G.map_injective p)

Composition of Faithful Functors is Faithful

Informal description

For any faithful functors $F \colon C \to D$ and $G \colon D \to E$, their composition $F \circ G \colon C \to E$ is also faithful.

CategoryTheory.Functor.Faithful.of_comp theorem

[(F ⋙ G).Faithful] : F.Faithful

Full source

theorem Faithful.of_comp [(F ⋙ G).Faithful] : F.Faithful :=
  -- Porting note: (F ⋙ G).map_injective.of_comp has the incorrect type
  { map_injective := fun {_ _} => Function.Injective.of_comp (F ⋙ G).map_injective }

Faithfulness of Functor Preserved Under Composition

Informal description

If the composition $F \circ G$ of functors $F \colon C \to D$ and $G \colon D \to E$ is faithful, then the functor $F$ is faithful.

CategoryTheory.Functor.instFaithfulOfIsThin instance

[Quiver.IsThin C] : F.Faithful

Full source

instance (priority := 100) [Quiver.IsThin C] : F.Faithful where

Functor from Thin Category is Faithful

Informal description

For any thin category $C$ and functor $F : C \to D$, $F$ is faithful.

CategoryTheory.Functor.Full.of_iso theorem

[Full F] (α : F ≅ F') : Full F'

Full source

/-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full. -/
lemma Full.of_iso [Full F] (α : F ≅ F') : Full F' where
  map_surjective {X Y} f :=
    ⟨F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv), by simp [← NatIso.naturality_1 α]⟩

Fullness is preserved under natural isomorphism

Informal description

If a functor $F \colon C \to D$ is full and there exists a natural isomorphism $\alpha \colon F \cong F'$ between $F$ and another functor $F' \colon C \to D$, then $F'$ is also full.

CategoryTheory.Functor.Faithful.of_iso theorem

[F.Faithful] (α : F ≅ F') : F'.Faithful

Full source

theorem Faithful.of_iso [F.Faithful] (α : F ≅ F') : F'.Faithful :=
  { map_injective := fun h =>
      F.map_injective (by rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]) }

Faithfulness is preserved under natural isomorphism

Informal description

If a functor $F \colon C \to D$ is faithful and there exists a natural isomorphism $\alpha \colon F \cong F'$ between $F$ and another functor $F' \colon C \to D$, then $F'$ is also faithful.

CategoryTheory.Functor.Faithful.of_comp_iso theorem

{H : C ⥤ E} [H.Faithful] (h : F ⋙ G ≅ H) : F.Faithful

Full source

theorem Faithful.of_comp_iso {H : C ⥤ E} [H.Faithful] (h : F ⋙ GF ⋙ G ≅ H) : F.Faithful :=
  @Faithful.of_comp _ _ _ _ _ _ F G (Faithful.of_iso h.symm)

Faithfulness of $F$ via composition isomorphism with faithful $H$

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $H \colon C \to E$ be a faithful functor. If there exists a natural isomorphism $h \colon F \circ G \cong H$, then the functor $F$ is faithful.

CategoryTheory.Functor.Faithful.of_comp_eq theorem

{H : C ⥤ E} [ℋ : H.Faithful] (h : F ⋙ G = H) : F.Faithful

Full source

theorem Faithful.of_comp_eq {H : C ⥤ E} [ℋ : H.Faithful] (h : F ⋙ G = H) : F.Faithful :=
  @Faithful.of_comp _ _ _ _ _ _ F G (h.symm ▸ ℋ)

Faithfulness of Functor Preserved Under Composition Equality

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors, and let $H \colon C \to E$ be a faithful functor such that the composition $F \circ G$ equals $H$. Then $F$ is faithful.

CategoryTheory.Functor.Faithful.div definition

 (F : C ⥤ E) (G : D ⥤ E) [G.Faithful] (obj : C → D) (h_obj : ∀ X, G.obj (obj X) = F.obj X)
  (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : C ⥤ D

Full source

/-- “Divide” a functor by a faithful functor. -/
protected def Faithful.div (F : C ⥤ E) (G : D ⥤ E) [G.Faithful] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : C ⥤ D :=
  { obj, map := @map,
    map_id := by
      intros X
      apply G.map_injective
      apply eq_of_heq
      trans F.map (𝟙 X)
      · exact h_map
      · rw [F.map_id, G.map_id, h_obj X]
    map_comp := by
      intros X Y Z f g
      refine G.map_injective <| eq_of_heq <| h_map.trans ?_
      simp only [Functor.map_comp]
      convert HEq.refl (F.map f ≫ F.map g)
      all_goals { first | apply h_obj | apply h_map } }

Division of a functor by a faithful functor

Informal description

Given a faithful functor $ G : D \to E $, a functor $ F : C \to E $, and data consisting of: - An object map $ \text{obj} : C \to D $ such that $ G(\text{obj}(X)) = F(X) $ for all objects $ X $ in $ C $, - A morphism map $ \text{map} : (X \to Y) \to (\text{obj}(X) \to \text{obj}(Y)) $ such that $ G(\text{map}(f)) $ is heq to $ F(f) $ for all morphisms $ f : X \to Y $ in $ C $, then we can construct a functor $ \text{Faithful.div} F G \text{obj} \text{map} : C \to D $ that "divides" $ F $ by $ G $. This functor satisfies $ \text{Faithful.div} F G \text{obj} \text{map} \circ G = F $ and is itself faithful when $ F $ is faithful.

CategoryTheory.Functor.Faithful.div_comp theorem

 (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D) (h_obj : ∀ X, G.obj (obj X) = F.obj X)
  (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) :
  Faithful.div F G obj @h_obj @map @h_map ⋙ G = F

Full source

theorem Faithful.div_comp (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) :
    Faithful.divFaithful.div F G obj @h_obj @map @h_map ⋙ G = F := by
  obtain ⟨⟨F_obj, _⟩, _, _⟩ := F; obtain ⟨⟨G_obj, _⟩, _, _⟩ := G
  unfold Faithful.div Functor.comp
  have : F_obj = G_obj ∘ obj := (funext h_obj).symm
  subst this
  congr
  simp only [Function.comp_apply, heq_eq_eq] at h_map
  ext
  exact h_map

Composition of Divided Functor with Faithful Functor Recovers Original Functor

Informal description

Given faithful functors $F \colon C \to E$ and $G \colon D \to E$, an object map $\text{obj} \colon C \to D$ satisfying $G(\text{obj}(X)) = F(X)$ for all objects $X$ in $C$, and a morphism map $\text{map} \colon (X \to Y) \to (\text{obj}(X) \to \text{obj}(Y))$ such that $G(\text{map}(f))$ is heq to $F(f)$ for all morphisms $f \colon X \to Y$ in $C$, the composition of the functor $\text{Faithful.div}\, F\, G\, \text{obj}\, \text{map}$ with $G$ equals $F$.

CategoryTheory.Functor.Faithful.div_faithful theorem

 (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D) (h_obj : ∀ X, G.obj (obj X) = F.obj X)
  (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) :
  Functor.Faithful (Faithful.div F G obj @h_obj @map @h_map)

Full source

theorem Faithful.div_faithful (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) :
    Functor.Faithful (Faithful.div F G obj @h_obj @map @h_map) :=
  (Faithful.div_comp F G _ h_obj _ @h_map).faithful_of_comp

Faithfulness of the Divided Functor Construction

Informal description

Let $F \colon C \to E$ and $G \colon D \to E$ be faithful functors between categories. Given: - An object map $\text{obj} \colon C \to D$ such that $G(\text{obj}(X)) = F(X)$ for all objects $X$ in $C$, - A morphism map $\text{map} \colon (X \to Y) \to (\text{obj}(X) \to \text{obj}(Y))$ satisfying $G(\text{map}(f)) = F(f)$ for all morphisms $f \colon X \to Y$ in $C$, then the functor $\text{Faithful.div}\, F\, G\, \text{obj}\, \text{map} \colon C \to D$ constructed from this data is faithful.

CategoryTheory.Functor.Full.comp instance

[Full F] [Full G] : Full (F ⋙ G)

Full source

instance Full.comp [Full F] [Full G] : Full (F ⋙ G) where
  map_surjective f := ⟨F.preimage (G.preimage f), by simp⟩

Composition of Full Functors is Full

Informal description

Given two full functors $F \colon C \to D$ and $G \colon D \to E$ between categories, their composition $F \circ G \colon C \to E$ is also a full functor.

CategoryTheory.Functor.Full.of_comp_faithful theorem

[Full <| F ⋙ G] [G.Faithful] : Full F

Full source

/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full. -/
lemma Full.of_comp_faithful [Full <| F ⋙ G] [G.Faithful] : Full F where
  map_surjective f := ⟨(F ⋙ G).preimage (G.map f), G.map_injective ((F ⋙ G).map_preimage _)⟩

Fullness via Composition with Faithful Functor: $F \circ G$ full and $G$ faithful implies $F$ full

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If the composition $F \circ G$ is full and $G$ is faithful, then $F$ is full.

CategoryTheory.Functor.Full.of_comp_faithful_iso theorem

{F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [Full H] [G.Faithful] (h : F ⋙ G ≅ H) : Full F

Full source

/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full. -/
lemma Full.of_comp_faithful_iso {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [Full H] [G.Faithful]
    (h : F ⋙ GF ⋙ G ≅ H) : Full F := by
  have := Full.of_iso h.symm
  exact Full.of_comp_faithful F G

Fullness via Composition with Faithful Functor and Natural Isomorphism: $F \circ G \cong H$, $H$ full and $G$ faithful implies $F$ full

Informal description

Let $F \colon C \to D$, $G \colon D \to E$, and $H \colon C \to E$ be functors between categories. If there exists a natural isomorphism $h \colon F \circ G \cong H$ such that $H$ is full and $G$ is faithful, then $F$ is full.

CategoryTheory.Functor.fullyFaithfulCancelRight definition

{F G : C ⥤ D} (H : D ⥤ E) [Full H] [H.Faithful] (comp_iso : F ⋙ H ≅ G ⋙ H) : F ≅ G

Full source

/-- Given a natural isomorphism between `F ⋙ H` and `G ⋙ H` for a fully faithful functor `H`, we
can 'cancel' it to give a natural iso between `F` and `G`.
-/
noncomputable def fullyFaithfulCancelRight {F G : C ⥤ D} (H : D ⥤ E) [Full H] [H.Faithful]
    (comp_iso : F ⋙ HF ⋙ H ≅ G ⋙ H) : F ≅ G :=
  NatIso.ofComponents (fun X => H.preimageIso (comp_iso.app X)) fun f =>
    H.map_injective (by simpa using comp_iso.hom.naturality f)

Cancellation of natural isomorphism under fully faithful functor

Informal description

Given two functors $F, G \colon C \to D$ and a fully faithful functor $H \colon D \to E$, if there exists a natural isomorphism $\alpha \colon F \circ H \cong G \circ H$ between the compositions, then there exists a natural isomorphism $\beta \colon F \cong G$ obtained by applying the preimage of $H$ to the components of $\alpha$.

CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app theorem

 {F G : C ⥤ D} {H : D ⥤ E} [Full H] [H.Faithful] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :
  (fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)

Full source

@[simp]
theorem fullyFaithfulCancelRight_hom_app {F G : C ⥤ D} {H : D ⥤ E} [Full H] [H.Faithful]
    (comp_iso : F ⋙ HF ⋙ H ≅ G ⋙ H) (X : C) :
    (fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X) :=
  rfl

Component Formula for Natural Isomorphism Cancellation under Fully Faithful Functor

Informal description

Let $F, G \colon C \to D$ be functors and $H \colon D \to E$ be a fully faithful functor. Given a natural isomorphism $\alpha \colon F \circ H \cong G \circ H$, for any object $X$ in $C$, the component of the induced isomorphism $\beta \colon F \cong G$ at $X$ is equal to the preimage under $H$ of the component of $\alpha$ at $X$, i.e., \[ \beta_X = H^{-1}(\alpha_X). \]

CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app theorem

 {F G : C ⥤ D} {H : D ⥤ E} [Full H] [H.Faithful] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :
  (fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)

Full source

@[simp]
theorem fullyFaithfulCancelRight_inv_app {F G : C ⥤ D} {H : D ⥤ E} [Full H] [H.Faithful]
    (comp_iso : F ⋙ HF ⋙ H ≅ G ⋙ H) (X : C) :
    (fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X) :=
  rfl

Component formula for inverse of cancellation isomorphism under fully faithful functor

Informal description

Let $F, G \colon C \to D$ and $H \colon D \to E$ be functors between categories, where $H$ is fully faithful. Given a natural isomorphism $\alpha \colon F \circ H \cong G \circ H$, the component of the inverse of the induced isomorphism $\beta \colon F \cong G$ at an object $X \in C$ is equal to the preimage under $H$ of the component of the inverse of $\alpha$ at $X$. That is, $$(\beta^{-1})_X = H^{-1}(\alpha^{-1}_X).$$

Main definitions and results