isoindexConeLift — Mathlib

English

There is a canonical isomorphism from Profinite.of C.Elem to the limit cone's point, induced by isoindexConeLift.

Русский

Существует канонический изоморфизм от Profinite.of C.Elem к точке предел-конуса, индуцируемый isoindexConeLift.

LaTeX

$$$\\text{isoindexConeLift}(hC): \\; \\text{indexCone}(hC) \\cong \\text{limitCone}(\\text{indexFunctor}(hC))$$$

Lean4

/-- The canonical map from `C` to the explicit limit as an isomorphism. -/
noncomputable def isoindexConeLift :
    @Profinite.of C _ (by rwa [← isCompact_iff_compactSpace]) _ _ ≅ (Profinite.limitCone.{u, u} (indexFunctor hC)).pt :=
  asIso <| (Profinite.limitConeIsLimit.{u, u} _).lift (indexCone hC)

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