isIso_asLimitCone_lift — Mathlib

English

The lift from asLimitCone to the limit cone is an isomorphism.

Русский

Подъем из asLimitCone к пределу-конусу является изоморфизмом.

LaTeX

$$$\text{IsIso}( (\limConeIsLimit(X.diagram)).lift(X.asLimitCone) )$$$

Lean4

instance isIso_asLimitCone_lift : IsIso ((limitConeIsLimit.{u, u} X.diagram).lift X.asLimitCone) :=
  CompHausLike.isIso_of_bijective _
    (by
      refine ⟨fun a b h => ?_, fun a => ?_⟩
      · refine DiscreteQuotient.eq_of_forall_proj_eq fun S => ?_
        apply_fun fun f : (limitCone.{u, u} X.diagram).pt => f.val S at h
        exact h
      · obtain ⟨b, hb⟩ := DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
        use b
        apply Subtype.ext
        apply funext
        rintro S
        apply hb)

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