pullback_fst_iso_of_right_iso — Mathlib

English

If g is an isomorphism, then the first projection from the pullback is an isomorphism.

Русский

Если правая дуга g изоморфизм, то первая проекция pullback является изоморфизмом.

LaTeX

$$$$ \text{pullback.fst}(f,g) \text{ is an isomorphism}. $$$$

Lean4

instance pullback_fst_iso_of_right_iso : IsIso (pullback.fst f g) :=
  by
  refine ⟨⟨pullback.lift (𝟙 _) (f ≫ inv g) (by simp), ?_, by simp⟩⟩
  ext
  · simp
  · simp [pullback.condition_assoc]

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