pullback_snd_iso_of_left_iso — Mathlib

English

If f is an isomorphism, then the second projection from the pullback is an isomorphism.

Русский

Если f — изоморфизм, то в pullback второй проекционный морфизм isomorphism.

LaTeX

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

Lean4

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

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