pullbackIsoProdSubtype_inv_snd — Mathlib

English

Let f: X -> Z and g: Y -> Z. There is a canonical isomorphism between the pullback and the subtype; the inverse followed by the second projection equals the standard second projection.

Русский

Пусть f: X → Z и g: Y → Z. Существуют каноническое изоморфизм между пределом pullback(f,g) и подтипом; обратное отображение затем вторая проекция совпадают с обычной проекцией на Y.

LaTeX

$$$ (pullbackIsoProdSubtype f g)^{-1} \circ pullback.snd\, f\, g = pullbackSnd\, f\, g $$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackIsoProdSubtype_inv_snd (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).inv ≫ pullback.snd _ _ = pullbackSnd f g := by
  simp [pullbackCone, pullbackIsoProdSubtype]

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