Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison

! This file was ported from Lean 3 source module category_theory.functor.fully_faithful
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.NatIso
import Mathlib.Logic.Equiv.Defs

/-!
# Full and faithful functors

We define typeclasses `Full` and `Faithful`, decorating functors.

## Main definitions and results
* Use `F.map_injective` to retrieve the fact that `F.map` is injective when `[Faithful F]`.
* Similarly, `F.map_surjective` states that `F.map` is surjective when `[Full F]`.
* Use `F.preimage` to obtain preimages of morphisms when `[Full F]`.
* We prove some basic "cancellation" lemmas for full and/or faithful functors, as well as a
  construction for "dividing" a functor by a faithful functor, see `Faithful.div`.
* `Full F` carries data, so definitional properties of the preimage can be used when using
  `F.preimage`. To obtain an instance of `Full F` non-constructively, you can use `fullOfExists`
  and `fullOfSurjective`.

See `CategoryTheory.Equivalence.of_fullyFaithful_ess_surj` for the fact that a functor is an
equivalence if and only if it is fully faithful and essentially surjective.

-/


-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
universe v₁ v₂ v₃ u₁ u₂ u₃

namespace CategoryTheory

variable {
C: Type u₁
C : 
Type u₁: Type (u₁+1)
Type u₁} [
Category: Type ?u.4 → Type (max?u.4(v₁+1))
Category.{v₁} 
C: Type u₁
C] {
D: Type u₂
D : 
Type u₂: Type (u₂+1)
Type u₂} [
Category: Type ?u.9 → Type (max?u.9(v₂+1))
Category.{v₂} 
D: Type u₂
D]

/-- A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective.
In fact, we use a constructive definition, so the `Full F` typeclass contains data,
specifying a particular preimage of each `f : F.obj X ⟶ F.obj Y`.

See .
-/
class 
Full: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {F : C ⥤ D} →
          (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) →
            autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f) _auto✝ → Full F
Full (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) where
  /-- The data of a preimage for every `f : F.obj X ⟶ F.obj Y`. -/
  
preimage: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → {F : C ⥤ D} → [self : Full F] → {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage : ∀ {
X: C
X 
Y: C
Y : 
C: Type u₁
C} (
_: F.obj X ⟶ F.obj Y
_ : 
F: C ⥤ D
F.
obj: {V : Type ?u.132} → [inst : Quiver V] → {W : Type ?u.131} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.182} → [inst : Quiver V] → {W : Type ?u.181} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y), 
X: C
X ⟶ 
Y: C
Y
  /-- The property that `Full.preimage f` of maps to `f` via `F.map`. -/
  
witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C}
  (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
witness : ∀ {
X: C
X 
Y: C
Y : 
C: Type u₁
C} (
f: F.obj X ⟶ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.276} → [inst : Quiver V] → {W : Type ?u.275} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.296} → [inst : Quiver V] → {W : Type ?u.295} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y), 
F: C ⥤ D
F.
map: {V : Type ?u.336} →
  [inst : Quiver V] →
    {W : Type ?u.335} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map (
preimage: {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: F.obj X ⟶ F.obj Y
f) = 
f: F.obj X ⟶ F.obj Y
f := by aesop_cat
#align category_theory.full 
CategoryTheory.Full: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → C ⥤ D → Type (max(maxu₁v₁)v₂)
CategoryTheory.Full
#align category_theory.full.witness 
CategoryTheory.Full.witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C}
  (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
CategoryTheory.Full.witness

attribute [simp] 
Full.witness: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Full F] {X Y : C}
  (f : F.obj X ⟶ F.obj Y), F.map (Full.preimage f) = f
Full.witness


/- ./././Mathport/Syntax/Translate/Command.lean:379:30: infer kinds are unsupported in Lean 4:
#[`map_injective'] [] -/
/-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective.

See .
-/
class 
Faithful: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D},
  autoParam (∀ {X Y : C}, Function.Injective F.map) _auto✝ → Faithful F
Faithful (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) : 
Prop: Type
Prop where
  /-- `F.map` is injective for each `X Y : C`. -/
  
map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F] {X Y : C},
  Function.Injective F.map
map_injective : ∀ {
X: C
X 
Y: C
Y : 
C: Type u₁
C}, 
Function.Injective: {α : Sort ?u.497} → {β : Sort ?u.496} → (α → β) → Prop
Function.Injective (
F: C ⥤ D
F.
map: {V : Type ?u.654} →
  [inst : Quiver V] →
    {W : Type ?u.653} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map : (
X: C
X ⟶ 
Y: C
Y) → (
F: C ⥤ D
F.
obj: {V : Type ?u.567} → [inst : Quiver V] → {W : Type ?u.566} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.616} → [inst : Quiver V] → {W : Type ?u.615} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y)) := by
    aesop_cat
#align category_theory.faithful 
CategoryTheory.Faithful: {C : Type u₁} → [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → C ⥤ D → Prop
CategoryTheory.Faithful
#align category_theory.faithful.map_injective 
CategoryTheory.Faithful.map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F] {X Y : C},
  Function.Injective F.map
CategoryTheory.Faithful.map_injective

namespace Functor

variable {
X: C
X 
Y: C
Y : 
C: Type u₁
C}

theorem 
map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F],
  Function.Injective F.map
map_injective (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Faithful: {C : Type ?u.734} → [inst : Category C] → {D : Type ?u.733} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] :
    
Function.Injective: {α : Sort ?u.776} → {β : Sort ?u.775} → (α → β) → Prop
Function.Injective <| (
F: C ⥤ D
F.
map: {V : Type ?u.925} →
  [inst : Quiver V] →
    {W : Type ?u.924} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map : (
X: C
X ⟶ 
Y: C
Y) → (
F: C ⥤ D
F.
obj: {V : Type ?u.838} → [inst : Quiver V] → {W : Type ?u.837} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.887} → [inst : Quiver V] → {W : Type ?u.886} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y)) :=
  
Faithful.map_injective: ∀ {C : Type ?u.950} [inst : Category C] {D : Type ?u.949} [inst_1 : Category D] {F : C ⥤ D} [self : Faithful F]
  {X Y : C}, Function.Injective F.map
Faithful.map_injective
#align category_theory.functor.map_injective 
CategoryTheory.Functor.map_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F],
  Function.Injective F.map
CategoryTheory.Functor.map_injective

theorem 
mapIso_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F],
  Function.Injective F.mapIso
mapIso_injective (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Faithful: {C : Type ?u.1059} → [inst : Category C] → {D : Type ?u.1058} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] :
    
Function.Injective: {α : Sort ?u.1101} → {β : Sort ?u.1100} → (α → β) → Prop
Function.Injective <| (
F: C ⥤ D
F.
mapIso: {C : Type ?u.1213} →
  [inst : Category C] →
    {D : Type ?u.1212} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso : (
X: C
X ≅ 
Y: C
Y) → (
F: C ⥤ D
F.
obj: {V : Type ?u.1149} → [inst : Quiver V] → {W : Type ?u.1148} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ≅ 
F: C ⥤ D
F.
obj: {V : Type ?u.1199} → [inst : Quiver V] → {W : Type ?u.1198} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y))  := fun 
_: ?m.1249
_ 
_: ?m.1252
_ 
h: ?m.1255
h =>
  
