C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category 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)
C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
hP' : RespectsIso P
hP'' : StableUnderBaseChange P
⊢ StableUnderComposition (MorphismProperty.diagonal P)
introv X h₁ h₂
C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category 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)
C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category 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)
rw [diagonal_iff, pullback.diagonal_comp]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category 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)
exact hP _ _ h₁ (by simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂)
no goals
C : Type u
inst✝² : Category C
D : Type ?u.77182
inst✝¹ : Category 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)
simpa [hP'.cancel_left_isIso] using hP''.snd _ _ h₂