isLimitEquivBijective — Mathlib

English

A pullback cone in Type is a limit iff the map to the explicit pullback obj is bijective.

Русский

Пуллбэк-конос в категориях типов есть предел тогда и только тогда, когда отображение в явный pullback объект является биекцией.

LaTeX

$$$\\text{IsLimit } c \\;\\simeq\\; \\mathrm{Bijective}\\; c.toPullbackObj$$$

Lean4

/-- A pullback cone `c` in the category of types is limit iff the
map `c.toPullbackObj : c.pt → Types.PullbackObj f g` is a bijection. -/
noncomputable def isLimitEquivBijective : IsLimit c ≃ Function.Bijective c.toPullbackObj
    where
  toFun h := (IsLimit.equivPullbackObj h).bijective
  invFun
    h :=
    IsLimit.ofIsoLimit (Types.pullbackLimitCone f g).isLimit (Iso.symm (PullbackCone.ext (Equiv.ofBijective _ h).toIso))
  left_inv _ := Subsingleton.elim _ _

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