Iso.ext: ∀ {C : Type ?u.1257} [inst : Category C] {X Y : C} ⦃α β : X ≅ Y⦄, α.hom = β.hom → α = β
Iso.ext (
map_injective: ∀ {C : Type ?u.1283} [inst : Category C] {D : Type ?u.1282} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective 
F: C ⥤ D
F (
congr_arg: ∀ {α : Sort ?u.1316} {β : Sort ?u.1315} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
Iso.hom: {C : Type ?u.1321} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
Iso.hom 
h: ?m.1255
h : 
_: Sort ?u.1313
_))
#align category_theory.functor.map_iso_injective 
CategoryTheory.Functor.mapIso_injective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Faithful F],
  Function.Injective F.mapIso
CategoryTheory.Functor.mapIso_injective

/-- The specified preimage of a morphism under a full functor. -/
def 
preimage: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Full: {C : Type ?u.1404} →
  [inst : Category C] → {D : Type ?u.1403} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.1404?u.1406)?u.1405)
Full 
F: C ⥤ D
F] (
f: F.obj X ⟶ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.1470} → [inst : Quiver V] → {W : Type ?u.1469} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.1520} → [inst : Quiver V] → {W : Type ?u.1519} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y) : 
X: C
X ⟶ 
Y: C
Y :=
  
Full.preimage: {C : Type ?u.1587} →
  [inst : Category C] →
    {D : Type ?u.1586} →
      [inst_1 : Category D] → {F : C ⥤ D} → [self : Full F] → {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
Full.preimage.{v₁, v₂} 
f: F.obj X ⟶ F.obj Y
f
#align category_theory.functor.preimage 
CategoryTheory.Functor.preimage: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
CategoryTheory.Functor.preimage

pp_extended_field_notation 
preimage: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage

@[simp]
theorem 
image_preimage: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] {X Y : C}
  (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
image_preimage (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Full: {C : Type ?u.9143} →
  [inst : Category C] → {D : Type ?u.9142} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.9143?u.9145)?u.9144)
Full 
F: C ⥤ D
F] {
X: C
X 
Y: C
Y : 
C: Type u₁
C} (
f: F.obj X ⟶ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.9213} → [inst : Quiver V] → {W : Type ?u.9212} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.9263} → [inst : Quiver V] → {W : Type ?u.9262} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y) :
    
F: C ⥤ D
F.
map: {V : Type ?u.9304} →
  [inst : Quiver V] →
    {W : Type ?u.9303} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map (
preimage: {C : Type ?u.9316} →
  [inst : Category C] →
    {D : Type ?u.9315} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
F: C ⥤ D
F 
f: F.obj X ⟶ F.obj Y
f) = 
f: F.obj X ⟶ F.obj Y
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y

F.map (F.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y

F.map (Full.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y

F.map (Full.preimage f) = f
C: Type u₁

inst✝²: Category C

D: Type u₂

inst✝¹: Category D

X✝, Y✝: C

F: C ⥤ D

inst✝: Full F

X, Y: C

f: F.obj X ⟶ F.obj Y

F.map (F.preimage f) = f
Goals accomplished! 🐙

#align category_theory.functor.image_preimage 
CategoryTheory.Functor.image_preimage: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F] {X Y : C}
  (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
CategoryTheory.Functor.image_preimage

theorem 
map_surjective: ∀ (F : C ⥤ D) [inst : Full F], Function.Surjective F.map
map_surjective (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D) [
Full: {C : Type ?u.9770} →
  [inst : Category C] → {D : Type ?u.9769} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.9770?u.9772)?u.9771)
Full 
F: C ⥤ D
F] :
    
Function.Surjective: {α : Sort ?u.9812} → {β : Sort ?u.9811} → (α → β) → Prop
Function.Surjective (
F: C ⥤ D
F.
map: {V : Type ?u.9961} →
  [inst : Quiver V] →
    {W : Type ?u.9960} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map : (
X: C
X ⟶ 
Y: C
Y) → (
F: C ⥤ D
F.
obj: {V : Type ?u.9874} → [inst : Quiver V] → {W : Type ?u.9873} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.9923} → [inst : Quiver V] → {W : Type ?u.9922} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y)) :=
  fun 
f: ?m.9987
f => ⟨
F: C ⥤ D
F.
preimage: {C : Type ?u.10002} →
  [inst : Category C] →
    {D : Type ?u.10001} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: ?m.9987
f, 
F: C ⥤ D
F.
image_preimage: ∀ {C : Type ?u.10032} [inst : Category C] {D : Type ?u.10031} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f
image_preimage 
f: ?m.9987
f⟩
#align category_theory.functor.map_surjective 
CategoryTheory.Functor.map_surjective: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {X Y : C} (F : C ⥤ D) [inst_2 : Full F],
  Function.Surjective F.map
CategoryTheory.Functor.map_surjective

/-- Deduce that `F` is full from the existence of preimages, using choice. -/
noncomputable def 
fullOfExists: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
fullOfExists (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D)
    (
h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f
h : ∀ (
X: C
X 
Y: C
Y : 
C: Type u₁
C) (
f: F.obj X ⟶ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.10144} → [inst : Quiver V] → {W : Type ?u.10143} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.10194} → [inst : Quiver V] → {W : Type ?u.10193} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y), ∃ 
p: ?m.10226
p, 
F: C ⥤ D
F.
map: {V : Type ?u.10240} →
  [inst : Quiver V] →
    {W : Type ?u.10239} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
p: ?m.10226
p = 
f: F.obj X ⟶ F.obj Y
f) : 
Full: {C : Type ?u.10307} →
  [inst : Category C] →
    {D : Type ?u.10306} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.10307?u.10309)?u.10308)
Full 
F: C ⥤ D
F := 
Goals accomplished! 🐙
C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f

Full F
C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

p: (X Y : C) → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)

hp: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.map (p X Y f) = f

Full F
C: Type u₁

inst✝¹: Category C

D: Type u₂

inst✝: Category D

X, Y: C

F: C ⥤ D

h: ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f

Full F
Goals accomplished! 🐙

#align category_theory.functor.full_of_exists 
CategoryTheory.Functor.fullOfExists: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
CategoryTheory.Functor.fullOfExists

/-- Deduce that `F` is full from surjectivity of `F.map`, using choice. -/
noncomputable def 
fullOfSurjective: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C), Function.Surjective F.map) → Full F
fullOfSurjective (
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D)
    (
h: ∀ (X Y : C), Function.Surjective F.map
h : ∀ 
X: C
X 
Y: C
Y : 
C: Type u₁
C, 
Function.Surjective: {α : Sort ?u.10517} → {β : Sort ?u.10516} → (α → β) → Prop
Function.Surjective (
F: C ⥤ D
F.
map: {V : Type ?u.10672} →
  [inst : Quiver V] →
    {W : Type ?u.10671} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map : (
X: C
X ⟶ 
Y: C
Y) → (
F: C ⥤ D
F.
obj: {V : Type ?u.10585} → [inst : Quiver V] → {W : Type ?u.10584} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.10634} → [inst : Quiver V] → {W : Type ?u.10633} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y))) : 
Full: {C : Type ?u.10697} →
  [inst : Category C] →
    {D : Type ?u.10696} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.10697?u.10699)?u.10698)
Full 
F: C ⥤ D
F :=
  
fullOfExists: {C : Type ?u.10735} →
  [inst : Category C] →
    {D : Type ?u.10734} →
      [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, F.map p = f) → Full F
fullOfExists 
_: ?m.10738 ⥤ ?m.10740
_ 
h: ∀ (X Y : C), Function.Surjective F.map
h
#align category_theory.functor.full_of_surjective 
CategoryTheory.Functor.fullOfSurjective: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} → [inst_1 : Category D] → (F : C ⥤ D) → (∀ (X Y : C), Function.Surjective F.map) → Full F
CategoryTheory.Functor.fullOfSurjective

