rightExtensionInclusion — Mathlib

English

The identity natural transformation exhibits a right extension of the truncated restriction along the opposite of the truncation inclusion; in particular, the right extension of Truncated.inclusion n along its opposite yields the identity extension.

Русский

Идентичное натуральное преобразование задаёт правое продолжение ограничений, полученных от Truncated.inclusion n, через его противоположность, давая тождественное продолжение.

LaTeX

$$$\text{RightExtension}( \mathrm{Truncated.inclusion\, n}.\mathrm{op} , (\mathrm{Truncated.inclusion\, n}.\mathrm{op} \circ\!\!\! X))$ равен по определению тождественному трансформационному правому расширению.$$

Lean4

/-- The identity natural transformation exhibits a simplicial set as a right extension of its
restriction along `(Truncated.inclusion n).op`. -/
@[simps!]
def rightExtensionInclusion : RightExtension (Truncated.inclusion n).op ((Truncated.inclusion n).op ⋙ X) :=
  RightExtension.mk _ (𝟙 _)

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