search

b-mehta / topos

Topos theory in lean
55 stars 2 forks source link

Pullback of isomorphism #26

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

If two objects are isomorphic, then the pullbacks are iso. More specifically,

lemma pullback_iso' {U V W X : C} {f : U ⟶ X} {g : V ⟶ X} {h : W ⟶ X} (z : V ≅ W) (hyp : z.hom ≫ h = g) (c : pullback_cone f g) :
  is_limit c ≅ is_limit (pullback_iso z hyp c) :=