end Functor

section

variable {
F: C ⥤ D
F : 
C: Type u₁
C ⥤ 
D: Type u₂
D} [
Full: {C : Type ?u.11454} →
  [inst : Category C] →
    {D : Type ?u.11453} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.11454?u.11456)?u.11455)
Full 
F: C ⥤ D
F] [
Faithful: {C : Type ?u.12751} → [inst : Category C] → {D : Type ?u.12750} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] {
X: C
X 
Y: C
Y 
Z: C
Z : 
C: Type u₁
C}

@[simp]
theorem 
preimage_id: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X : C}, F.preimage (𝟙 (F.obj X)) = 𝟙 X
preimage_id : 
F: C ⥤ D
F.
preimage: {C : Type ?u.11020} →
  [inst : Category C] →
    {D : Type ?u.11019} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage (
𝟙: (X : ?m.11047) → X ⟶ X
𝟙 (
F: C ⥤ D
F.
obj: {V : Type ?u.11081} → [inst : Quiver V] → {W : Type ?u.11080} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X)) = 
𝟙: (X : ?m.11157) → X ⟶ X
𝟙 
X: C
X :=
  
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.11186} [inst : Category C] {D : Type ?u.11185} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)
Goals accomplished! 🐙
)
#align category_theory.preimage_id 
CategoryTheory.preimage_id: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X : C}, F.preimage (𝟙 (F.obj X)) = 𝟙 X
CategoryTheory.preimage_id

@[simp]
theorem 
preimage_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z),
  F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g
preimage_comp (
f: F.obj X ⟶ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.11570} → [inst : Quiver V] → {W : Type ?u.11569} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.11620} → [inst : Quiver V] → {W : Type ?u.11619} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y) (
g: F.obj Y ⟶ F.obj Z
g : 
F: C ⥤ D
F.
obj: {V : Type ?u.11672} → [inst : Quiver V] → {W : Type ?u.11671} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.11692} → [inst : Quiver V] → {W : Type ?u.11691} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Z: C
Z) :
    
F: C ⥤ D
F.
preimage: {C : Type ?u.11722} →
  [inst : Category C] →
    {D : Type ?u.11721} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage (
f: F.obj X ⟶ F.obj Y
f ≫ 
g: F.obj Y ⟶ F.obj Z
g) = 
F: C ⥤ D
F.
preimage: {C : Type ?u.11807} →
  [inst : Category C] →
    {D : Type ?u.11806} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: F.obj X ⟶ F.obj Y
f ≫ 
F: C ⥤ D
F.
preimage: {C : Type ?u.11842} →
  [inst : Category C] →
    {D : Type ?u.11841} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
g: F.obj Y ⟶ F.obj Z
g :=
  
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.11877} [inst : Category C] {D : Type ?u.11876} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ⟶ F.obj Y

g: F.obj Y ⟶ F.obj Z

F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)
Goals accomplished! 🐙
)
#align category_theory.preimage_comp 
CategoryTheory.preimage_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z),
  F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g
CategoryTheory.preimage_comp

@[simp]
theorem 
preimage_map: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), F.preimage (F.map f) = f
preimage_map (
f: X ⟶ Y
f : 
X: C
X ⟶ 
Y: C
Y) : 
F: C ⥤ D
F.
preimage: {C : Type ?u.12378} →
  [inst : Category C] →
    {D : Type ?u.12377} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage (
F: C ⥤ D
F.
map: {V : Type ?u.12419} →
  [inst : Quiver V] →
    {W : Type ?u.12418} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
f: X ⟶ Y
f) = 
f: X ⟶ Y
f :=
  
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.12488} [inst : Category C] {D : Type ?u.12487} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ⟶ Y

F.map (F.preimage (F.map f)) = F.map f
Goals accomplished! 🐙
)
#align category_theory.preimage_map 
CategoryTheory.preimage_map: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F : C ⥤ D} [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), F.preimage (F.map f) = f
CategoryTheory.preimage_map

variable (
F: ?m.12792
F)

namespace Functor

/-- If `F : C ⥤ D` is fully faithful, every isomorphism `F.obj X ≅ F.obj Y` has a preimage. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).inv = F.preimage f.inv
simps]
def 
preimageIso: (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso (
f: F.obj X ≅ F.obj Y
f : 
F: C ⥤ D
F.
obj: {V : Type ?u.12939} → [inst : Quiver V] → {W : Type ?u.12938} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: C
X ≅ 
F: C ⥤ D
F.
obj: {V : Type ?u.12989} → [inst : Quiver V] → {W : Type ?u.12988} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: C
Y) :
    
X: C
X ≅ 
Y: C
Y where
  hom := 
F: C ⥤ D
F.
preimage: {C : Type ?u.13033} →
  [inst : Category C] →
    {D : Type ?u.13032} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: F.obj X ≅ F.obj Y
f.
hom: {C : Type ?u.13069} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom
  inv := 
F: C ⥤ D
F.
preimage: {C : Type ?u.13081} →
  [inst : Category C] →
    {D : Type ?u.13080} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: F.obj X ≅ F.obj Y
f.
inv: {C : Type ?u.13102} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv
  hom_inv_id := 
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.13110} [inst : Category C] {D : Type ?u.13109} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ≅ F.obj Y

F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)
Goals accomplished! 🐙
)
  inv_hom_id := 
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.13151} [inst : Category C] {D : Type ?u.13150} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: F.obj X ≅ F.obj Y

F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)
Goals accomplished! 🐙
)
#align category_theory.functor.preimage_iso 
CategoryTheory.Functor.preimageIso: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
CategoryTheory.Functor.preimageIso
#align category_theory.functor.preimage_iso_inv 
CategoryTheory.Functor.preimageIso_inv: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).inv = F.preimage f.inv
CategoryTheory.Functor.preimageIso_inv
#align category_theory.functor.preimage_iso_hom 
CategoryTheory.Functor.preimageIso_hom: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), (preimageIso F f).hom = F.preimage f.hom
CategoryTheory.Functor.preimageIso_hom

@[simp]
theorem 
preimageIso_mapIso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), preimageIso F (F.mapIso f) = f
preimageIso_mapIso (
f: X ≅ Y
f : 
X: C
X ≅ 
Y: C
Y) : 
F: C ⥤ D
F.
preimageIso: {C : Type ?u.13998} →
  [inst : Category C] →
    {D : Type ?u.13997} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso (
F: C ⥤ D
F.
mapIso: {C : Type ?u.14027} →
  [inst : Category C] →
    {D : Type ?u.14026} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso 
f: X ≅ Y
f) = 
f: X ≅ Y
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y

preimageIso F (F.mapIso f) = f
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y

w
(preimageIso F (F.mapIso f)).hom = f.hom
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X, Y, Z: C

f: X ≅ Y

preimageIso F (F.mapIso f) = f
Goals accomplished! 🐙

#align category_theory.functor.preimage_iso_map_iso 
CategoryTheory.Functor.preimageIso_mapIso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), preimageIso F (F.mapIso f) = f
CategoryTheory.Functor.preimageIso_mapIso

end Functor

/-- 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) [inst : IsIso (F.map f)], IsIso f
isIso_of_fully_faithful (
f: X ⟶ Y
f : 
X: C
X ⟶ 
Y: C
Y) [
IsIso: {C : Type ?u.14582} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
IsIso (
F: C ⥤ D
F.
map: {V : Type ?u.14617} →
  [inst : Quiver V] →
    {W : Type ?u.14616} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
f: X ⟶ Y
f)] : 
IsIso: {C : Type ?u.14670} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
IsIso 
f: X ⟶ Y
f :=
  ⟨⟨
