mapLift_comp — Mathlib

English

Another assertion that the pushout map is an isomorphism under iso arms.

Русский

Ещё одно утверждение, что отображение pushout является изоморфизмом при условии изоморфий.

LaTeX

$$$\mathrm{IsIso}\big(\mathrm{CategoryTheory.Limits.pushout.map} f_1 f_2 g_1 g_2 i_1 i_2 i_3 eq_1 eq_2\big)$$$

Lean4

theorem mapLift_comp {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) (i' : S' ⟶ S) [HasPushout f g]
    [HasPushout (i ≫ f) (i ≫ g)] [HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)] [HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
    pushout.mapLift f g (i' ≫ i) =
      (pushout.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom ≫
        pushout.mapLift _ _ i' ≫ pushout.mapLift f g i :=
  by cat_disch

Похожие утверждения