fiberPullbackEquiv — Mathlib

English

The fiber of the pullback is the fiber product of the fibers.

Русский

Фибер pullback равен произведению волокон.

LaTeX

$$$\\mathrm{F.obj}(\\mathrm{pullback}(f,g)) \\cong { p:\\,\\mathrm{F.obj}(A) \\times \\mathrm{F.obj}(B) \\;|\\; \\mathrm{F.map}(f)p.1 = \\mathrm{F.map}(g)p.2 }$$$

Lean4

/-- The fiber of the pullback is the fiber product of the fibers. -/
noncomputable def fiberPullbackEquiv {X A B : C} (f : A ⟶ X) (g : B ⟶ X) :
    F.obj (pullback f g) ≃ { p : F.obj A × F.obj B // F.map f p.1 = F.map g p.2 } :=
  (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g ≪≫ Types.pullbackIsoPullback (F.map f) (F.map g)).toEquiv

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