F: C ⥤ D
F.
preimage: {C : Type ?u.14737} →
  [inst : Category C] →
    {D : Type ?u.14736} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage (
inv: {C : Type ?u.14771} → [inst : Category C] → {X Y : C} → (f : X ⟶ Y) → [I : IsIso f] → Y ⟶ X
inv (
F: C ⥤ D
F.
map: {V : Type ?u.14804} →
  [inst : Quiver V] →
    {W : Type ?u.14803} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
f: X ⟶ Y
f)), ⟨
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.14859} [inst : Category C] {D : Type ?u.14858} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

F: C ⥤ D

inst✝²: Full F

inst✝¹: Faithful F

X, Y, Z: C

f: X ⟶ Y

inst✝: IsIso (F.map f)

F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)
Goals accomplished! 🐙
), 
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.14900} [inst : Category C] {D : Type ?u.14899} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

F: C ⥤ D

inst✝²: Full F

inst✝¹: Faithful F

X, Y, Z: C

f: X ⟶ Y

inst✝: IsIso (F.map f)

F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)
Goals accomplished! 🐙
)⟩⟩⟩
#align category_theory.is_iso_of_fully_faithful 
CategoryTheory.isIso_of_fully_faithful: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y) [inst_4 : IsIso (F.map f)], IsIso f
CategoryTheory.isIso_of_fully_faithful

/-- If `F` is fully faithful, we have an equivalence of hom-sets `X ⟶ Y` and `F X ⟶ F Y`. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ⟶ F.obj Y), ↑(equivOfFullyFaithful F).symm f = F.preimage f
simps]
def 
equivOfFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
equivOfFullyFaithful {
X: ?m.15514
X 
Y: ?m.15517
Y} :
    (
X: ?m.15514
X ⟶ 
Y: ?m.15517
Y) ≃ (
F: C ⥤ D
F.
obj: {V : Type ?u.15582} → [inst : Quiver V] → {W : Type ?u.15581} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: ?m.15514
X ⟶ 
F: C ⥤ D
F.
obj: {V : Type ?u.15632} → [inst : Quiver V] → {W : Type ?u.15631} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: ?m.15517
Y) where
  toFun 
f: ?m.15687
f := 
F: C ⥤ D
F.
map: {V : Type ?u.15700} →
  [inst : Quiver V] →
    {W : Type ?u.15699} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
f: ?m.15687
f
  invFun 
f: ?m.15724
f := 
F: C ⥤ D
F.
preimage: {C : Type ?u.15727} →
  [inst : Category C] →
    {D : Type ?u.15726} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage 
f: ?m.15724
f
  left_inv 
f: ?m.15766
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: X ⟶ Y

(fun f => F.preimage f) ((fun f => F.map f) f) = f
Goals accomplished! 🐙

  right_inv 
f: ?m.15772
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ⟶ F.obj Y

(fun f => F.map f) ((fun f => F.preimage f) f) = f
Goals accomplished! 🐙

#align category_theory.equiv_of_fully_faithful 
CategoryTheory.equivOfFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
CategoryTheory.equivOfFullyFaithful
#align category_theory.equiv_of_fully_faithful_apply 
CategoryTheory.equivOfFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ⟶ Y), ↑(equivOfFullyFaithful F) f = F.map f
CategoryTheory.equivOfFullyFaithful_apply
#align category_theory.equiv_of_fully_faithful_symm_apply 
CategoryTheory.equivOfFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ⟶ F.obj Y), ↑(equivOfFullyFaithful F).symm f = F.preimage f
CategoryTheory.equivOfFullyFaithful_symm_apply

/-- If `F` is fully faithful, we have an equivalence of iso-sets `X ≅ Y` and `F X ≅ F Y`. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), ↑(isoEquivOfFullyFaithful F).symm f = Functor.preimageIso F f
simps]
def 
isoEquivOfFullyFaithful: {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
isoEquivOfFullyFaithful {
X: C
X 
Y: ?m.16316
Y} :
    (
X: ?m.16313
X ≅ 
Y: ?m.16316
Y) ≃ (
F: C ⥤ D
F.
obj: {V : Type ?u.16385} → [inst : Quiver V] → {W : Type ?u.16384} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: ?m.16313
X ≅ 
F: C ⥤ D
F.
obj: {V : Type ?u.16435} → [inst : Quiver V] → {W : Type ?u.16434} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
Y: ?m.16316
Y) where
  toFun 
f: ?m.16460
f := 
F: C ⥤ D
F.
mapIso: {C : Type ?u.16464} →
  [inst : Category C] →
    {D : Type ?u.16463} → [inst_1 : Category D] → (F : C ⥤ D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
mapIso 
f: ?m.16460
f
  invFun 
f: ?m.16499
f := 
F: C ⥤ D
F.
preimageIso: {C : Type ?u.16502} →
  [inst : Category C] →
    {D : Type ?u.16501} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (F.obj X ≅ F.obj Y) → (X ≅ Y)
preimageIso 
f: ?m.16499
f
  left_inv 
f: ?m.16550
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: X ≅ Y

(fun f => Functor.preimageIso F f) ((fun f => F.mapIso f) f) = f
Goals accomplished! 🐙

  right_inv 
f: ?m.16556
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y

(fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f) = f
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y

w
((fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f)).hom = f.hom
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

F: C ⥤ D

inst✝¹: Full F

inst✝: Faithful F

X✝, Y✝, Z, X, Y: C

f: F.obj X ≅ F.obj Y

(fun f => F.mapIso f) ((fun f => Functor.preimageIso F f) f) = f
Goals accomplished! 🐙

#align category_theory.iso_equiv_of_fully_faithful 
CategoryTheory.isoEquivOfFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
CategoryTheory.isoEquivOfFullyFaithful
#align category_theory.iso_equiv_of_fully_faithful_symm_apply 
CategoryTheory.isoEquivOfFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : F.obj X ≅ F.obj Y), ↑(isoEquivOfFullyFaithful F).symm f = Functor.preimageIso F f
CategoryTheory.isoEquivOfFullyFaithful_symm_apply
#align category_theory.iso_equiv_of_fully_faithful_apply 
CategoryTheory.isoEquivOfFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] (F : C ⥤ D) [inst_2 : Full F]
  [inst_3 : Faithful F] {X Y : C} (f : X ≅ Y), ↑(isoEquivOfFullyFaithful F) f = F.mapIso f
CategoryTheory.isoEquivOfFullyFaithful_apply

end

section

variable {
E: Type ?u.17178
E : 
Type _: Type (?u.17178+1)
Type _} [
Category: Type ?u.17181 → Type (max?u.17181(?u.17182+1))
Category 
E: Type ?u.17318
E] {
F: C ⥤ D
F 
G: C ⥤ D
G : 
C: Type u₁
C ⥤ 
D: Type u₂
D} (
H: D ⥤ E
H : 
D: Type u₂
D ⥤ 
E: Type ?u.17318
E) [
Full: {C : Type ?u.22200} →
  [inst : Category C] →
    {D : Type ?u.22199} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.22200?u.22202)?u.22201)
Full 
H: D ⥤ E
H] [
Faithful: {C : Type ?u.17273} → [inst : Category C] → {D : Type ?u.17272} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
H: D ⥤ E
H]

