[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.105, u_1} D
⊢ CompleteLattice (MorphismProperty C)
[PROOFSTEP]
dsimp only [MorphismProperty]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.105, u_1} D
⊢ CompleteLattice (⦃X Y : C⦄ → (X ⟶ Y) → Prop)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.6347, u_1} D
X Y : C
f : X ⟶ Y
⊢ ⊤ f
[PROOFSTEP]
simp only [top_eq]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.10321, u_1} D
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : X✝ ≅ Y✝
f : Y✝ ⟶ Z✝
x✝ : isoClosure P f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso iso.hom.left ≪≫ e.symm).hom ≫ (Arrow.mk (e.hom ≫ f)).hom = (Arrow.mk f').hom ≫ (asIso iso.hom.right).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.10321, u_1} D
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : Y✝ ≅ Z✝
f : X✝ ⟶ Y✝
x✝ : isoClosure P f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso iso.hom.left).hom ≫ (Arrow.mk (f ≫ e.hom)).hom = (Arrow.mk f').hom ≫ (asIso iso.hom.right ≪≫ e).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.20276, u_1} D
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g
[PROOFSTEP]
simpa using hP.1 (asIso f).symm (f ≫ g) h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.21442, u_1} D
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f
[PROOFSTEP]
simpa using hP.2 (asIso g).symm (f ≫ g) h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.22704, u_1} D
P : MorphismProperty C
hP : RespectsIso P
f g : Arrow C
e : f ≅ g
⊢ P f.hom ↔ P g.hom
[PROOFSTEP]
rw [← Arrow.inv_left_hom_right e.hom, hP.cancel_left_isIso, hP.cancel_right_isIso]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
⊢ RespectsIso P
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f hf
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P f
⊢ P (e.hom ≫ f)
[PROOFSTEP]
refine' hP (Arrow.mk f) (Arrow.mk (e.hom ≫ f)) (Arrow.isoMk e.symm (Iso.refl _) _) hf
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P f
⊢ e.symm.hom ≫ (Arrow.mk (e.hom ≫ f)).hom = (Arrow.mk f).hom ≫ (Iso.refl (Arrow.mk f).right).hom
[PROOFSTEP]
dsimp
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P f
⊢ e.inv ≫ e.hom ≫ f = f ≫ 𝟙 Z
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, Category.comp_id]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f hf
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e.hom)
[PROOFSTEP]
refine' hP (Arrow.mk f) (Arrow.mk (f ≫ e.hom)) (Arrow.isoMk (Iso.refl _) e _) hf
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P f
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk (f ≫ e.hom)).hom = (Arrow.mk f).hom ≫ e.hom
[PROOFSTEP]
dsimp
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.23989, u_1} D
P : MorphismProperty C
hP : ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P f
⊢ 𝟙 X ≫ f ≫ e.hom = f ≫ e.hom
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.26090, u_1} D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
⊢ P g'
[PROOFSTEP]
let e := sq.flip.isoPullback
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.26090, u_1} D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P g'
[PROOFSTEP]
rw [← hP₁.cancel_left_isIso e.inv, sq.flip.isoPullback_inv_fst]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.26090, u_1} D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P pullback.fst
[PROOFSTEP]
exact hP₂ _ _ _ f g hg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.27180, u_1} D
P : MorphismProperty C
hP : StableUnderBaseChange P
⊢ RespectsIso P
[PROOFSTEP]
apply RespectsIso.of_respects_arrow_iso
[GOAL]
case hP
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.27180, u_1} D
P : MorphismProperty C
hP : StableUnderBaseChange P
⊢ ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
[PROOFSTEP]
intro f g e
[GOAL]
case hP
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.27180, u_1} D
P : MorphismProperty C
hP : StableUnderBaseChange P
f g : Arrow C
e : f ≅ g
⊢ P f.hom → P g.hom
[PROOFSTEP]
exact hP (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w))
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
⊢ P ((baseChange f).map g).left
[PROOFSTEP]
let e := pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (g.w.trans (Category.comp_id _)) rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ P ((baseChange f).map g).left
[PROOFSTEP]
have : e.inv ≫ pullback.snd = ((baseChange f).map g).left := by ext <;> dsimp <;> simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ e.inv ≫ pullback.snd = ((baseChange f).map g).left
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ (e.inv ≫ pullback.snd) ≫ pullback.fst = ((baseChange f).map g).left ≫ pullback.fst
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ (e.inv ≫ pullback.snd) ≫ pullback.snd = ((baseChange f).map g).left ≫ pullback.snd
[PROOFSTEP]
dsimp
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ (((pullback.congrHom (_ : g.left ≫ Y.hom = X.hom) (_ : f = f)).inv ≫
          (pullbackRightPullbackFstIso Y.hom f g.left).inv) ≫
        pullback.snd) ≫
      pullback.fst =
    pullback.map X.hom f Y.hom f g.left (𝟙 S') (𝟙 S) (_ : X.hom ≫ 𝟙 S = g.left ≫ Y.hom) (_ : f ≫ 𝟙 S = 𝟙 S' ≫ f) ≫
      pullback.fst
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ (((pullback.congrHom (_ : g.left ≫ Y.hom = X.hom) (_ : f = f)).inv ≫
          (pullbackRightPullbackFstIso Y.hom f g.left).inv) ≫
        pullback.snd) ≫
      pullback.snd =
    pullback.map X.hom f Y.hom f g.left (𝟙 S') (𝟙 S) (_ : X.hom ≫ 𝟙 S = g.left ≫ Y.hom) (_ : f ≫ 𝟙 S = 𝟙 S' ≫ f) ≫
      pullback.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P ((baseChange f).map g).left
