hom_ext — Mathlib

English

If for all X,Y,B and open embedding f there is a pullback with g, then HasExplicitPullbacksOfInclusions P.

Русский

Если для всех X,Y,B и открытого вложения f существует пуллбэк c g, тогда HasExplicitPullbacksOfInclusions P.

LaTeX

$$$\\forall X,Y,B\\ (f:X\\to B)\\ (g:Y\\to B)\\ (\\mathrm{IsOpenEmbedding}\\, f)\\Rightarrow \\text{HasExplicitPullback } f\\ g \\Rightarrow \\text{HasExplicitPullbacksOfInclusions } P$$$

Lean4

theorem hom_ext {Z : CompHausLike P} (a b : Z ⟶ pullback f g) (hfst : a ≫ pullback.fst f g = b ≫ pullback.fst f g)
    (hsnd : a ≫ pullback.snd f g = b ≫ pullback.snd f g) : a = b :=
  by
  ext z
  apply_fun (fun q ↦ q z) at hfst hsnd
  apply Subtype.ext
  apply Prod.ext
  · exact hfst
  · exact hsnd

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