C : Type u₁
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ 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✝¹ : Full G
inst✝ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
⊢ ∀ [inst : Mono g], ∃ h, g ≫ h = f
intro
C : Type u₁
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize 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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits
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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ 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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
⊢ ∃ h, g ≫ h = f
rcases hI.factors (G.map f) (G.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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ 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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ h, g ≫ h = f
use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I) = G.map 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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I = f
refine' Faithful.map_injective (F := G) _
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✝² : Full G
inst✝¹ : Faithful G
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I) = G.map f
simpa