English
An instance ensures pushout.map f1 f2 g1 g2 i1 i2 i3 is an isomorphism under iso legs.
Русский
Экземпляр обеспечивает изоморфизм pushout.map f1 f2 g1 g2 i1 i2 i3 при условии изоморфизм ног.
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
instance map_isIso {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X) [HasPushout f₁ f₂] (g₁ : T ⟶ Y) (g₂ : T ⟶ Z)
[HasPushout g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁) (eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂)
[IsIso i₁] [IsIso i₂] [IsIso i₃] : IsIso (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :=
by
refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
· rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
· rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
· cat_disch
· cat_disch
