pullback_inv_fst_snd_of_right_isIso

English

If g is an isomorphism, then inv(fst) ; snd = f ; inv(g).

Русский

Если g является изоморфизмом, то inv(fst) ; snd = f ; inv(g).

LaTeX

$$$$ \mathrm{inv}(\mathrm{pullback.fst}(f,g)) \circ \mathrm{pullback.snd}(f,g) = f \circ \mathrm{inv}(g). $$$$

Lean4

@[reassoc (attr := simp)]
theorem pullback_inv_fst_snd_of_right_isIso : inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g := by
  rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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