/-- We can construct a natural transformation between functors by constructing a
natural transformation between those functors composed with a fully faithful functor. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C),
  (natTransOfCompFullyFaithful H α).app X = ↑(equivOfFullyFaithful H).symm (α.app X)
simps]
def 
natTransOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful (
α: F ⋙ H ⟶ G ⋙ H
α : 
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ⟶ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) :
    
F: C ⥤ D
F ⟶ 
G: C ⥤ D
G where
  app 
X: ?m.17684
X := (
equivOfFullyFaithful: {C : Type ?u.17687} →
  [inst : Category C] →
    {D : Type ?u.17686} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)
equivOfFullyFaithful 
H: D ⥤ E
H).
symm: {α : Sort ?u.17727} → {β : Sort ?u.17726} → α ≃ β → β ≃ α
symm (
α: F ⋙ H ⟶ G ⋙ H
α.
app: {C : Type ?u.17803} →
  [inst : Category C] →
    {D : Type ?u.17802} → [inst_1 : Category D] → {F G : C ⥤ D} → NatTrans F G → (X : C) → F.obj X ⟶ G.obj X
app 
X: ?m.17684
X)
  naturality 
X: ?m.17840
X 
Y: ?m.17843
Y 
f: ?m.17846
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y

F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y =   (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y

F.map f ≫ H.preimage (α.app Y) = H.preimage (α.app X) ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y

F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y =   (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y

a
H.map (F.map f ≫ H.preimage (α.app Y)) = H.map (H.preimage (α.app X) ≫ G.map f)
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.17318

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

α: F ⋙ H ⟶ G ⋙ H

X, Y: C

f: X ⟶ Y

F.map f ≫ (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) Y =   (fun X => ↑(equivOfFullyFaithful H).symm (α.app X)) X ≫ G.map f
Goals accomplished! 🐙

#align category_theory.nat_trans_of_comp_fully_faithful 
CategoryTheory.natTransOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
CategoryTheory.natTransOfCompFullyFaithful
#align category_theory.nat_trans_of_comp_fully_faithful_app 
CategoryTheory.natTransOfCompFullyFaithful_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C),
  (natTransOfCompFullyFaithful H α).app X = ↑(equivOfFullyFaithful H).symm (α.app X)
CategoryTheory.natTransOfCompFullyFaithful_app

/-- We can construct a natural isomorphism between functors by constructing a natural isomorphism
between those functors composed with a fully faithful functor. -/
@[simps!]
def 
natIsoOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful (
i: F ⋙ H ≅ G ⋙ H
i : 
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ≅ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) : 
F: C ⥤ D
F ≅ 
G: C ⥤ D
G :=
  
NatIso.ofComponents: {C : Type ?u.19746} →
  [inst : Category C] →
    {D : Type ?u.19745} →
      [inst_1 : Category D] →
        {F G : C ⥤ D} →
          (app : (X : C) → F.obj X ≅ G.obj X) →
            (∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) → (F ≅ G)
NatIso.ofComponents (fun 
X: ?m.19788
X => (
isoEquivOfFullyFaithful: {C : Type ?u.19791} →
  [inst : Category C] →
    {D : Type ?u.19790} →
      [inst_1 : Category D] →
        (F : C ⥤ D) → [inst_2 : Full F] → [inst_3 : Faithful F] → {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
isoEquivOfFullyFaithful 
H: D ⥤ E
H).
symm: {α : Sort ?u.19831} → {β : Sort ?u.19830} → α ≃ β → β ≃ α
symm (
i: F ⋙ H ≅ G ⋙ H
i.
app: {C : Type ?u.19907} →
  [inst : Category C] →
    {D : Type ?u.19906} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app 
X: ?m.19788
X)) fun 
f: ?m.19962
f => 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝

F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom =   ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝

F.map f ≫ H.preimage (i.hom.app Y✝) = H.preimage (i.hom.app X✝) ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝

F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom =   ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝

a
H.map (F.map f ≫ H.preimage (i.hom.app Y✝)) = H.map (H.preimage (i.hom.app X✝) ≫ G.map f)
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.19429

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

X✝, Y✝: C

f: X✝ ⟶ Y✝

F.map f ≫ ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) Y✝).hom =   ((fun X => ↑(isoEquivOfFullyFaithful H).symm (i.app X)) X✝).hom ≫ G.map f
Goals accomplished! 🐙

#align category_theory.nat_iso_of_comp_fully_faithful 
CategoryTheory.natIsoOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
CategoryTheory.natIsoOfCompFullyFaithful
#align category_theory.nat_iso_of_comp_fully_faithful_hom_app 
CategoryTheory.natIsoOfCompFullyFaithful_hom_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C),
  (natIsoOfCompFullyFaithful H i).hom.app X = H.preimage (i.hom.app X)
CategoryTheory.natIsoOfCompFullyFaithful_hom_app
#align category_theory.nat_iso_of_comp_fully_faithful_inv_app 
CategoryTheory.natIsoOfCompFullyFaithful_inv_app: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C),
  (natIsoOfCompFullyFaithful H i).inv.app X = H.preimage (i.inv.app X)
CategoryTheory.natIsoOfCompFullyFaithful_inv_app

theorem 
natIsoOfCompFullyFaithful_hom: ∀ (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
natIsoOfCompFullyFaithful_hom (
i: F ⋙ H ≅ G ⋙ H
i : 
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ≅ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) :
    (
natIsoOfCompFullyFaithful: {C : Type ?u.22433} →
  [inst : Category C] →
    {D : Type ?u.22432} →
      [inst_1 : Category D] →
        {E : Type ?u.22431} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful 
H: D ⥤ E
H 
i: F ⋙ H ≅ G ⋙ H
i).
hom: {C : Type ?u.22503} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom = 
natTransOfCompFullyFaithful: {C : Type ?u.22535} →
  [inst : Category C] →
    {D : Type ?u.22534} →
      [inst_1 : Category D] →
        {E : Type ?u.22533} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful 
H: D ⥤ E
H 
i: F ⋙ H ≅ G ⋙ H
i.
hom: {C : Type ?u.22554} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

(natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

x✝: C

w.h
(natIsoOfCompFullyFaithful H i).hom.app x✝ = (natTransOfCompFullyFaithful H i.hom).app x✝
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

(natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
Goals accomplished! 🐙

#align category_theory.nat_iso_of_comp_fully_faithful_hom 
CategoryTheory.natIsoOfCompFullyFaithful_hom: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_2} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H),
  (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
CategoryTheory.natIsoOfCompFullyFaithful_hom

theorem 
natIsoOfCompFullyFaithful_inv: ∀ (i : F ⋙ H ≅ G ⋙ H), (natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
natIsoOfCompFullyFaithful_inv (
i: F ⋙ H ≅ G ⋙ H
i : 
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ≅ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) :
    (
natIsoOfCompFullyFaithful: {C : Type ?u.24093} →
  [inst : Category C] →
    {D : Type ?u.24092} →
      [inst_1 : Category D] →
        {E : Type ?u.24091} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful 
H: D ⥤ E
H 
i: F ⋙ H ≅ G ⋙ H
i).
inv: {C : Type ?u.24163} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv = 
natTransOfCompFullyFaithful: {C : Type ?u.24195} →
  [inst : Category C] →
    {D : Type ?u.24194} →
      [inst_1 : Category D] →
        {E : Type ?u.24193} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful 
H: D ⥤ E
H 
i: F ⋙ H ≅ G ⋙ H
i.
inv: {C : Type ?u.24214} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

(natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

x✝: C

w.h
(natIsoOfCompFullyFaithful H i).inv.app x✝ = (natTransOfCompFullyFaithful H i.inv).app x✝
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type u_2

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

i: F ⋙ H ≅ G ⋙ H

(natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
Goals accomplished! 🐙

#align category_theory.nat_iso_of_comp_fully_faithful_inv 
CategoryTheory.natIsoOfCompFullyFaithful_inv: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_2} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H),
  (natIsoOfCompFullyFaithful H i).inv = natTransOfCompFullyFaithful H i.inv
CategoryTheory.natIsoOfCompFullyFaithful_inv

/-- Horizontal composition with a fully faithful functor induces a bijection on
natural transformations. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H),
  ↑(equivOfCompFullyFaithful H).symm α = natTransOfCompFullyFaithful H α
simps]
def 
NatTrans.equivOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)
NatTrans.equivOfCompFullyFaithful :
    (
F: C ⥤ D
F ⟶ 
G: C ⥤ D
G) ≃ (
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ⟶ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) where
  toFun 
