[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X✝ Y✝ : C
g : X✝ ⟶ 0
f : X✝ ⟶ Y✝
inst✝ : Mono f
⊢ f ≫ 0 = g
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨h ≫ i.hom, _⟩
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g
[PROOFSTEP]
rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
z : Y✝
⊢ X
[PROOFSTEP]
classical exact if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
z : Y✝
⊢ X
[PROOFSTEP]
exact if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) = g
[PROOFSTEP]
ext y
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) y = g y
[PROOFSTEP]
classical
change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
split_ifs <;> rename_i h
· rw [mono_iff_injective] at mono 
  erw [mono (Classical.choose_spec h)]
· exact False.elim (h ⟨y, rfl⟩)
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (f ≫ fun z => if h : z ∈ Set.range f then g (Classical.choose h) else Nonempty.some (_ : Nonempty X)) y = g y
[PROOFSTEP]
change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (if h : f y ∈ Set.range f then g (Classical.choose h) else (fun h => Nonempty.some (_ : Nonempty X)) h) = g y
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h✝ : f y ∈ Set.range f
⊢ g (Classical.choose h✝) = g y
[PROOFSTEP]
rename_i h
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h✝ : ¬f y ∈ Set.range f
⊢ (fun h => Nonempty.some (_ : Nonempty X)) h✝ = g y
[PROOFSTEP]
rename_i h
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : f y ∈ Set.range f
⊢ g (Classical.choose h) = g y
[PROOFSTEP]
rw [mono_iff_injective] at mono 
[GOAL]
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Function.Injective f
y : X✝
h : f y ∈ Set.range f
⊢ g (Classical.choose h) = g y
[PROOFSTEP]
erw [mono (Classical.choose_spec h)]
[GOAL]
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : ¬f y ∈ Set.range f
⊢ (fun h => Nonempty.some (_ : Nonempty X)) h = g y
[PROOFSTEP]
exact False.elim (h ⟨y, rfl⟩)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Mono some
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Function.Injective some
[PROOFSTEP]
exact Option.some_injective X
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g
[PROOFSTEP]
simp only [prod.comp_lift, comp_factorThru]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.fst = g ≫ prod.fst
[PROOFSTEP]
simp only [prod.lift_fst]
[GOAL]
case h.h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.snd = g ≫ prod.snd
[PROOFSTEP]
simp only [prod.lift_snd]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, _⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ Pi.lift fun b => factorThru (g ≫ Pi.π c b) f) = g
[PROOFSTEP]
ext b
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ c
f : X✝ ⟶ Y✝
mono : Mono f
b : β
⊢ (f ≫ Pi.lift fun b => factorThru (g ≫ Pi.π c b) f) ≫ Pi.π c b = g ≫ Pi.π c b
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app, comp_factorThru]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), _⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f) = g
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.fst = g ≫ biprod.fst
[PROOFSTEP]
simp only [Category.assoc, biprod.lift_fst, comp_factorThru]
[GOAL]
case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.snd = g ≫ biprod.snd
[PROOFSTEP]
simp only [Category.assoc, biprod.lift_snd, comp_factorThru]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
skip
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, _⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biproduct.lift fun b => factorThru (g ≫ biproduct.π c b) f) = g
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
j✝ : β
⊢ (f ≫ biproduct.lift fun b => factorThru (g ≫ biproduct.π c b) f) ≫ biproduct.π c j✝ = g ≫ biproduct.π c j✝
[PROOFSTEP]
simp only [Category.assoc, biproduct.lift_π, comp_factorThru]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ
inst✝ : Projective P
X✝ Y✝ : C
g : X✝ ⟶ P.unop
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.op f.op).unop).op = g.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Cᵒᵖ
inst✝ : Injective J
E✝ X✝ : C
f : J.unop ⟶ X✝
e : E✝ ⟶ X✝
he : Epi e
⊢ ((factorThru f.op e.op).unop ≫ e).op = f.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : C
inst✝ : Injective J
E✝ X✝ : Cᵒᵖ
f : op J ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ ((factorThru f.unop e.unop).op ≫ e).unop = f.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : C
inst✝ : Projective P
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ op P
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.unop f.unop).op).unop = g.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Injective J ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Functor.PreservesEpimorphisms (coyoneda.obj (op (op J))) ↔ Functor.PreservesEpimorphisms (yoneda.obj J)
[PROOFSTEP]
exact Functor.preservesEpimorphisms.iso_iff (Coyoneda.objOpOp _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝¹ : PreservesMonomorphisms L
adj : L ⊣ R
J : D
inst✝ : Injective J
A x✝ : C
g : A ⟶ R.obj J
f : A ⟶ x✝
im : Mono f
⊢ ↑(Adjunction.homEquiv adj A J).symm
      (f ≫ ↑(Adjunction.homEquiv adj x✝ J) (factorThru (↑(Adjunction.homEquiv adj A J).symm g) (L.map f))) =
    ↑(Adjunction.homEquiv adj A J).symm g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasImages Cᵒᵖ
inst✝¹ : HasEqualizers Cᵒᵖ
J Q R S : C
inst✝ : Injective J
h : R ⟶ J
f : Q ⟶ R
g : R ⟶ S
hgf : Exact g.op f.op
w : f ≫ h = 0
⊢ g ≫ desc h f g hgf w = h
[PROOFSTEP]
convert congr_arg Quiver.Hom.unop (Exact.lift_comp h.op g.op f.op hgf (congrArg Quiver.Hom.op w))
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} 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
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w, h⟩
[GOAL]
case intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} 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 ≫ NatTrans.app adj.counit I
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
use adj.unit.app Y ≫ G.map w
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} 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 ≫ NatTrans.app adj.counit I
⊢ g ≫ NatTrans.app adj.unit Y ≫ G.map w = f
[PROOFSTEP]
rw [← unit_naturality_assoc, ← G.map_comp, h]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} 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 ≫ NatTrans.app adj.counit I
⊢ NatTrans.app adj.unit X ≫ G.map (F.map f ≫ NatTrans.app adj.counit I) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{u_2, u_1} 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
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} 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
[PROOFSTEP]
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} 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.{0, 0, u_2, v₁, u_1, u₁} G
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
rcases hI.factors (G.map f) (G.map g) with ⟨w, h⟩
[GOAL]
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} 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.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ h, g ≫ h = f
[PROOFSTEP]
use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} 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.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ g ≫ inv (NatTrans.app adj.counit Y) ≫ F.map w ≫ NatTrans.app adj.counit I = f
[PROOFSTEP]
refine' Faithful.map_injective (F := G) _
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{u_2, u_1} 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.{0, 0, u_2, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (NatTrans.app adj.counit Y) ≫ F.map w ≫ NatTrans.app adj.counit I) = G.map f
[PROOFSTEP]
simpa
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{?u.56282, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
X : D
I : InjectivePresentation X
⊢ Mono (G.map I.f)
[PROOFSTEP]
haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{?u.56282, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesMonomorphisms F
X : D
I : InjectivePresentation X
this : PreservesLimitsOfSize.{0, 0, ?u.56282, v₁, u_1, u₁} G
⊢ Mono (G.map I.f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C ↔ EnoughInjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives D → EnoughInjectives C
[PROOFSTEP]
all_goals intro H; constructor; intro X; constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D
[PROOFSTEP]
intro H
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
⊢ EnoughInjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
⊢ ∀ (X : D), Nonempty (InjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mp.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
X : D
⊢ Nonempty (InjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
⊢ EnoughInjectives D → EnoughInjectives C
[PROOFSTEP]
intro H
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
⊢ EnoughInjectives C
[PROOFSTEP]
constructor
[GOAL]
case mpr.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
⊢ ∀ (X : C), Nonempty (InjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mpr.presentation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
X : C
⊢ Nonempty (InjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation.val
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives C
X : D
⊢ InjectivePresentation X
[PROOFSTEP]
exact F.symm.injectivePresentationOfMapInjectivePresentation _ (Nonempty.some (H.presentation (F.inverse.obj X)))
[GOAL]
case mpr.presentation.val
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F✝ F : C ≌ D
H : EnoughInjectives D
X : C
⊢ InjectivePresentation X
[PROOFSTEP]
exact F.injectivePresentationOfMapInjectivePresentation X (Nonempty.some (H.presentation (F.functor.obj X)))
