asLimitConeAux — Mathlib

English

An auxiliary isomorphism between cones used to prove that S.asLimitConeAux is a limit cone.

Русский

Вспомогательный изоморфизм между конусами, используемый для доказательства, что S.asLimitConeAux является пределом конуса.

LaTeX

$$$\\text{isoMapCone} : \\mathrm{lightToProfinite.mapCone}(S.asLimitConeAux) \\cong S.toLightDiagram.cone$$$

Lean4

/-- A cone over `S.diagram` whose cone point is isomorphic to `S`.
(Auxiliary definition, use `S.asLimitCone` instead.)
-/
def asLimitConeAux : Cone S.diagram :=
  let c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
  let hc : IsLimit c := S.toLightDiagram.isLimit
  liftLimit hc

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