pushout_inr_inv_inl_of_right_isIso

English

Let f: X → Y and g: X → Z with g an isomorphism. Then the relation (pushout.inr f g)^{-1} ≡ (pushout.inl f g)^{-1} ⋅ (f^{-1} ⋅ g) holds; equivalently, pushout.inr is invertible and relates to inl and f.

Русский

Пусть f: X → Y и g: X → Z с g изоморфизм. Тогда существует равенство обратных стрелок в пушауте между inr и inl через f^{-1} и g.

LaTeX

$$$(\mathrm{pushout.inr}(f,g))^{-1} = (\mathrm{pushout.inl}(f,g))^{-1} \circ f^{-1} \circ g$$$

Lean4

@[reassoc (attr := simp)]
theorem pushout_inr_inv_inl_of_right_isIso : pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f := by
  rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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