α: ?m.25281
α := 
α: ?m.25281
α ◫ 
𝟙: (X : ?m.25347) → X ⟶ X
𝟙 
H: D ⥤ E
H
  invFun := 
natTransOfCompFullyFaithful: {C : Type ?u.25398} →
  [inst : Category C] →
    {D : Type ?u.25397} →
      [inst_1 : Category D] →
        {E : Type ?u.25396} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ⟶ G ⋙ H) → (F ⟶ G)
natTransOfCompFullyFaithful 
H: D ⥤ E
H
  left_inv := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.24929

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

Function.LeftInverse (natTransOfCompFullyFaithful H) fun α => α ◫ 𝟙 H
Goals accomplished! 🐙

  right_inv := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.24929

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

Function.RightInverse (natTransOfCompFullyFaithful H) fun α => α ◫ 𝟙 H
Goals accomplished! 🐙

#align category_theory.nat_trans.equiv_of_comp_fully_faithful 
CategoryTheory.NatTrans.equivOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)
CategoryTheory.NatTrans.equivOfCompFullyFaithful
#align category_theory.nat_trans.equiv_of_comp_fully_faithful_apply 
CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⟶ G),
  ↑(NatTrans.equivOfCompFullyFaithful H) α = α ◫ 𝟙 H
CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply
#align category_theory.nat_trans.equiv_of_comp_fully_faithful_symm_apply 
CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (α : F ⋙ H ⟶ G ⋙ H),
  ↑(NatTrans.equivOfCompFullyFaithful H).symm α = natTransOfCompFullyFaithful H α
CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply

/-- Horizontal composition with a fully faithful functor induces a bijection on
natural isomorphisms. -/
@[
simps: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (e : F ≅ G),
  ↑(equivOfCompFullyFaithful H) e = hcomp e (Iso.refl H)
simps]
def 
NatIso.equivOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)
NatIso.equivOfCompFullyFaithful :
    (
F: C ⥤ D
F ≅ 
G: C ⥤ D
G) ≃ (
F: C ⥤ D
F ⋙ 
H: D ⥤ E
H ≅ 
G: C ⥤ D
G ⋙ 
H: D ⥤ E
H) where
  toFun 
e: ?m.28637
e := 
NatIso.hcomp: {C : Type ?u.28641} →
  [inst : Category C] →
    {D : Type ?u.28640} →
      [inst_1 : Category D] →
        {E : Type ?u.28639} →
          [inst_2 : Category E] → {F G : C ⥤ D} → {H I : D ⥤ E} → (F ≅ G) → (H ≅ I) → (F ⋙ H ≅ G ⋙ I)
NatIso.hcomp 
e: ?m.28637
e (
Iso.refl: {C : Type ?u.28705} → [inst : Category C] → (X : C) → X ≅ X
Iso.refl 
H: D ⥤ E
H)
  invFun := 
natIsoOfCompFullyFaithful: {C : Type ?u.28740} →
  [inst : Category C] →
    {D : Type ?u.28739} →
      [inst_1 : Category D] →
        {E : Type ?u.28738} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ⋙ H ≅ G ⋙ H) → (F ≅ G)
natIsoOfCompFullyFaithful 
H: D ⥤ E
H
  left_inv := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.28315

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

Function.LeftInverse (natIsoOfCompFullyFaithful H) fun e => hcomp e (Iso.refl H)
Goals accomplished! 🐙

  right_inv := 
Goals accomplished! 🐙
C: Type u₁

inst✝⁴: Category C

D: Type u₂

inst✝³: Category D

E: Type ?u.28315

inst✝²: Category E

F, G: C ⥤ D

H: D ⥤ E

inst✝¹: Full H

inst✝: Faithful H

Function.RightInverse (natIsoOfCompFullyFaithful H) fun e => hcomp e (Iso.refl H)
Goals accomplished! 🐙

#align category_theory.nat_iso.equiv_of_comp_fully_faithful 
CategoryTheory.NatIso.equivOfCompFullyFaithful: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u_1} →
          [inst_2 : Category E] →
            {F G : C ⥤ D} → (H : D ⥤ E) → [inst_3 : Full H] → [inst_4 : Faithful H] → (F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)
CategoryTheory.NatIso.equivOfCompFullyFaithful
#align category_theory.nat_iso.equiv_of_comp_fully_faithful_symm_apply 
CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (i : F ⋙ H ≅ G ⋙ H),
  ↑(NatIso.equivOfCompFullyFaithful H).symm i = natIsoOfCompFullyFaithful H i
CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply
#align category_theory.nat_iso.equiv_of_comp_fully_faithful_apply 
CategoryTheory.NatIso.equivOfCompFullyFaithful_apply: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u_1} [inst_2 : Category E]
  {F G : C ⥤ D} (H : D ⥤ E) [inst_3 : Full H] [inst_4 : Faithful H] (e : F ≅ G),
  ↑(NatIso.equivOfCompFullyFaithful H) e = NatIso.hcomp e (Iso.refl H)
CategoryTheory.NatIso.equivOfCompFullyFaithful_apply

end

end CategoryTheory

namespace CategoryTheory

variable {
C: Type u₁
C : 
Type u₁: Type (u₁+1)
Type u₁} [
Category: Type ?u.34795 → Type (max?u.34795(v₁+1))
Category.{v₁} 
C: Type u₁
C]

instance 
Full.id: Full (𝟭 C)
Full.id : 
Full: {C : Type ?u.31765} →
  [inst : Category C] →
    {D : Type ?u.31764} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.31765?u.31767)?u.31766)
Full (
𝟭: (C : Type ?u.31790) → [inst : Category C] → C ⥤ C
𝟭 
C: Type u₁
C) where preimage 
f: ?m.31831
f := 
f: ?m.31831
f
#align category_theory.full.id 
CategoryTheory.Full.id: {C : Type u₁} → [inst : Category C] → Full (𝟭 C)
CategoryTheory.Full.id

instance 
Faithful.id: ∀ {C : Type u₁} [inst : Category C], Faithful (𝟭 C)
Faithful.id : 
Faithful: {C : Type ?u.32209} → [inst : Category C] → {D : Type ?u.32208} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful (
𝟭: (C : Type ?u.32234) → [inst : Category C] → C ⥤ C
𝟭 
C: Type u₁
C) := 
{ }: Faithful ?m.32346
{ }
#align category_theory.faithful.id 
CategoryTheory.Faithful.id: ∀ {C : Type u₁} [inst : Category C], Faithful (𝟭 C)
CategoryTheory.Faithful.id

