homPullbackEquiv — Mathlib

English

The pullback cone satisfies the commuting condition fst ≫ f = snd ≫ g.

Русский

Конус обратного предела удовлетворяет условию пересечения fst ≫ f = snd ≫ g.

LaTeX

$$$(pullbackCone\\ f\\ g\\ pb).fst \\;\\gg\\; f = (pullbackCone\\ f\\ g\\ pb).snd \\;\\gg\\; g$$$

Lean4

/-- The `Equiv` that witnesses that `pullbackCone f g pb` is actually a pullback. This is the
universal property of pullbacks. -/
@[simps!]
def homPullbackEquiv : (T ⟶ (pullbackCone f g pb).pt) ≃ { p : (T ⟶ X) × (T ⟶ Y) // p.1 ≫ f = p.2 ≫ g }
    where
  toFun m := ⟨⟨m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd⟩, by simp⟩
  invFun
    s :=
    ⟨fun i ↦ ⟨(s.1.1.f i, s.1.2.f i), congrFun (congrArg Hom.f s.2) i⟩, fun i ↦
      (hpb _).lift (PullbackCone.mk (s.1.1.φ i) (s.1.2.φ i) (by simpa using ((hom_ext_iff _ _).1 s.2).2 i))⟩
  left_inv
    m :=
    hom_ext rfl
      (fun i ↦ by
        simp only [category_comp_f, category_comp_φ, eqToHom_refl, Category.comp_id]
        exact (hpb _).hom_ext ((pb _).equalizer_ext (by aesop) (by aesop)))
  right_inv s := by ext <;> simp

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