English
An instance ensures pullback.map f1 f2 g1 g2 i1 i2 i3 is an isomorphism under iso legs and pushout structure.
Русский
Экземпляр обеспечивает изоморфизм pullback.map f1 f2 g1 g2 i1 i2 i3 при условии, что ноги — изоморфизмы и присутствует структура пуш-аута.
LaTeX
$$$\mathrm{IsIso}\big(\mathrm{pullback.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₁ : W ⟶ S) (f₂ : X ⟶ S) [HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T)
[HasPullback 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 (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :=
by
refine ⟨⟨pullback.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
