C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this : WellPowered C
⊢ ∃ G, Injective G ∧ IsCoseparator G
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
⊢ ∃ G, Injective G ∧ IsCoseparator G
haveI : WellPowered C := wellPowered_of_isDetector G hG.isDetector
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
⊢ ∃ G, Injective G ∧ IsCoseparator G
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this : WellPowered C
⊢ ∃ G, Injective G ∧ IsCoseparator G
haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small _ _
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ ∃ G, Injective G ∧ IsCoseparator G
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
⊢ ∃ G, Injective G ∧ IsCoseparator G
let T : C := Injective.under (piObj fun P : Subobject (op G) => unop P)
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ ∃ G, Injective G ∧ IsCoseparator G
refine' ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => _⟩
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ h ≫ f = 0
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0
refine' (Preadditive.isSeparator_iff _).1 hG _ fun h => _
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : factorThruImage (h ≫ f) = 0
⊢ h ≫ f = 0

case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ factorThruImage (h ≫ f) = 0
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ h ≫ f = 0
suffices hh : factorThruImage (h ≫ f) = 0
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
⊢ factorThruImage (h ≫ f) = 0
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ factorThruImage (h ≫ f) = 0
let R := Subobject.mk (factorThruImage (h ≫ f)).op
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
⊢ factorThruImage (h ≫ f) = 0
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
⊢ factorThruImage (h ≫ f) = 0
let q₁ : image (h ≫ f) ⟶ unop R :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
⊢ factorThruImage (h ≫ f) = 0
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
⊢ factorThruImage (h ≫ f) = 0
let q₂ : unop (R : Cᵒᵖ) ⟶ piObj fun P : Subobject (op G) => unop P :=
  section_ (Pi.π (fun P : Subobject (op G) => (unop P : C)) R)
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ factorThruImage (h ≫ f) = 0
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
⊢ factorThruImage (h ≫ f) = 0
let q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι _
no goals
case hh
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ factorThruImage (h ≫ f) = 0
exact zero_of_comp_mono q
  (by rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
    Category.assoc, hf, comp_zero])
no goals
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : factorThruImage (h ≫ f) = 0
⊢ h ≫ f = 0
rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
no goals
C : Type u
inst✝³ : Category C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered C
this : HasProductsOfShape (Subobject G.op) C
T : C := Injective.under (∏ fun P => (Subobject.underlying.obj P).unop)
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject G.op := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ (Subobject.underlying.obj R).unop :=
  (Iso.unop (Subobject.underlyingIso (factorThruImage (h ≫ f)).op)).hom
q₂ : (Subobject.underlying.obj R).unop ⟶ ∏ fun P => (Subobject.underlying.obj P).unop :=
  section_ (Pi.π (fun P => (Subobject.underlying.obj P).unop) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ fun P => (Subobject.underlying.obj P).unop)
⊢ factorThruImage (h ≫ f) ≫ q = 0
rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
Category.assoc, hf, comp_zero]