variable {
D: Type u₂
D : 
Type u₂: Type (u₂+1)
Type u₂} [
Category: Type ?u.33275 → Type (max?u.33275(v₂+1))
Category.{v₂} 
D: Type u₂
D] {
E: Type u₃
E : 
Type u₃: Type (u₃+1)
Type u₃} [
Category: Type ?u.33280 → Type (max?u.33280(v₃+1))
Category.{v₃} 
E: Type u₃
E]

variable (
F: C ⥤ D
F 
F': C ⥤ D
F' : 
C: Type u₁
C ⥤ 
D: Type u₂
D) (
G: D ⥤ E
G : 
D: Type u₂
D ⥤ 
E: Type u₃
E)

instance 
Faithful.comp: ∀ [inst : Faithful F] [inst : Faithful G], Faithful (F ⋙ G)
Faithful.comp [
Faithful: {C : Type ?u.32881} → [inst : Category C] → {D : Type ?u.32880} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] [
Faithful: {C : Type ?u.32925} → [inst : Category C] → {D : Type ?u.32924} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
G: D ⥤ E
G] :
    
Faithful: {C : Type ?u.32967} → [inst : Category C] → {D : Type ?u.32966} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful (
F: C ⥤ D
F ⋙ 
G: D ⥤ E
G) where map_injective 
p: ?m.33081
p := 
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.33084} [inst : Category C] {D : Type ?u.33083} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
G: D ⥤ E
G.
map_injective: ∀ {C : Type ?u.33129} [inst : Category C] {D : Type ?u.33128} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective 
p: ?m.33081
p)
#align category_theory.faithful.comp 
CategoryTheory.Faithful.comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] (F : C ⥤ D)
  (G : D ⥤ E) [inst_3 : Faithful F] [inst_4 : Faithful G], Faithful (F ⋙ G)
CategoryTheory.Faithful.comp

