isoMapCone — Mathlib

English

Same as above: an auxiliary isomorphism of 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

/-- An auxiliary isomorphism of cones used to prove that `S.asLimitConeAux` is a limit cone. -/
def isoMapCone : lightToProfinite.mapCone S.asLimitConeAux ≅ S.toLightDiagram.cone :=
  let c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
  let hc : IsLimit c := S.toLightDiagram.isLimit
  liftedLimitMapsToOriginal hc

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