C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f
C : Type u₁
inst✝² : Category C
D : Type u_2
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
⊢ ∀ [inst : Mono g], ∃ h, g ≫ h = f
intro
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ ∃ h, g ≫ h = f
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f
rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w,h⟩
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ g ≫ adj.unit.app Y ≫ G.map w = f
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ ∃ h, g ≫ h = f
use adj.unit.app Y ≫ G.map w
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ g ≫ adj.unit.app Y ≫ G.map w = f
rw [← unit_naturality_assoc, ← G.map_comp, h]
no goals
case intro
C : Type u₁
inst✝³ : Category C
D : Type u_2
inst✝² : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Functor.PreservesMonomorphisms F
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f
simp