theorem 
Faithful.of_comp: ∀ [inst : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp [
Faithful: {C : Type ?u.33329} → [inst : Category C] → {D : Type ?u.33328} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful <| 
F: C ⥤ D
F ⋙ 
G: D ⥤ E
G] : 
Faithful: {C : Type ?u.33434} → [inst : Category C] → {D : Type ?u.33433} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F :=
  -- Porting note: (F ⋙ G).map_injective.of_comp has the incorrect type
  { map_injective := fun {
_: ?m.33488
_ 
_: ?m.33491
_} => 
Function.Injective.of_comp: ∀ {α : Sort ?u.33495} {β : Sort ?u.33494} {γ : Sort ?u.33493} {f : α → β} {g : γ → α},
  Function.Injective (f ∘ g) → Function.Injective g
Function.Injective.of_comp (
F: C ⥤ D
F ⋙ 
G: D ⥤ E
G).
map_injective: ∀ {C : Type ?u.33534} [inst : Category C] {D : Type ?u.33533} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective }
#align category_theory.faithful.of_comp 
CategoryTheory.Faithful.of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] (F : C ⥤ D)
  (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
CategoryTheory.Faithful.of_comp

section

variable {
F: ?m.33662
F 
F': ?m.33665
F'}

/-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full. -/
def 
Full.ofIso: [inst : Full F] → (F ≅ F') → Full F'
Full.ofIso [
Full: {C : Type ?u.33729} →
  [inst : Category C] →
    {D : Type ?u.33728} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.33729?u.33731)?u.33730)
Full 
F: C ⥤ D
F] (
α: F ≅ F'
α : 
F: C ⥤ D
F ≅ 
F': C ⥤ D
F') :
    
Full: {C : Type ?u.33808} →
  [inst : Category C] →
    {D : Type ?u.33807} → [inst_1 : Category D] → C ⥤ D → Type (max(max?u.33808?u.33810)?u.33809)
Full 
F': C ⥤ D
F' where
  preimage {
X: ?m.33863
X 
Y: ?m.33866
Y} 
f: ?m.33869
f := 
F: C ⥤ D
F.
preimage: {C : Type ?u.33872} →
  [inst : Category C] →
    {D : Type ?u.33871} →
      [inst_1 : Category D] → {X Y : C} → (F : C ⥤ D) → [inst_2 : Full F] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
preimage ((
α: F ≅ F'
α.
app: {C : Type ?u.33933} →
  [inst : Category C] →
    {D : Type ?u.33932} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app 
X: ?m.33863
X).
hom: {C : Type ?u.33964} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
hom ≫ 
f: ?m.33869
f ≫ (
α: F ≅ F'
α.
app: {C : Type ?u.34006} →
  [inst : Category C] →
    {D : Type ?u.34005} → [inst_1 : Category D] → {F G : C ⥤ D} → (F ≅ G) → (X : C) → F.obj X ≅ G.obj X
app 
Y: ?m.33866
Y).
inv: {C : Type ?u.34029} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
inv)
  witness 
f: ?m.34051
f := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Full F

α: F ≅ F'

X✝, Y✝: C

f: F'.obj X✝ ⟶ F'.obj Y✝

F'.map ((fun {X Y} f => F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) f) = f
Goals accomplished! 🐙

#align category_theory.full.of_iso 
CategoryTheory.Full.ofIso: {C : Type u₁} →
  [inst : Category C] → {D : Type u₂} → [inst_1 : Category D] → {F F' : C ⥤ D} → [inst_2 : Full F] → (F ≅ F') → Full F'
CategoryTheory.Full.ofIso

theorem 
Faithful.of_iso: ∀ [inst : Faithful F], (F ≅ F') → Faithful F'
Faithful.of_iso [
Faithful: {C : Type ?u.34854} → [inst : Category C] → {D : Type ?u.34853} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F] (
α: F ≅ F'
α : 
F: C ⥤ D
F ≅ 
F': C ⥤ D
F') : 
Faithful: {C : Type ?u.34933} → [inst : Category C] → {D : Type ?u.34932} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F': C ⥤ D
F' :=
  { map_injective := fun 
h: ?m.34992
h =>
      
F: C ⥤ D
F.
map_injective: ∀ {C : Type ?u.34995} [inst : Category C] {D : Type ?u.34994} [inst_1 : Category D] {X Y : C} (F : C ⥤ D)
  [inst_2 : Faithful F], Function.Injective F.map
map_injective (
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

α.symm.inv.app X✝ ≫ F'.map a₁✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

α.symm.inv.app X✝ ≫ F'.map a₂✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

F.map a₁✝ = F.map a₂✝
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F, F': C ⥤ D

G: D ⥤ E

inst✝: Faithful F

α: F ≅ F'

X✝, Y✝: C

a₁✝, a₂✝: X✝ ⟶ Y✝

h: F'.map a₁✝ = F'.map a₂✝

F.map a₂✝ = F.map a₂✝
Goals accomplished! 🐙
) }
#align category_theory.faithful.of_iso 
CategoryTheory.Faithful.of_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {F F' : C ⥤ D} [inst_2 : Faithful F],
  (F ≅ F') → Faithful F'
CategoryTheory.Faithful.of_iso

end

variable {
F: ?m.35253
F 
G: ?m.35256
G}

theorem 
Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
Faithful.of_comp_iso {
H: C ⥤ E
H : 
C: Type u₁
C ⥤ 
E: Type u₃
E} [
Faithful: {C : Type ?u.35336} → [inst : Category C] → {D : Type ?u.35335} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
H: C ⥤ E
H] (
h: F ⋙ G ≅ H
h : 
F: C ⥤ D
F ⋙ 
G: D ⥤ E
G ≅ 
H: C ⥤ E
H) : 
Faithful: {C : Type ?u.35476} → [inst : Category C] → {D : Type ?u.35475} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F :=
  @
Faithful.of_comp: ∀ {C : Type ?u.35513} [inst : Category C] {D : Type ?u.35512} [inst_1 : Category D] {E : Type ?u.35511}
  [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp 
_: Type ?u.35513
_ _ 
_: Type ?u.35512
_ _ 
_: Type ?u.35511
_ _ 
F: C ⥤ D
F 
G: D ⥤ E
G (
Faithful.of_iso: ∀ {C : Type ?u.35551} [inst : Category C] {D : Type ?u.35550} [inst_1 : Category D] {F F' : C ⥤ D}
  [inst_2 : Faithful F], (F ≅ F') → Faithful F'
Faithful.of_iso 
h: F ⋙ G ≅ H
h.
symm: {C : Type ?u.35600} → [inst : Category C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
symm)
#align category_theory.faithful.of_comp_iso 
CategoryTheory.Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
CategoryTheory.Faithful.of_comp_iso

alias 
Faithful.of_comp_iso: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
Faithful.of_comp_iso ← 
_root_.CategoryTheory.Iso.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
_root_.CategoryTheory.Iso.faithful_of_comp
#align category_theory.iso.faithful_of_comp 
CategoryTheory.Iso.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [inst_3 : Faithful H], (F ⋙ G ≅ H) → Faithful F
CategoryTheory.Iso.faithful_of_comp

-- We could prove this from `Faithful.of_comp_iso` using `eq_to_iso`,
-- but that would introduce a cyclic import.
theorem 
Faithful.of_comp_eq: ∀ {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Faithful.of_comp_eq {
H: C ⥤ E
H : 
C: Type u₁
C ⥤ 
E: Type u₃
E} [
ℋ: Faithful H
ℋ : 
Faithful: {C : Type ?u.35724} → [inst : Category C] → {D : Type ?u.35723} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
H: C ⥤ E
H] (
h: F ⋙ G = H
h : 
F: C ⥤ D
F ⋙ 
G: D ⥤ E
G = 
H: C ⥤ E
H) : 
Faithful: {C : Type ?u.35806} → [inst : Category C] → {D : Type ?u.35805} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
F: C ⥤ D
F :=
  @
Faithful.of_comp: ∀ {C : Type ?u.35843} [inst : Category C] {D : Type ?u.35842} [inst_1 : Category D] {E : Type ?u.35841}
  [inst_2 : Category E] (F : C ⥤ D) (G : D ⥤ E) [inst_3 : Faithful (F ⋙ G)], Faithful F
Faithful.of_comp 
_: Type ?u.35843
_ _ 
_: Type ?u.35842
_ _ 
_: Type ?u.35841
_ _ 
F: C ⥤ D
F 
G: D ⥤ E
G (
h: F ⋙ G = H
h.
symm: ∀ {α : Sort ?u.35880} {a b : α}, a = b → b = a
symm ▸ 
ℋ: Faithful H
ℋ)
#align category_theory.faithful.of_comp_eq 
CategoryTheory.Faithful.of_comp_eq: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
CategoryTheory.Faithful.of_comp_eq

alias 
Faithful.of_comp_eq: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Faithful.of_comp_eq ← 
_root_.Eq.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
_root_.Eq.faithful_of_comp
#align eq.faithful_of_comp 
Eq.faithful_of_comp: ∀ {C : Type u₁} [inst : Category C] {D : Type u₂} [inst_1 : Category D] {E : Type u₃} [inst_2 : Category E] {F : C ⥤ D}
  {G : D ⥤ E} {H : C ⥤ E} [ℋ : Faithful H], F ⋙ G = H → Faithful F
Eq.faithful_of_comp

variable (
F: ?m.35979
F 
G: ?m.35982
G)
/-- “Divide” a functor by a faithful functor. -/
protected def 
Faithful.div: {C : Type u₁} →
  [inst : Category C] →
    {D : Type u₂} →
      [inst_1 : Category D] →
        {E : Type u₃} →
          [inst_2 : Category E] →
            (F : C ⥤ E) →
              (G : D ⥤ E) →
                [inst_3 : Faithful G] →
                  (obj : C → D) →
                    (∀ (X : C), G.obj (obj X) = F.obj X) →
                      (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
                        (∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) → C ⥤ D
Faithful.div (
F: C ⥤ E
F : 
C: Type u₁
C ⥤ 
E: Type u₃
E) (
G: D ⥤ E
G : 
D: Type u₂
D ⥤ 
E: Type u₃
E) [
Faithful: {C : Type ?u.36077} → [inst : Category C] → {D : Type ?u.36076} → [inst_1 : Category D] → C ⥤ D → Prop
Faithful 
G: D ⥤ E
G] (
obj: C → D
obj : 
C: Type u₁
C → 
D: Type u₂
D)
    (
h_obj: ∀ (X : C), G.obj (obj X) = F.obj X
h_obj : ∀ 
X: ?m.36123
X, 
G: D ⥤ E
G.
obj: {V : Type ?u.36140} → [inst : Quiver V] → {W : Type ?u.36139} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj (
obj: C → D
obj 
X: ?m.36123
X) = 
F: C ⥤ E
F.
obj: {V : Type ?u.36196} → [inst : Quiver V] → {W : Type ?u.36195} → [inst_1 : Quiver W] → V ⥤q W → V → W
obj 
X: ?m.36123
X) (
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map : ∀ {
X: ?m.36226
X 
Y: ?m.36229
Y}, (
X: ?m.36226
X ⟶ 
Y: ?m.36229
Y) → (
obj: C → D
obj 
X: ?m.36226
X ⟶ 
obj: C → D
obj 
Y: ?m.36229
Y))
    (
h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)
h_map : ∀ {
X: ?m.36298
X 
Y: ?m.36301
Y} {
f: X ⟶ Y
f : 
X: ?m.36298
X ⟶ 
Y: ?m.36301
Y}, 
HEq: {α : Sort ?u.36333} → α → {β : Sort ?u.36333} → β → Prop
HEq (
G: D ⥤ E
G.
map: {V : Type ?u.36346} →
  [inst : Quiver V] →
    {W : Type ?u.36345} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map (
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map 
f: X ⟶ Y
f)) (
F: C ⥤ E
F.
map: {V : Type ?u.36440} →
  [inst : Quiver V] →
    {W : Type ?u.36439} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map 
f: X ⟶ Y
f)) : 
C: Type u₁
C ⥤ 
D: Type u₂
D :=
  { obj, map := @
map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map,
    map_id := 
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

{ obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

a
G.map ({ obj := obj, map := map }.map (𝟙 X)) = G.map (𝟙 ({ obj := obj, map := map }.obj X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

a.h
HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

HEq (F.map (𝟙 X)) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

HEq (G.map ({ obj := obj, map := map }.map (𝟙 X))) (F.map (𝟙 X))
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C

HEq (F.map (𝟙 X)) (G.map (𝟙 ({ obj := obj, map := map }.obj X)))
Goals accomplished! 🐙
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

∀ (X : C), { obj := obj, map := map }.map (𝟙 X) = 𝟙 ({ obj := obj, map := map }.obj X)
C: Type u₁

inst✝³: Category C

D: Type u₂

inst✝²: Category D

E: Type u₃

inst✝¹: Category E

F✝, F': C ⥤ D

G✝: D ⥤ E

F: C ⥤ E

G: D ⥤ E

inst✝: Faithful G

obj: C → D

h_obj: ∀ (X : C), G.obj (obj X) = F.obj X

map: {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)

h_map: ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)

X: C