isPointwiseRightKanExtension — Mathlib

English

If X carries a StrictSegal structure, then the right extension along the inclusion in dimension 2 is pointwise, i.e. the cones computing the extension are limit cones at each object.

Русский

Если X имеет структуру StrictSegal, то правое расширение вдоль включения в размер 2 является точечным, то есть конусы, вычисляющие расширение, являются пределами на каждом объекте.

LaTeX

$$$ \mathrm{IsPointwiseRightKanExtension}\big( \mathrm{rightExtensionInclusion}(X, 2) \big)$$$

Lean4

/-- Since `StrictSegal.isPointwiseRightKanExtensionAt` proves that the appropriate
cones are limit cones, `rightExtensionInclusion X 2` is a pointwise right Kan extension. -/
noncomputable def isPointwiseRightKanExtension : (rightExtensionInclusion X 2).IsPointwiseRightKanExtension := fun Δ =>
  sx.isPointwiseRightKanExtensionAt Δ.unop.len

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