[PROOFSTEP]
rw [← this, hP.respectsIso.cancel_left_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.30641, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P pullback.snd
[PROOFSTEP]
exact hP.snd _ _ H
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g'))
[PROOFSTEP]
have :
  pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁) ((Category.comp_id _).trans e₂) =
    ((pullbackSymmetry _ _).hom ≫ ((baseChange _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
      (pullbackSymmetry _ _).hom ≫ ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left :=
  by ext <;> dsimp <;> simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') ≫ pullback.fst =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left) ≫
      pullback.fst
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') ≫ pullback.snd =
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
          ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
        (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left) ≫
      pullback.snd
[PROOFSTEP]
dsimp
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') ≫ pullback.fst =
    (((pullbackSymmetry f g).hom ≫
          pullback.map g f g' f i₂ (𝟙 X) (𝟙 S) (_ : (Over.mk g).hom ≫ 𝟙 S = (Over.homMk i₂).left ≫ (Over.mk g').hom)
            (_ : f ≫ 𝟙 S = 𝟙 X ≫ f)) ≫
        (pullbackSymmetry g' f).hom ≫
          pullback.map f g' f' g' i₁ (𝟙 Y') (𝟙 S) (_ : (Over.mk f).hom ≫ 𝟙 S = (Over.homMk i₁).left ≫ (Over.mk f').hom)
            (_ : g' ≫ 𝟙 S = 𝟙 Y' ≫ g')) ≫
      pullback.fst
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
⊢ pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') ≫ pullback.snd =
    (((pullbackSymmetry f g).hom ≫
          pullback.map g f g' f i₂ (𝟙 X) (𝟙 S) (_ : (Over.mk g).hom ≫ 𝟙 S = (Over.homMk i₂).left ≫ (Over.mk g').hom)
            (_ : f ≫ 𝟙 S = 𝟙 X ≫ f)) ≫
        (pullbackSymmetry g' f).hom ≫
          pullback.map f g' f' g' i₁ (𝟙 Y') (𝟙 S) (_ : (Over.mk f).hom ≫ 𝟙 S = (Over.homMk i₁).left ≫ (Over.mk f').hom)
            (_ : g' ≫ 𝟙 S = 𝟙 Y' ≫ g')) ≫
      pullback.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P (pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g'))
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P
    (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫
        ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left)
[PROOFSTEP]
apply hP'
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left)
[PROOFSTEP]
rw [hP.respectsIso.cancel_left_isIso]
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left)
[PROOFSTEP]
rw [hP.respectsIso.cancel_left_isIso]
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.39138, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : StableUnderComposition P
S X X' Y Y' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this :
  pullback.map f g f' g' i₁ i₂ (𝟙 S) (_ : f ≫ 𝟙 S = i₁ ≫ f') (_ : g ≫ 𝟙 S = i₂ ≫ g') =
    ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((baseChange (Over.mk f).hom).map (Over.homMk i₂)).left) ≫
      (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((baseChange g').map (Over.homMk i₁)).left
⊢ P ((baseChange g').map (Over.homMk i₁)).left
[PROOFSTEP]
exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
  hP.baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.47372, u_1} D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'
[PROOFSTEP]
let e := sq.flip.isoPushout
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.47372, u_1} D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P f'
[PROOFSTEP]
rw [← hP₁.cancel_right_isIso _ e.hom, sq.flip.inr_isoPushout_hom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.47372, u_1} D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P pushout.inr
[PROOFSTEP]
exact hP₂ _ _ _ f g hf
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{?u.53343, u_1} D
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝² : Category.{u_5, u_2} C₁
inst✝¹ : Category.{u_6, u_3} C₂
inst✝ : Category.{u_7, u_4} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso ((F ⋙ G).map f)
[PROOFSTEP]
haveI := hF f hf
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{?u.53343, u_1} D
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝² : Category.{u_5, u_2} C₁
inst✝¹ : Category.{u_6, u_3} C₂
inst✝ : Category.{u_7, u_4} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{?u.53343, u_1} D
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝² : Category.{u_5, u_2} C₁
inst✝¹ : Category.{u_6, u_3} C₂
inst✝ : Category.{u_7, u_4} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : IsInvertedBy W F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ D
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
⊢ IsIso (L.op.map f)
[PROOFSTEP]
haveI := h f.unop hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ D
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
this : IsIso (L.map f.unop)
⊢ IsIso (L.op.map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ D
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.rightOp.map f)
[PROOFSTEP]
haveI := h f.op hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.rightOp.map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
⊢ IsIso (L.leftOp.map f)
[PROOFSTEP]
haveI := h f.unop hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
this : IsIso (L.map f.unop)
⊢ IsIso (L.leftOp.map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : C ⥤ Dᵒᵖ
h : IsInvertedBy W L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.op W f
this : IsIso (L.map f.unop)
⊢ IsIso (L.map f.unop).unop
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso ((Functor.unop L).map f)
[PROOFSTEP]
haveI := h f.op hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso ((Functor.unop L).map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : IsInvertedBy (MorphismProperty.op W) L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).unop
[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
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : naturalityProperty app f
hg : naturalityProperty app g
⊢ naturalityProperty app (f ≫ g)
[PROOFSTEP]
simp only [naturalityProperty] at hf hg ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
⊢ F₁.map (f ≫ g) ≫ app Z = app X ≫ F₂.map (f ≫ g)
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc, hg]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
⊢ F₁.map f ≫ app Y ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
[PROOFSTEP]
slice_lhs 1 2 => rw [hf]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₁.map f ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₂.map g
[PROOFSTEP]
rw [hf]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₁.map f ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₂.map g
[PROOFSTEP]
rw [hf]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₁.map f ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
| F₂.map g
[PROOFSTEP]
rw [hf]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : F₁.map f ≫ app Y = app X ≫ F₂.map f
hg : F₁.map g ≫ app Z = app Y ≫ F₂.map g
⊢ (app X ≫ F₂.map f) ≫ F₂.map g = app X ≫ F₂.map f ≫ F₂.map g
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : naturalityProperty app e.hom
⊢ naturalityProperty app e.inv
[PROOFSTEP]
simp only [naturalityProperty] at he ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv
[PROOFSTEP]
rw [← cancel_epi (F₁.map e.hom)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
[PROOFSTEP]
slice_rhs 1 2 => rw [he]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₁.map e.hom ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₂.map e.inv
[PROOFSTEP]
rw [he]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₁.map e.hom ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₂.map e.inv
[PROOFSTEP]
rw [he]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₁.map e.hom ≫ app Y
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
| F₂.map e.inv
[PROOFSTEP]
rw [he]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv
[PROOFSTEP]
simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id, Category.id_comp,
  Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ RespectsIso (MorphismProperty.inverseImage P F)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (e.hom ≫ f)
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (f ≫ e.hom)
[PROOFSTEP]
all_goals
  intro X Y Z e f hf
  dsimp [MorphismProperty.inverseImage]
  rw [F.map_comp]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f hf
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
⊢ MorphismProperty.inverseImage P F (e.hom ≫ f)
[PROOFSTEP]
dsimp [MorphismProperty.inverseImage]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map (e.hom ≫ f))
[PROOFSTEP]
rw [F.map_comp]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.inverseImage P F f → MorphismProperty.inverseImage P F (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f hf
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ MorphismProperty.inverseImage P F (f ≫ e.hom)
[PROOFSTEP]
dsimp [MorphismProperty.inverseImage]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map (f ≫ e.hom))
[PROOFSTEP]
rw [F.map_comp]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map e.hom ≫ F.map f)
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : RespectsIso P
F : C ⥤ D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : MorphismProperty.inverseImage P F f
⊢ P (F.map f ≫ F.map e.hom)
[PROOFSTEP]
exacts [h.1 (F.mapIso e) (F.map f) hf, h.2 (F.mapIso e) (F.map f) hf]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
h : StableUnderComposition P
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.inverseImage P F f
hg : MorphismProperty.inverseImage P F g
⊢ MorphismProperty.inverseImage P F (f ≫ g)
[PROOFSTEP]
simpa only [← F.map_comp] using h (F.map f) (F.map g) hf hg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.65654, u_1} D
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.65803, u_1} D
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.65952, u_1} D
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
⊢ RespectsIso (MorphismProperty.monomorphisms C)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
[PROOFSTEP]
simp only [monomorphisms.iff]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ Mono f → Mono (e.hom ≫ f)
[PROOFSTEP]
intro
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
a✝ : Mono f
⊢ Mono (e.hom ≫ f)
[PROOFSTEP]
apply mono_comp
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
[PROOFSTEP]
simp only [monomorphisms.iff]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Mono f → Mono (f ≫ e.hom)
[PROOFSTEP]
intro
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.66779, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : Mono f
⊢ Mono (f ≫ e.hom)
[PROOFSTEP]
apply mono_comp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
⊢ RespectsIso (MorphismProperty.epimorphisms C)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
[PROOFSTEP]
simp only [epimorphisms.iff]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ Epi f → Epi (e.hom ≫ f)
[PROOFSTEP]
intro
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
a✝ : Epi f
⊢ Epi (e.hom ≫ f)
[PROOFSTEP]
apply epi_comp
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
[PROOFSTEP]
simp only [epimorphisms.iff]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Epi f → Epi (f ≫ e.hom)
[PROOFSTEP]
intro
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.67468, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : Epi f
⊢ Epi (f ≫ e.hom)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
⊢ RespectsIso (MorphismProperty.isomorphisms C)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
[PROOFSTEP]
simp only [isomorphisms.iff]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ IsIso f → IsIso (e.hom ≫ f)
[PROOFSTEP]
intro
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
a✝ : IsIso f
⊢ IsIso (e.hom ≫ f)
[PROOFSTEP]
infer_instance
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
[PROOFSTEP]
simp only [isomorphisms.iff]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ IsIso f → IsIso (f ≫ e.hom)
[PROOFSTEP]
intro
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68149, u_1} D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : IsIso f
⊢ IsIso (f ≫ e.hom)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68670, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.isomorphisms C f
hg : MorphismProperty.isomorphisms C g
⊢ MorphismProperty.isomorphisms C (f ≫ g)
[PROOFSTEP]
rw [isomorphisms.iff] at hf hg ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68670, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
⊢ IsIso (f ≫ g)
[PROOFSTEP]
haveI := hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68670, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this : IsIso f
⊢ IsIso (f ≫ g)
[PROOFSTEP]
haveI := hg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.68670, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsIso f
hg : IsIso g
this✝ : IsIso f
this : IsIso g
⊢ IsIso (f ≫ g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.69618, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.monomorphisms C f
hg : MorphismProperty.monomorphisms C g
⊢ MorphismProperty.monomorphisms C (f ≫ g)
[PROOFSTEP]
rw [monomorphisms.iff] at hf hg ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.69618, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Mono f
hg : Mono g
⊢ Mono (f ≫ g)
[PROOFSTEP]
haveI := hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.69618, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Mono f
hg : Mono g
this : Mono f
⊢ Mono (f ≫ g)
[PROOFSTEP]
haveI := hg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.69618, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Mono f
hg : Mono g
this✝ : Mono f
this : Mono g
⊢ Mono (f ≫ g)
[PROOFSTEP]
apply mono_comp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.70586, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.epimorphisms C f
hg : MorphismProperty.epimorphisms C g
⊢ MorphismProperty.epimorphisms C (f ≫ g)
[PROOFSTEP]
rw [epimorphisms.iff] at hf hg ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.70586, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
[PROOFSTEP]
haveI := hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.70586, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this : Epi f
⊢ Epi (f ≫ g)
[PROOFSTEP]
haveI := hg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.70586, u_1} D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this✝ : Epi f
this : Epi g
⊢ Epi (f ≫ g)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : FunctorsInverting W D
h : F₁.obj = F₂.obj
⊢ F₁ = F₂
[PROOFSTEP]
cases F₁
[GOAL]
case mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₂ : FunctorsInverting W D
obj✝ : C ⥤ D
property✝ : IsInvertedBy W obj✝
h : { obj := obj✝, property := property✝ }.obj = F₂.obj
⊢ { obj := obj✝, property := property✝ } = F₂
[PROOFSTEP]
cases F₂
[GOAL]
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
obj✝¹ : C ⥤ D
property✝¹ : IsInvertedBy W obj✝¹
obj✝ : C ⥤ D
property✝ : IsInvertedBy W obj✝
h : { obj := obj✝¹, property := property✝¹ }.obj = { obj := obj✝, property := property✝ }.obj
⊢ { obj := obj✝¹, property := property✝¹ } = { obj := obj✝, property := property✝ }
[PROOFSTEP]
subst h
[GOAL]
case mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
obj✝ : C ⥤ D
property✝¹ : IsInvertedBy W obj✝
property✝ : IsInvertedBy W { obj := obj✝, property := property✝¹ }.obj
⊢ { obj := obj✝, property := property✝¹ } =
    { obj := { obj := obj✝, property := property✝¹ }.obj, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ IsInvertedBy W F₁ ↔ IsInvertedBy W F₂
[PROOFSTEP]
suffices ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
  by
  constructor
  exact fun h X Y f hf => by
    rw [← this]
    exact h f hf
  exact fun h X Y f hf => by
    rw [this]
    exact h f hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₁ ↔ IsInvertedBy W F₂
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₁ → IsInvertedBy W F₂
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
[PROOFSTEP]
exact fun h X Y f hf => by
  rw [← this]
  exact h f hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₁
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₂.map f)
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₁
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₁.map f)
[PROOFSTEP]
exact h f hf
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
⊢ IsInvertedBy W F₂ → IsInvertedBy W F₁
[PROOFSTEP]
exact fun h X Y f hf => by
  rw [this]
  exact h f hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₂
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₁.map f)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
this : ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
h : IsInvertedBy W F₂
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (F₂.map f)
[PROOFSTEP]
exact h f hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ ∀ (X Y : C) (f : X ⟶ Y), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
[PROOFSTEP]
exact (RespectsIso.isomorphisms D).arrow_mk_iso_iff (Arrow.isoMk (e.app X) (e.app Y) (by simp))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ (e.app X).hom ≫ (Arrow.mk (F₂.map f)).hom = (Arrow.mk (F₁.map f)).hom ≫ (e.app Y).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ RespectsIso (MorphismProperty.diagonal P)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.diagonal P f → MorphismProperty.diagonal P (e.hom ≫ f)
[PROOFSTEP]
introv H
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (e.hom ≫ f)
[PROOFSTEP]
rwa [diagonal_iff, pullback.diagonal_comp, hP.cancel_left_isIso, hP.cancel_left_isIso, ←
  hP.cancel_right_isIso _ (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)), ←
  pullback.condition, hP.cancel_left_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : MorphismProperty.diagonal P f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.diagonal P f → MorphismProperty.diagonal P (f ≫ e.hom)
[PROOFSTEP]
introv H
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ MorphismProperty.diagonal P (f ≫ e.hom)
[PROOFSTEP]
delta diagonal
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.75953, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : MorphismProperty.diagonal P f
⊢ P (pullback.diagonal (f ≫ e.hom))
[PROOFSTEP]
rwa [pullback.diagonal_comp, hP.cancel_right_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.83850, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
hP' : RespectsIso P
hP'' : StableUnderBaseChange P
⊢ StableUnderComposition (MorphismProperty.diagonal P)
[PROOFSTEP]
introv X h₁ h₂
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.83850, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
hP' : RespectsIso P
hP'' : StableUnderBaseChange P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ : MorphismProperty.diagonal P f
h₂ : MorphismProperty.diagonal P g
⊢ MorphismProperty.diagonal P (f ≫ g)
[PROOFSTEP]
rw [diagonal_iff, pullback.diagonal_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.83850, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
hP' : RespectsIso P
hP'' : StableUnderBaseChange P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ : MorphismProperty.diagonal P f
h₂ : MorphismProperty.diagonal P g
⊢ P (pullback.diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ pullback.snd)
[PROOFSTEP]
exact hP _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.83850, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
hP' : RespectsIso P
hP'' : StableUnderBaseChange P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ : MorphismProperty.diagonal P f
h₂ : MorphismProperty.diagonal P g
⊢ P ((pullbackDiagonalMapIdIso f f g).inv ≫ pullback.snd)
[PROOFSTEP]
simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.86028, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
⊢ ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), MorphismProperty.diagonal P g → MorphismProperty.diagonal P pullback.fst
[PROOFSTEP]
introv h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.86028, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ MorphismProperty.diagonal P pullback.fst
[PROOFSTEP]
rw [diagonal_iff, diagonal_pullback_fst, hP'.cancel_left_isIso, hP'.cancel_right_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.86028, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ P ((baseChange f).map (Over.homMk (pullback.diagonal g))).left
[PROOFSTEP]
exact hP.baseChange_map f _ (by simpa)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.86028, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ P (Over.homMk (pullback.diagonal g)).left
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
⊢ RespectsIso (universally P)
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), universally P f → universally P (e.hom ≫ f)
[PROOFSTEP]
intro X Y Z e f hf X' Z' i₁ i₂ f' H
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ P f'
[PROOFSTEP]
have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
  IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
[PROOFSTEP]
rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ P f'
[PROOFSTEP]
exact hf _ _ _ (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ IsPullback f' ?m.90182 ?m.90183 f
[PROOFSTEP]
simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), universally P f → universally P (f ≫ e.hom)
[PROOFSTEP]
intro X Y Z e f hf X' Z' i₁ i₂ f' H
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
⊢ P f'
[PROOFSTEP]
have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv := IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ P f'
[PROOFSTEP]
exact
  hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id, Category.comp_id, Category.comp_id] using H.paste_horiz this)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.88038, u_1} D
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : universally P f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ IsPullback f' ?m.91717 ?m.91718 f
[PROOFSTEP]
simpa only [Category.assoc, Iso.hom_inv_id, Category.comp_id, Category.comp_id] using H.paste_horiz this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.92183, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
⊢ StableUnderComposition (MorphismProperty.universally P)
[PROOFSTEP]
intro X Y Z f g hf hg X' Z' i₁ i₂ f' H
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.92183, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
⊢ P f'
[PROOFSTEP]
have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.92183, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P f'
[PROOFSTEP]
rw [← this] at H ⊢
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.92183, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst)
[PROOFSTEP]
apply hP _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.92183, u_1} D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g))
[PROOFSTEP]
exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.93105, u_1} D
P : MorphismProperty C
⊢ universally P ≤ P
[PROOFSTEP]
intro X Y f hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.93105, u_1} D
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : universally P f
⊢ P f
[PROOFSTEP]
exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.93105, u_1} D
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : universally P f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
[PROOFSTEP]
rw [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.95780, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ MorphismProperty.injective C (f ≫ g)
[PROOFSTEP]
delta MorphismProperty.injective
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.95780, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective ↑(f ≫ g)
[PROOFSTEP]
rw [coe_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.95780, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective (↑g ∘ ↑f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96246, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ MorphismProperty.surjective C (f ≫ g)
[PROOFSTEP]
delta MorphismProperty.surjective
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96246, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective ↑(f ≫ g)
[PROOFSTEP]
rw [coe_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96246, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective (↑g ∘ ↑f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96710, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ MorphismProperty.bijective C (f ≫ g)
[PROOFSTEP]
delta MorphismProperty.bijective
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96710, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective ↑(f ≫ g)
[PROOFSTEP]
rw [coe_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{?u.96710, u_1} D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective (↑g ∘ ↑f)
[PROOFSTEP]
exact hg.comp hf