[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro X p hp
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case mp.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
exact
  ⟨Nonempty.intro
      { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
        isLimit := by
          apply Fork.IsLimit.mk'
          intro s
          refine' ⟨s.ι ≫ e, _⟩
          constructor
          · erw [assoc, h₂, ← Limits.Fork.condition s, comp_id]
          · intro m hm
            rw [Fork.ι_ofι] at hm 
            rw [← hm]
            simp only [← hm, assoc, h₁]
            exact (comp_id m).symm }⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X = i ≫ p
[PROOFSTEP]
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ IsLimit (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p))
[PROOFSTEP]
apply Fork.IsLimit.mk'
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (s : Fork (𝟙 X) p) →
    { l //
      l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
                WalkingParallelPair.zero},
          m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l //
    l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
[PROOFSTEP]
refine' ⟨s.ι ≫ e, _⟩
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
          ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
      m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
[PROOFSTEP]
constructor
[GOAL]
case create.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
[PROOFSTEP]
erw [assoc, h₂, ← Limits.Fork.condition s, comp_id]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
[PROOFSTEP]
intro m hm
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
⊢ m = Fork.ι s ≫ e
[PROOFSTEP]
rw [Fork.ι_ofι] at hm 
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = Fork.ι s ≫ e
[PROOFSTEP]
rw [← hm]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = (m ≫ i) ≫ e
[PROOFSTEP]
simp only [← hm, assoc, h₁]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = m ≫ 𝟙 Y
[PROOFSTEP]
exact (comp_id m).symm
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X p hp
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
haveI : HasEqualizer (𝟙 X) p := h X p hp
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
refine'
  ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p, equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), _,
    equalizer.lift_ι _ _⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ p ≫ 𝟙 X = p ≫ p
[PROOFSTEP]
rw [hp, comp_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p) = 𝟙 (equalizer (𝟙 X) p)
[PROOFSTEP]
ext
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p)) ≫ equalizer.ι (𝟙 X) p =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
[PROOFSTEP]
simp only [assoc, limit.lift_π, Eq.ndrec, id_eq, eq_mpr_eq_cast, Fork.ofι_pt, Fork.ofι_π_app, id_comp]
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p
[PROOFSTEP]
rw [← equalizer.condition, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ (𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p
[PROOFSTEP]
simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
intro h X p hp
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasKernel p
[PROOFSTEP]
haveI : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ HasKernel p
[PROOFSTEP]
convert hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
[GOAL]
case h.e'_6
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ p = 𝟙 X - (𝟙 X - p)
[PROOFSTEP]
rw [sub_sub_cancel]
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro h X p hp
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
haveI : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasKernel (𝟙 X - p)
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
apply Preadditive.hasEqualizer_of_hasKernel
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
⊢ IsIdempotentComplete D
[PROOFSTEP]
rw [isIdempotentComplete_iff_idempotents_have_kernels]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
X✝ : D
p✝ : X✝ ⟶ X✝
a✝ : p✝ ≫ p✝ = p✝
⊢ HasKernel p✝
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
h : ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
use Y, i ≫ φ.hom, φ.inv ≫ e
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y
[PROOFSTEP]
slice_lhs 2 3 => rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X ≫ e = 𝟙 Y
[PROOFSTEP]
rw [id_comp, h₁]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
[PROOFSTEP]
slice_lhs 2 3 => rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ φ.inv ≫ p ≫ φ.hom = p'
[PROOFSTEP]
rw [hpp', ← assoc, φ.inv_hom_id, id_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
exact split_imp_of_iso φ p p' hpp'
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
apply split_imp_of_iso φ.symm p' p
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
[PROOFSTEP]
rw [← comp_id p, ← φ.hom_inv_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
[PROOFSTEP]
slice_rhs 2 3 => rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
[PROOFSTEP]
slice_rhs 1 2 => erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = (𝟙 X' ≫ p') ≫ φ.inv
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = p' ≫ φ.inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ IsIdempotentComplete D
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X' p hp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
let φ := ε.counitIso.symm.app X'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
erw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
    (by
      slice_rhs 1 2 => rw [φ.hom_inv_id]
      rw [id_comp])]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
slice_rhs 1 2 => rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 ((𝟭 D).obj X') ≫ p) ≫ φ.hom
[PROOFSTEP]
rw [id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
    (by rw [← ε.inverse.map_comp, hp]) with
  ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p
[PROOFSTEP]
rw [← ε.inverse.map_comp, hp]
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
[PROOFSTEP]
rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
[GOAL]
case h.right
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
[GOAL]
case h.right
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ NatTrans.app (Equivalence.counit ε) X' ≫ p ≫ NatTrans.app (Equivalence.counitInv ε) X' =
    (ε.counitIso.symm.app X').inv ≫ p ≫ (ε.counitIso.symm.app X').hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D
[PROOFSTEP]
exact Equivalence.isIdempotentComplete ε
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
[PROOFSTEP]
exact Equivalence.isIdempotentComplete ε.symm
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ IsIdempotentComplete C
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X p hp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op
[PROOFSTEP]
rw [← op_comp, hp]
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
use Y.unop, e.unop, i.unop
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop ∧ i.unop ≫ e.unop = p
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop
[PROOFSTEP]
simp only [← unop_comp, h₁]
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ (𝟙 Y).unop = 𝟙 Y.unop
[PROOFSTEP]
rfl
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
[PROOFSTEP]
simp only [← unop_comp, h₂]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ p.op.unop = p
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C
[PROOFSTEP]
exact isIdempotentComplete_of_isIdempotentComplete_opposite
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
apply isIdempotentComplete_of_isIdempotentComplete_opposite
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ
[PROOFSTEP]
rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C
[PROOFSTEP]
exact h
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.32276, u_1} C
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
rwa [isIdempotentComplete_iff_opposite]
